---

Step * 1 of Lemma bag-monad_wf


1. T : Type
2. S : Type
3. x : T
4. f : T ⟶ ((λT.bag(T)) S)@i
⊢ ((λba,f. ⋃x∈ba.f x) ((λx.{x}) x) f) = (f x) ∈ ((λT.bag(T)) S)
BY
{ All Reduce THEN RWO "bag-combine-single-left" 0 THEN Auto⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  S  :  Type
3.  x  :  T
4.  f  :  T  {}\mrightarrow{}  ((\mlambda{}T.bag(T))  S)@i
\mvdash{}  ((\mlambda{}ba,f.  \mcup{}x\mmember{}ba.f  x)  ((\mlambda{}x.\{x\})  x)  f)  =  (f  x)


By

---

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

---

Home Index