---

Step * of Lemma extend-type-property

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

1
1. [T] : Type
⊢ T ⊆r (T)+

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

---

Latex:

---

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


By

---

Latex:
(Intro  THEN  D  0)

---

Home Index