Nuprl Rule : setEquality

This rule proved as lemma rule_set_equality_true in file rules/rules_set.v at https://github.com/vrahli/NuprlInCoq  

H  ⊢ {x1:A1| B1}  {x2:A2| B2}  ∈ Type

  BY setEquality x
  
  H  ⊢ A1 A2 ∈ Type
  x:A1 ⊢ B1[x/x1] B2[x/x2] ∈ Type



Definitions occuring in rule :  set: {x:A| B[x]}  equal: t ∈ T universe: Type axiom: Ax

Latex:
H    \mvdash{}  \{x1:A1|  B1\}    =  \{x2:A2|  B2\} 

    BY  setEquality  x
   
    H    \mvdash{}  A1  =  A2
    H  x:A1  \mvdash{}  B1[x/x1]  =  B2[x/x2]



Date html generated: 2016_12_14-AM-08_53_26
Last ObjectModification: 2016_07_08-PM-03_48_48

Theory : rules


Home Index