---

Step * of Lemma hd-reverse-is-last

∀[T:Type]. ∀[L:T List].  hd(rev(L)) = last(L) ∈ T supposing 0 < ||L||
BY
{ ((Auto THEN Unfold `last` 0)
   THEN (InstLemma `select-reverse` [⌜T⌝;⌜L⌝;⌜0⌝]⋅ THENA Auto)
   THEN RWO "select0" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    hd(rev(L))  =  last(L)  supposing  0  <  ||L||


By

---

Latex:
((Auto  THEN  Unfold  `last`  0)
  THEN  (InstLemma  `select-reverse`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "select0"  (-1)
  THEN  Auto)

---

Home Index