---

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


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)
BY
{ ((InstHyp [⌜x⌝] (-3)⋅ THEN Auto) THEN D -1) }

1
.....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

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 ∈ bs)
20. x ↓∈ bs supposing x ↓∈ as
21. x ↓∈ as
⊢ (x ∈ as)

---

Latex:

---

Latex:

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)
\mvdash{}  (x  \mmember{}  as)


By

---

Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-3)\mcdot{}  THEN  Auto)  THEN  D  -1)

---

Home Index