---

Step * of Lemma eager-append_assoc

∀[as,bs,cs:Top List].  (eager-append(eager-append(as;bs);cs) ~ eager-append(as;eager-append(bs;cs)))
BY
{ (Intros THEN (RWW "eager-append-is-append" 0 THENA Auto) THEN BLemma `append_assoc` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[as,bs,cs:Top  List].    (eager-append(eager-append(as;bs);cs)  \msim{}  eager-append(as;eager-append(bs;cs)))


By

---

Latex:
(Intros  THEN  (RWW  "eager-append-is-append"  0  THENA  Auto)  THEN  BLemma  `append\_assoc`  THEN  Auto)

---

Home Index