---

Step * of Lemma record+_subtype_rel

∀[T:Type]. ∀[B:T ⟶ Type]. ∀[z:Atom].  (T; z:B[self] ⊆r T)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[B:T  {}\mrightarrow{}  Type].  \mforall{}[z:Atom].    (T;  z:B[self]  \msubseteq{}r  T)


By

---

Latex:
Auto

---

Home Index