---

Step * 1 1 of Lemma extend-type-property

.....subterm..... T:t
1:n
1. T : Type
2. x : T
⊢ x ∈ (T)+
BY
{ (PointwiseFunctionalityForEquality (-1) THENA Auto) }

1
1. T : Type
2. x : Base
3. x1 : Base
4. x = x1 ∈ T
⊢ x = x1 ∈ (T)+

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  T  :  Type
2.  x  :  T
\mvdash{}  x  \mmember{}  (T)+


By

---

Latex:
(PointwiseFunctionalityForEquality  (-1)  THENA  Auto)

---

Home Index