---

Step * of Lemma member-bag-to-set

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  uiff(x ↓∈ bs;x ↓∈ bag-to-set(eq;bs))
BY
{ (InstLemma `member-bag-remove-repeats` [] THEN Fold `bag-to-set` (-1) THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].    uiff(x  \mdownarrow{}\mmember{}  bs;x  \mdownarrow{}\mmember{}  bag-to-set(eq;bs))


By

---

Latex:
(InstLemma  `member-bag-remove-repeats`  []  THEN  Fold  `bag-to-set`  (-1)  THEN  Trivial)

---

Home Index