---

Step * 1 of Lemma hd-reverse


1. T : Type
2. L : T List
⊢ hd(rev(L)) ~ last(L)
BY
{ Subst ⌜L ~ rev(rev(L))⌝ 0⋅ }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
Subst  \mkleeneopen{}L  \msim{}  rev(rev(L))\mkleeneclose{}  0\mcdot{}

---

Home Index