---

Step * of Lemma is-list-prop2

∀[T:Type]. ∀[t:T List].  (is-list(t))↓
BY
{ (Auto THEN ListInd 2 THEN (RecUnfold `is-list` 0⋅ THEN (RepUR ``cons`` 0 THEN Reduce 0) THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[t:T  List].    (is-list(t))\mdownarrow{}


By

---

Latex:
(Auto  THEN  ListInd  2  THEN  (RecUnfold  `is-list`  0\mcdot{}  THEN  (RepUR  ``cons``  0  THEN  Reduce  0)  THEN  Auto)\mcdot{})

---

Home Index