---

Step * 1 of Lemma bag-extensionality1


1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. ∀[x,y:T].  (↑(eq x y) ⇐⇒ x = y ∈ T)
4. as : bag(T)
5. bs : bag(T)
6. ∀x:T. (#([y∈as|eq x y]) = #([y∈bs|eq x y]) ∈ ℤ)
⊢ as = bs ∈ bag(T)
BY
{ (OnVar `as' newQuotD THEN OnVar `bs' newQuotD THEN ((Unfold `bag` 0 THEN EqTypeCD) THEN Auto)⋅) }

1
.....antecedent..... 
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. ∀[x,y:T].  (↑(eq x y) ⇐⇒ x = y ∈ T)
4. T List ∈ Type
5. ∀a1,b1:T List.  (permutation(T;a1;b1) ∈ Type)
6. ∀a1:T List. permutation(T;a1;a1)
7. a : Base
8. b : Base
9. c : a = b ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
10. a ∈ T List
11. b ∈ T List
12. permutation(T;a;b)
13. T List ∈ Type
14. ∀as,b1:T List.  (permutation(T;as;b1) ∈ Type)
15. ∀as:T List. permutation(T;as;as)
16. a1 : Base
17. b1 : Base
18. c1 : a1 = b1 ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
19. a1 ∈ T List
20. b1 ∈ T List
21. permutation(T;a1;b1)
22. ∀x:T. (#([y∈a|eq x y]) = #([y∈a1|eq x y]) ∈ ℤ)
⊢ permutation(T;a;a1)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
3.  \mforall{}[x,y:T].    (\muparrow{}(eq  x  y)  \mLeftarrow{}{}\mRightarrow{}  x  =  y)
4.  as  :  bag(T)
5.  bs  :  bag(T)
6.  \mforall{}x:T.  (\#([y\mmember{}as|eq  x  y])  =  \#([y\mmember{}bs|eq  x  y]))
\mvdash{}  as  =  bs


By

---

Latex:
(OnVar  `as'  newQuotD  THEN  OnVar  `bs'  newQuotD  THEN  ((Unfold  `bag`  0  THEN  EqTypeCD)  THEN  Auto)\mcdot{})

---

Home Index