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