---

Step * of Lemma rev-append-property-top

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

---

Latex:

---

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


By

---

Latex:
ListAccumSq  `as'

---

Home Index