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