---

Step * of Lemma bag-extensionality

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].  uiff(as = bs ∈ bag(T);∀x:T. ((#x in as) = (#x in bs) ∈ ℤ))
BY
{ (Auto
   THEN (OnVar `as' newQuotD THENL [(OnVar `bs' newQuotD THENL [(Unfold `bag` 0 THEN EqTypeCD THEN Auto); Auto]); Auto])
   ) }

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[as,bs:bag(T)].    uiff(as  =  bs;\mforall{}x:T.  ((\#x  in  as)  =  (\#x  in  bs)))


By

---

Latex:
(Auto
  THEN  (OnVar  `as'  newQuotD
              THENL  [(OnVar  `bs'  newQuotD  THENL  [(Unfold  `bag`  0  THEN  EqTypeCD  THEN  Auto);  Auto]);  Auto]
            )
  )

---

Home Index