---

Step * 1 of Lemma select_append_back


1. T : Type
2. as : T List
3. bs : T List
4. i : {||as||..||as|| + ||bs||-}
⊢ as @ bs[i] = bs[i - ||as||] ∈ T
BY
{ (((ListInd 2 THEN AbReduce 0) THEN D 0) THENA Auto) }

1
1. T : Type
2. bs : T List
3. i : ℕ0 + ||bs||
⊢ bs[i] = bs[i - 0] ∈ T

2
1. T : Type
2. bs : T List
3. u : T
4. v : T List
5. ∀i:{||v||..||v|| + ||bs||-}. (v @ bs[i] = bs[i - ||v||] ∈ T)
6. i : {||v|| + 1..(||v|| + 1) + ||bs||-}
⊢ [u / (v @ bs)][i] = bs[i - ||v|| + 1] ∈ T

---

Latex:

---

Latex:

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


By

---

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

---

Home Index