---

Step * of Lemma set-equal-cons

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index