---

Step * of Lemma append-nil

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

---

Latex:

---

Latex:
\mforall{}[l:Top  List].  (l  @  []  \msim{}  l)


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  EqCD  THEN  Auto)

---

Home Index