---

Step * 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||
⊢ firstn(e;L) @ [if e <z ||L|| then L[e] else hd(L) fi ] ~ firstn(e + 1;L)
BY
{ AutoSplit }

1
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)

---

Latex:

---

Latex:

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


By

---

Latex:
AutoSplit

---

Home Index