---

Step * 2 2 of Lemma l_contains-cons


1. [T] : Type
2. u : T
3. v : T List
4. bs : T List
5. no_repeats(T;[u / v])
6. no_repeats(T;bs)
7. cs : T List
8. ds : T List
9. bs = (cs @ [u / ds]) ∈ (T List)
10. ∀i:ℕ||v||. ((v[i] ∈ cs) ∨ (v[i] ∈ ds))
11. i : ℕ||[u / v]||
12. ¬(i = 0 ∈ ℤ)
⊢ ([u / v][i] ∈ cs) ∨ ([u / v][i] ∈ [u / ds])
BY
{ (RWO "select-cons-tl" 0 THEN Auto) }

1
1. [T] : Type
2. u : T
3. v : T List
4. bs : T List
5. no_repeats(T;[u / v])
6. no_repeats(T;bs)
7. cs : T List
8. ds : T List
9. bs = (cs @ [u / ds]) ∈ (T List)
10. ∀i:ℕ||v||. ((v[i] ∈ cs) ∨ (v[i] ∈ ds))
11. i : ℕ||[u / v]||
12. ¬(i = 0 ∈ ℤ)
⊢ (v[i - 1] ∈ cs) ∨ (v[i - 1] ∈ [u / ds])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  u  :  T
3.  v  :  T  List
4.  bs  :  T  List
5.  no\_repeats(T;[u  /  v])
6.  no\_repeats(T;bs)
7.  cs  :  T  List
8.  ds  :  T  List
9.  bs  =  (cs  @  [u  /  ds])
10.  \mforall{}i:\mBbbN{}||v||.  ((v[i]  \mmember{}  cs)  \mvee{}  (v[i]  \mmember{}  ds))
11.  i  :  \mBbbN{}||[u  /  v]||
12.  \mneg{}(i  =  0)
\mvdash{}  ([u  /  v][i]  \mmember{}  cs)  \mvee{}  ([u  /  v][i]  \mmember{}  [u  /  ds])


By

---

Latex:
(RWO  "select-cons-tl"  0  THEN  Auto)

---

Home Index