---

Step * of Lemma listid_wf

∀[A:Type]. ∀[L:A List].  (listid(L) ∈ A List)
BY
{ InductionOnList
THEN RepUR ``listid`` 0
THEN Try (Fold `listid` 0)
THEN Auto }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[L:A  List].    (listid(L)  \mmember{}  A  List)


By

---

Latex:
InductionOnList
THEN  RepUR  ``listid``  0
THEN  Try  (Fold  `listid`  0)
THEN  Auto

---

Home Index