---

Step * 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
⊢ [u / (v @ bs)][i] = [u / v][i] ∈ T
BY
{ (CaseNat 0 `i' THEN Reduce 0 THEN Auto) }

1
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

---

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
\mvdash{}  [u  /  (v  @  bs)][i]  =  [u  /  v][i]


By

---

Latex:
(CaseNat  0  `i'  THEN  Reduce  0  THEN  Auto)

---

Home Index