---

Step * of Lemma bag-decomp_wf2

∀[T:Type]. ∀[bs:bag(T)].  (bag-decomp(bs) ∈ bag({p:T × bag(T)| bs = ({fst(p)} + (snd(p))) ∈ bag(T)} ))
BY
{ (Auto THEN BLemma `bag-settype` THEN Auto) }

1
1. T : Type
2. bs : bag(T)
3. p : T × bag(T)@i
4. p ↓∈ bag-decomp(bs)@i
⊢ bs = ({fst(p)} + (snd(p))) ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].    (bag-decomp(bs)  \mmember{}  bag(\{p:T  \mtimes{}  bag(T)|  bs  =  (\{fst(p)\}  +  (snd(p)))\}  ))


By

---

Latex:
(Auto  THEN  BLemma  `bag-settype`  THEN  Auto)

---

Home Index