---

Step * 1 2 of Lemma hd-reverse


1. T : Type
2. L : T List
⊢ hd(rev(rev(rev(L)))) ~ last(rev(rev(L)))
BY
{ ((RWO "last-reverse" 0 THENA Auto) THEN RepeatFor 2 (EqCD)) }

1
1. T : Type
2. L : T List
⊢ rev(rev(L)) ~ L

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
\mvdash{}  hd(rev(rev(rev(L))))  \msim{}  last(rev(rev(L)))


By

---

Latex:
((RWO  "last-reverse"  0  THENA  Auto)  THEN  RepeatFor  2  (EqCD))

---

Home Index