---

Step * of Lemma bag-combine-restrict_wf

∀[A,B:Type]. ∀[b:bag(A)]. ∀[f:{a:A| a ↓∈ b}  ⟶ bag(B)].  (bag-combine-restrict(b;x.f[x]) ∈ bag(B))
BY
{ (Auto
   THEN RepUR ``bag-combine-restrict bag-combine`` 0
   THEN (MemCD THENA Auto)
   THEN (Using [`A',⌜{a:A| a ↓∈ b} ⌝] (BLemma `bag-map_wf`)⋅ THEN Auto)
   THEN BLemma `bag-subtype`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[b:bag(A)].  \mforall{}[f:\{a:A|  a  \mdownarrow{}\mmember{}  b\}    {}\mrightarrow{}  bag(B)].    (bag-combine-restrict(b;x.f[x])  \mmember{}  bag(B))


By

---

Latex:
(Auto
  THEN  RepUR  ``bag-combine-restrict  bag-combine``  0
  THEN  (MemCD  THENA  Auto)
  THEN  (Using  [`A',\mkleeneopen{}\{a:A|  a  \mdownarrow{}\mmember{}  b\}  \mkleeneclose{}]  (BLemma  `bag-map\_wf`)\mcdot{}  THEN  Auto)
  THEN  BLemma  `bag-subtype`
  THEN  Auto)

---

Home Index