---

Step * 1 1 1 1 of Lemma list-eo-info-le-before


1. L : Top List@i
2. i : Id@i
3. e : {e:ℕ| ↑e <z ||L||} @i
4. e < ||L||
5. e < ||L||
⊢ firstn(e;L) @ [L[e]] ~ firstn(e + 1;L)
BY
{ (RW (AddrC [2] (RevLemmaC `firstn_decomp`)) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  Top  List@i
2.  i  :  Id@i
3.  e  :  \{e:\mBbbN{}|  \muparrow{}e  <z  ||L||\}  @i
4.  e  <  ||L||
5.  e  <  ||L||
\mvdash{}  firstn(e;L)  @  [L[e]]  \msim{}  firstn(e  +  1;L)


By

---

Latex:
(RW  (AddrC  [2]  (RevLemmaC  `firstn\_decomp`))  0  THEN  Auto)

---

Home Index