---

Step * 1 2 1 of Lemma hd-reverse


1. T : Type
2. L : T List
⊢ rev(rev(L)) ~ L
BY
{ (RWO "reverse-reverse" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "reverse-reverse"  0  THEN  Auto)\mcdot{}

---

Home Index