---

Step * of Lemma reverse-cons

∀[as,a:Top].  (rev([a / as]) ~ rev(as) @ [a])
BY
{ (((UnivCD THENA Auto) THEN RepUR ``reverse`` 0)
   THEN RWO "rev-append-property-top<" 0
   THEN Auto
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[as,a:Top].    (rev([a  /  as])  \msim{}  rev(as)  @  [a])


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  RepUR  ``reverse``  0)
  THEN  RWO  "rev-append-property-top<"  0
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto)

---

Home Index