---

Step * of Lemma rev-append-pair

∀[a,b,c:Top].  (rev(<a, b>) + c ~ rev(b) + <a, c>)
BY
{ (Fold `cons` 0 THEN RepUR ``rev-append`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b,c:Top].    (rev(<a,  b>)  +  c  \msim{}  rev(b)  +  <a,  c>)


By

---

Latex:
(Fold  `cons`  0  THEN  RepUR  ``rev-append``  0  THEN  Auto)

---

Home Index