Nuprl Rule : dependent_set_memberEquality_alt
H  ⊢ a1 = a2 ∈ {x:A| B} 
  BY dependent_set_memberEquality_alt y ()
  
  H  ⊢ a1 = a2 ∈ A
  H  ⊢ B[a1/x]
  H y:A ⊢ istype(B[y/x])
Latex:
H    \mvdash{}  a1  =  a2
    BY  dependent\_set\_memberEquality\_alt  y  ()
   
    H    \mvdash{}  a1  =  a2
    H    \mvdash{}  B[a1/x]
    H  y:A  \mvdash{}  istype(B[y/x])
Date html generated:
2019_06_20-PM-04_11_44
Last ObjectModification:
2018_09_25-PM-02_46_11
Theory : rules
Home
Index