Step
*
1
2
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 ∈ as)
⊢ (x ∈ bs)
BY
{ ((InstHyp [⌜x⌝] (-3)⋅ THEN Auto) THEN D -2) }
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 ∈ as)
20. x ↓∈ as supposing 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)
20. x ↓∈ as supposing x ↓∈ bs
21. x ↓∈ bs
⊢ (x ∈ bs)
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{}  as)
\mvdash{}  (x  \mmember{}  bs)
By
Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-3)\mcdot{}  THEN  Auto)  THEN  D  -2)
Home
Index