---

Step * of Lemma listid-sq

∀[L:Top List]. (listid(L) ~ L)
BY
{ InductionOnList
THEN Reduce 0
THEN EqCD
THEN Auto }

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  (listid(L)  \msim{}  L)


By

---

Latex:
InductionOnList
THEN  Reduce  0
THEN  EqCD
THEN  Auto

---

Home Index