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
  H x:A1 ⊢ B1[x/x1] = B2[x/x2] ∈ Type
Definitions occuring in rule : 
set: {x:A| B[x]} 
, 
equal: s = 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:
2019_06_20-PM-04_11_48
Last ObjectModification:
2016_07_08-PM-03_48_48
Theory : rules
Home
Index