---

Step * 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,ds:T List. ((bs = (cs @ [u / ds]) ∈ (T List)) ∧ v ⊆ cs @ ds)
⊢ [u / v] ⊆ bs
BY
{ (((ExRepD THEN (HypSubst' -2 0 THENA Auto))
    THEN RepeatFor 2 (ParallelLast)
    THEN (RWO "member_append" (-1) THENA Auto)⋅
    THEN (RWO "member_append" 0 THENA Auto)⋅)
   THEN (Auto THEN CaseNat 0 `i')
   THEN Reduce 0) }

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 ∈ ℤ
⊢ (u ∈ cs) ∨ (u ∈ [u / ds])

2
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])

---

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.  \mexists{}cs,ds:T  List.  ((bs  =  (cs  @  [u  /  ds]))  \mwedge{}  v  \msubseteq{}  cs  @  ds)
\mvdash{}  [u  /  v]  \msubseteq{}  bs


By

---

Latex:
(((ExRepD  THEN  (HypSubst'  -2  0  THENA  Auto))
    THEN  RepeatFor  2  (ParallelLast)
    THEN  (RWO  "member\_append"  (-1)  THENA  Auto)\mcdot{}
    THEN  (RWO  "member\_append"  0  THENA  Auto)\mcdot{})
  THEN  (Auto  THEN  CaseNat  0  `i')
  THEN  Reduce  0)

---

Home Index