---

Step * 1 1 1 2 of Lemma firstn_is_iseg


1. T : Type
2. l : T List
3. u : T
4. v : T List
5. v = firstn(||v||;v @ l) ∈ (T List)
⊢ [u / v] = firstn(||v|| + 1;[u / (v @ l)]) ∈ (T List)
BY
{ Subst firstn(||v|| + 1;[u / (v @ l)]) ~ [u / firstn(||v||;v @ l)] 0 }

1
.....equality..... 
1. T : Type
2. l : T List
3. u : T
4. v : T List
5. v = firstn(||v||;v @ l) ∈ (T List)
⊢ firstn(||v|| + 1;[u / (v @ l)]) ~ [u / firstn(||v||;v @ l)]

2
1. T : Type
2. l : T List
3. u : T
4. v : T List
5. v = firstn(||v||;v @ l) ∈ (T List)
⊢ [u / v] = [u / firstn(||v||;v @ l)] ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  l  :  T  List
3.  u  :  T
4.  v  :  T  List
5.  v  =  firstn(||v||;v  @  l)
\mvdash{}  [u  /  v]  =  firstn(||v||  +  1;[u  /  (v  @  l)])


By

---

Latex:
Subst  firstn(||v||  +  1;[u  /  (v  @  l)])  \msim{}  [u  /  firstn(||v||;v  @  l)]  0

---

Home Index