---

Step * 1 1 1 of Lemma bag-extensionality-no-repeats

.....antecedent..... 
1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. as : T List
4. bs : T List
5. L1 : T List
6. L1 = as ∈ (as,bs:T List//permutation(T;as;bs))
7. L1 ∈ T List
8. as ∈ T List
9. permutation(T;L1;as)
10. no_repeats(T;L1)
11. L : T List
12. L = bs ∈ (as,bs:T List//permutation(T;as;bs))
13. L ∈ T List
14. bs ∈ T List
15. permutation(T;L;bs)
16. no_repeats(T;L)
17. ∀x:T. uiff(x ↓∈ as;x ↓∈ bs)
18. x : T
19. (x ∈ bs)
20. x ↓∈ bs supposing x ↓∈ as
⊢ x ↓∈ bs
BY
{ (D 0 THEN Auto THEN With ⌜bs⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  as  :  T  List
4.  bs  :  T  List
5.  L1  :  T  List
6.  L1  =  as
7.  L1  \mmember{}  T  List
8.  as  \mmember{}  T  List
9.  permutation(T;L1;as)
10.  no\_repeats(T;L1)
11.  L  :  T  List
12.  L  =  bs
13.  L  \mmember{}  T  List
14.  bs  \mmember{}  T  List
15.  permutation(T;L;bs)
16.  no\_repeats(T;L)
17.  \mforall{}x:T.  uiff(x  \mdownarrow{}\mmember{}  as;x  \mdownarrow{}\mmember{}  bs)
18.  x  :  T
19.  (x  \mmember{}  bs)
20.  x  \mdownarrow{}\mmember{}  bs  supposing  x  \mdownarrow{}\mmember{}  as
\mvdash{}  x  \mdownarrow{}\mmember{}  bs


By

---

Latex:
(D  0  THEN  Auto  THEN  With  \mkleeneopen{}bs\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index