---

Step * 2 1 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 ∈ cs) ∨ (u ∈ [u / ds])
BY
{ (OrRight THEN Auto)⋅ }

---

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.  i  =  0
\mvdash{}  (u  \mmember{}  cs)  \mvee{}  (u  \mmember{}  [u  /  ds])


By

---

Latex:
(OrRight  THEN  Auto)\mcdot{}

---

Home Index