---

Step * of Lemma respects-equality-bag

∀[A,B:Type].  respects-equality(bag(A);bag(B)) supposing respects-equality(A;B)
BY
{ (Intros THEN Unfold `bag` 0 THEN BLemma `respects-equality-quotient` THEN (Complete (Auto) ORELSE Intros)) }

1
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
7. as ∈ B List
⊢ (bs ∈ B List) ∧ permutation(B;as;bs)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    respects-equality(bag(A);bag(B))  supposing  respects-equality(A;B)


By

---

Latex:
(Intros
  THEN  Unfold  `bag`  0
  THEN  BLemma  `respects-equality-quotient`
  THEN  (Complete  (Auto)  ORELSE  Intros))

---

Home Index