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