---

Step * 1 of Lemma bag-extensionality

.....antecedent..... 
1. T : Type
2. eq : EqDecider(T)
3. istype(T List)
4. ∀a1,b1:T List.  istype(permutation(T;a1;b1))
5. ∀a1:T List. permutation(T;a1;a1)
6. a : Base
7. b : Base
8. c : a = b ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
9. a ∈ T List
10. b ∈ T List
11. permutation(T;a;b)
12. istype(T List)
13. ∀as,b1:T List.  istype(permutation(T;as;b1))
14. ∀as:T List. permutation(T;as;as)
15. a1 : Base
16. b1 : Base
17. c1 : a1 = b1 ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
18. a1 ∈ T List
19. b1 ∈ T List
20. permutation(T;a1;b1)
21. ∀x:T. ((#x in a) = (#x in a1) ∈ ℤ)
⊢ permutation(T;a;a1)
BY
{ ((InstLemma `permutation-iff-count` [⌜T⌝;⌜eq⌝;⌜a⌝;⌜a1⌝]⋅ THENA Auto) THEN BHyp (-1) THEN (ParallelOp -2 THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. istype(T List)
4. ∀a1,b1:T List.  istype(permutation(T;a1;b1))
5. ∀a1:T List. permutation(T;a1;a1)
6. a : Base
7. b : Base
8. c : a = b ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
9. a ∈ T List
10. b ∈ T List
11. permutation(T;a;b)
12. istype(T List)
13. ∀as,b1:T List.  istype(permutation(T;as;b1))
14. ∀as:T List. permutation(T;as;as)
15. a1 : Base
16. b1 : Base
17. c1 : a1 = b1 ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
18. a1 ∈ T List
19. b1 ∈ T List
20. permutation(T;a1;b1)
21. ∀x:T. ((#x in a) = (#x in a1) ∈ ℤ)
22. ∀x:T. (||filter(eqof(eq) x;a)|| = ||filter(eqof(eq) x;a1)|| ∈ ℤ) ⇐⇒ permutation(T;a;a1)
23. x : T
24. (#x in a) = (#x in a1) ∈ ℤ
⊢ ||filter(eqof(eq) x;a)|| = ||filter(eqof(eq) x;a1)|| ∈ ℤ

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  istype(T  List)
4.  \mforall{}a1,b1:T  List.    istype(permutation(T;a1;b1))
5.  \mforall{}a1:T  List.  permutation(T;a1;a1)
6.  a  :  Base
7.  b  :  Base
8.  c  :  a  =  b
9.  a  \mmember{}  T  List
10.  b  \mmember{}  T  List
11.  permutation(T;a;b)
12.  istype(T  List)
13.  \mforall{}as,b1:T  List.    istype(permutation(T;as;b1))
14.  \mforall{}as:T  List.  permutation(T;as;as)
15.  a1  :  Base
16.  b1  :  Base
17.  c1  :  a1  =  b1
18.  a1  \mmember{}  T  List
19.  b1  \mmember{}  T  List
20.  permutation(T;a1;b1)
21.  \mforall{}x:T.  ((\#x  in  a)  =  (\#x  in  a1))
\mvdash{}  permutation(T;a;a1)


By

---

Latex:
((InstLemma  `permutation-iff-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  (-1)
  THEN  (ParallelOp  -2  THENA  Auto))

---

Home Index