---

Step * of Lemma member-bag-remove-repeats

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  uiff(x ↓∈ bs;x ↓∈ bag-remove-repeats(eq;bs))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `bag-member-count` [⌜T⌝;⌜eq⌝]⋅ THENA Auto)
   THEN RWW "-1 count-bag-remove-repeats" 0
   THEN Auto
   THEN Try (AutoSplit)
   THEN Try ((SplitOnHypITE -1  THEN Auto))) }

---

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-remove-repeats(eq;bs))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `bag-member-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWW  "-1  count-bag-remove-repeats"  0
  THEN  Auto
  THEN  Try  (AutoSplit)
  THEN  Try  ((SplitOnHypITE  -1    THEN  Auto)))

---

Home Index