---

Step * of Lemma bag-subtype-fset

∀[A:Type]. (bag(A) ⊆r fset(A))
BY
{ xxx(((Auto THEN D 0) THENM D -1) THEN Auto THEN EqTypeCD THEN Auto)xxx }

1
.....antecedent..... 
1. A : Type
2. x : Base
3. x1 : Base
4. x = x1 ∈ pertype(λas,bs. ((as ∈ A List) ∧ (bs ∈ A List) ∧ permutation(A;as;bs)))
5. x ∈ A List
6. x1 ∈ A List
7. permutation(A;x;x1)
⊢ set-equal(A;x;x1)

---

Latex:

---

Latex:
\mforall{}[A:Type].  (bag(A)  \msubseteq{}r  fset(A))


By

---

Latex:
xxx(((Auto  THEN  D  0)  THENM  D  -1)  THEN  Auto  THEN  EqTypeCD  THEN  Auto)xxx

---

Home Index