---

Step * of Lemma append_assoc_sq

∀[as,bs,cs:Top].  ((as @ bs) @ cs ~ as @ bs @ cs)
BY
{ (InstLemma `append_assoc` [] THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `append\_assoc`  []  THEN  Trivial)

---

Home Index