---

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


1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. as : bag(T)
4. bs : bag(T)
5. bag-no-repeats(T;as)
6. bag-no-repeats(T;bs)
7. ∀x:T. uiff(x ↓∈ as;x ↓∈ bs)
⊢ as = bs ∈ bag(T)
BY
{ ((BagToList 3 THEN Auto)
   THEN (BagToList 4 THEN Auto)
   THEN D (-3)
   THEN D -2
   THEN ExRepD
   THEN (EqTypeHD (-6) THEN Auto)
   THEN EqTypeHD (-3)
   THEN Auto
   THEN EqTypeCD 
   THEN Auto
   THEN BLemma `permutation-when-no_repeats`
   THEN Auto) }

1
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)
⊢ (x ∈ as)

2
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 ∈ as)
⊢ (x ∈ bs)

---

Latex:

---

Latex:

1.  T  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  as  :  bag(T)
4.  bs  :  bag(T)
5.  bag-no-repeats(T;as)
6.  bag-no-repeats(T;bs)
7.  \mforall{}x:T.  uiff(x  \mdownarrow{}\mmember{}  as;x  \mdownarrow{}\mmember{}  bs)
\mvdash{}  as  =  bs


By

---

Latex:
((BagToList  3  THEN  Auto)
  THEN  (BagToList  4  THEN  Auto)
  THEN  D  (-3)
  THEN  D  -2
  THEN  ExRepD
  THEN  (EqTypeHD  (-6)  THEN  Auto)
  THEN  EqTypeHD  (-3)
  THEN  Auto
  THEN  EqTypeCD 
  THEN  Auto
  THEN  BLemma  `permutation-when-no\_repeats`
  THEN  Auto)

---

Home Index