Step
*
1
of Lemma
uand-subtype1
1. A : Type
2. B : Type
3. z : ⋂x:Base. ⋂p:(x)↓. if x = Ax then A otherwise B
4. y : ⋂p:(Ax)↓. if Ax = Ax then A otherwise B
5. y = z ∈ (⋂p:0 ≤ 0. A)
⊢ z ∈ A
BY
{ ((SubsumeC ⌜⋂p:0 ≤ 0. A⌝⋅ THEN Auto) THEN D 0 THEN Auto) }
Latex:
Latex:
1. A : Type
2. B : Type
3. z : \mcap{}x:Base. \mcap{}p:(x)\mdownarrow{}. if x = Ax then A otherwise B
4. y : \mcap{}p:(Ax)\mdownarrow{}. if Ax = Ax then A otherwise B
5. y = z
\mvdash{} z \mmember{} A
By
Latex:
((SubsumeC \mkleeneopen{}\mcap{}p:0 \mleq{} 0. A\mkleeneclose{}\mcdot{} THEN Auto) THEN D 0 THEN Auto)
Home
Index