---

Step * 2 1 of Lemma extend-type-property


1. [T] : Type
⊢ respects-equality((T)+;T)
BY
{ RepeatFor 4 ((D 0 THENW Auto)) }

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

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  respects-equality((T)+;T)


By

---

Latex:
RepeatFor  4  ((D  0  THENW  Auto))

---

Home Index