---

Step * 2 2 of Lemma extend-type-property


1. [T] : Type
⊢ ∀X:Type. (respects-equality(X;T) ⇒ (X ⊆r (T)+))
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
.....subterm..... T:t
1:n
1. T : Type
2. X : Type
3. respects-equality(X;T)
4. x : X
⊢ x ∈ (T)+

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  \mforall{}X:Type.  (respects-equality(X;T)  {}\mRightarrow{}  (X  \msubseteq{}r  (T)+))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index