---

Step * of Lemma rev-append-rev-append

∀[as:Top List]. ∀[bs,cs:Top].  (rev(rev(as) + bs) + cs ~ rev(bs) + as @ cs)
BY
{ ((InductionOnList THEN Reduce 0) THEN (RWW "-1" 0 THENA Auto) THEN Reduce 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((InductionOnList  THEN  Reduce  0)  THEN  (RWW  "-1"  0  THENA  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index