---

Step * 1 of Lemma set-equal-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. set-equal(T;[u / v];bs)
⊢ ∃cs,ds:T List. ((bs = (cs @ [u / ds]) ∈ (T List)) ∧ set-equal(T;v;cs @ ds))
BY
{ (Assert (u ∈ bs) BY
         (UnfoldTopAb (-1) THEN (InstHyp [⌜u⌝] (-1)⋅ THENA Auto) THEN D -1 THEN D -2 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. set-equal(T;[u / v];bs)
8. (u ∈ bs)
⊢ ∃cs,ds:T List. ((bs = (cs @ [u / ds]) ∈ (T List)) ∧ set-equal(T;v;cs @ 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.  set-equal(T;[u  /  v];bs)
\mvdash{}  \mexists{}cs,ds:T  List.  ((bs  =  (cs  @  [u  /  ds]))  \mwedge{}  set-equal(T;v;cs  @  ds))


By

---

Latex:
(Assert  (u  \mmember{}  bs)  BY
              (UnfoldTopAb  (-1)  THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  D  -2  THEN  Auto))\mcdot{}

---

Home Index