---

Step * 1 of Lemma select_append_front


1. T : Type
2. as : T List
3. bs : T List
4. i : ℕ||as||
⊢ as @ bs[i] = as[i] ∈ T
BY
{ (((ListInd 2 THEN AbReduce 0) THEN D 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
⊢ [u / (v @ bs)][i] = [u / v][i] ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  i  :  \mBbbN{}||as||
\mvdash{}  as  @  bs[i]  =  as[i]


By

---

Latex:
(((ListInd  2  THEN  AbReduce  0)  THEN  D  0)  THEN  Auto)

---

Home Index