---

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


1. L : Top List@i
2. i : Id@i
3. e : ℕ@i
4. e < ||L||
⊢ map(λe.if e <z ||L|| then L[e] else hd(L) fi ;upto(e)) ~ firstn(e;L)
BY
{ (Thin 2 THEN RepeatFor 2 (MoveToConcl (-1)) THEN ListInd 1 THEN Auto') }

1
1. u : Top
2. v : Top List
3. ∀e:ℕ. (e < ||v|| ⇒ (map(λe.if e <z ||v|| then v[e] else hd(v) fi ;upto(e)) ~ firstn(e;v)))
4. e : ℕ@i
5. e < ||[u / v]||@i
⊢ map(λe.if e <z ||[u / v]|| then [u / v][e] else hd([u / v]) fi ;upto(e)) ~ firstn(e;[u / v])

---

Latex:

---

Latex:

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


By

---

Latex:
(Thin  2  THEN  RepeatFor  2  (MoveToConcl  (-1))  THEN  ListInd  1  THEN  Auto')

---

Home Index