Step
*
1
1
of Lemma
hd-reverse
.....equality..... 
1. T : Type
2. L : T List
⊢ L ~ rev(rev(L))
BY
{ (RWO "reverse-reverse" 0 THEN Auto) }
Latex:
Latex:
.....equality..... 
1.  T  :  Type
2.  L  :  T  List
\mvdash{}  L  \msim{}  rev(rev(L))
By
Latex:
(RWO  "reverse-reverse"  0  THEN  Auto)
Home
Index