---

Step * 1 1 1 of Lemma select_append_front


1. T : Type
2. bs : T List
3. u : T
4. v : T List
5. ∀i:ℕ||v||. (v @ bs[i] = v[i] ∈ T)
6. i : ℕ||v|| + 1
7. ¬(i = 0 ∈ ℤ)
⊢ [u / (v @ bs)][i] = [u / v][i] ∈ T
BY
{ (RWO "select_cons_tl" 0 THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  T  List
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}i:\mBbbN{}||v||.  (v  @  bs[i]  =  v[i])
6.  i  :  \mBbbN{}||v||  +  1
7.  \mneg{}(i  =  0)
\mvdash{}  [u  /  (v  @  bs)][i]  =  [u  /  v][i]


By

---

Latex:
(RWO  "select\_cons\_tl"  0  THEN  Auto')

---

Home Index