---

Step * 1 1 of Lemma select_append_back


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

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  T  List
3.  i  :  \mBbbN{}0  +  ||bs||
\mvdash{}  bs[i]  =  bs[i  -  0]


By

---

Latex:
Auto

---

Home Index