---

Step * 2 of Lemma bag-monad_wf


1. T : Type
2. m : (λT.bag(T)) T
⊢ ((λba,f. ⋃x∈ba.f x) m (λx.{x})) = m ∈ ((λT.bag(T)) T)
BY
{ All Reduce THEN RWO "bag-combine-single-right" 0 THEN Auto⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  m  :  (\mlambda{}T.bag(T))  T
\mvdash{}  ((\mlambda{}ba,f.  \mcup{}x\mmember{}ba.f  x)  m  (\mlambda{}x.\{x\}))  =  m


By

---

Latex:
All  Reduce  THEN  RWO  "bag-combine-single-right"  0  THEN  Auto\mcdot{}

---

Home Index