---

Step * 2 of Lemma extend-type-property


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

1
1. [T] : Type
⊢ respects-equality((T)+;T)

2
1. [T] : Type
⊢ ∀X:Type. (respects-equality(X;T) ⇒ (X ⊆r (T)+))

---

Latex:

---

Latex:

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


By

---

Latex:
D  0

---

Home Index