---

Step * of Lemma rev-append-axiom

∀[c:Top]. (rev(Ax) + c ~ c)
BY
{ (Fold `it` 0 THEN Fold `nil` 0 THEN RepUR ``rev-append`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[c:Top].  (rev(Ax)  +  c  \msim{}  c)


By

---

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

---

Home Index