---

Step * of Lemma last-reverse

∀[T:Type]. ∀[L:T List].  (last(rev(L)) ~ hd(L))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN ((RWO "last_append" 0 THENA Auto)
   ORELSE (TACTIC:TACTIC:RepUR ``hd nil it`` 0 THEN (RWO "pi1-axiom" 0 THENA Auto))
   )
   THEN RepUR ``last`` 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    (last(rev(L))  \msim{}  hd(L))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  ((RWO  "last\_append"  0  THENA  Auto)
  ORELSE  (TACTIC:TACTIC:RepUR  ``hd  nil  it``  0  THEN  (RWO  "pi1-axiom"  0  THENA  Auto))
  )
  THEN  RepUR  ``last``  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index