---

Step * of Lemma bag-separate_wf

∀[A,B:Type]. ∀[bs:bag(A + B)].  (bag-separate(bs) ∈ bag(A) × bag(B))
BY
{ (ProveWfLemma THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[bs:bag(A  +  B)].    (bag-separate(bs)  \mmember{}  bag(A)  \mtimes{}  bag(B))


By

---

Latex:
(ProveWfLemma  THEN  All  Reduce  THEN  Auto)

---

Home Index