---

Step * of Lemma rev-append-append

∀[as:Top List]. ∀[bs,cs:Top].  (rev(as @ bs) + cs ~ rev(bs) + rev(as) + cs)
BY
{ ((UnivCD THENA Auto) THEN Unfold `rev-append` 0 THEN RWO "list_accum_append" 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `rev-append`  0  THEN  RWO  "list\_accum\_append"  0  THEN  Auto)

---

Home Index