---

Step * of Lemma list_subtype_base

∀[A:Type]. (A List) ⊆r Base supposing A ⊆r Base
BY
{ ((UnivCD THENA Auto) THEN (D 0 THENA Auto) THEN ListInd (-1) THEN RepUR ``nil cons`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  (A  List)  \msubseteq{}r  Base  supposing  A  \msubseteq{}r  Base


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (D  0  THENA  Auto)  THEN  ListInd  (-1)  THEN  RepUR  ``nil  cons``  0  THEN  Auto)

---

Home Index