---

Step * of Lemma l_contains-cons

∀[T:Type]
  ∀u:T. ∀v,bs:T List.
    ([u / v] ⊆ bs ⇐⇒ ∃cs,ds:T List. ((bs = (cs @ [u / ds]) ∈ (T List)) ∧ v ⊆ cs @ ds)) supposing 
       (no_repeats(T;bs) and 
       no_repeats(T;[u / v]))
BY
{ 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. [u / v] ⊆ bs
⊢ ∃cs,ds:T List. ((bs = (cs @ [u / ds]) ∈ (T List)) ∧ v ⊆ cs @ 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,ds:T List. ((bs = (cs @ [u / ds]) ∈ (T List)) ∧ v ⊆ cs @ ds)
⊢ [u / v] ⊆ bs

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}u:T.  \mforall{}v,bs:T  List.
        ([u  /  v]  \msubseteq{}  bs  \mLeftarrow{}{}\mRightarrow{}  \mexists{}cs,ds:T  List.  ((bs  =  (cs  @  [u  /  ds]))  \mwedge{}  v  \msubseteq{}  cs  @  ds))  supposing 
              (no\_repeats(T;bs)  and 
              no\_repeats(T;[u  /  v]))


By

---

Latex:
Auto

---

Home Index