---

Step * of Lemma single-bag_wf

∀T:Type. ∀x:T.  ({x} ∈ bag(T))
BY
{ (ProveWfLemma THEN DoSubsume THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}x:T.    (\{x\}  \mmember{}  bag(T))


By

---

Latex:
(ProveWfLemma  THEN  DoSubsume  THEN  Auto)

---

Home Index