---

Step * of Lemma append_assoc

∀[as,bs,cs:Top].  ((as @ bs) @ cs ~ as @ bs @ cs)
BY
{ ListIndSq `as' }

---

Latex:

---

Latex:
\mforall{}[as,bs,cs:Top].    ((as  @  bs)  @  cs  \msim{}  as  @  bs  @  cs)


By

---

Latex:
ListIndSq  `as'

---

Home Index