---

Step * of Lemma bag-map_wf

∀[B,A:Type]. ∀[f:A ⟶ B]. ∀[bs:bag(A)].  (bag-map(f;bs) ∈ bag(B))
BY
{ ((UnivCD THENA Auto)
   THEN (D -1 THENA Auto)
   THEN Unfold `bag-map` 0
   THEN EqTypeCD
   THEN Auto
   THEN BLemma `permutation-map`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[B,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[bs:bag(A)].    (bag-map(f;bs)  \mmember{}  bag(B))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (D  -1  THENA  Auto)
  THEN  Unfold  `bag-map`  0
  THEN  EqTypeCD
  THEN  Auto
  THEN  BLemma  `permutation-map`
  THEN  Auto)

---

Home Index