---

Step * of Lemma bag-deq-member-bag-diff

∀[T:Type]. ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).  (bag-deq-member(eq;x;bs) ~ isl(bag-diff(eq;bs;{x})))
BY
{ (InstLemma `bag-member-bag-diff` []
   THEN (RepeatFor 4 (ParallelLast') THEN Auto)
   THEN BLemma `iff_imp_equal_bool`
   THEN Auto
   THEN (All (RWO "assert-bag-deq-member") THENA Auto)
   THEN ThinTrivial
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}bs:bag(T).    (bag-deq-member(eq;x;bs)  \msim{}  isl(bag-diff(eq;bs;\{x\})))


By

---

Latex:
(InstLemma  `bag-member-bag-diff`  []
  THEN  (RepeatFor  4  (ParallelLast')  THEN  Auto)
  THEN  BLemma  `iff\_imp\_equal\_bool`
  THEN  Auto
  THEN  (All  (RWO  "assert-bag-deq-member")  THENA  Auto)
  THEN  ThinTrivial
  THEN  Auto)

---

Home Index