---

Step * of Lemma bag-deq-member_wf

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[b:bag(A)]. ∀[x:A].  (bag-deq-member(eq;x;b) ∈ 𝔹)
BY
{ ((UnivCD THENA Auto)
   THEN BagD (-2)
   THEN Unfold `bag-deq-member` 0
   THEN (BLemma `iff_imp_equal_bool` THEN Auto)
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN FLemma `member-permutation` [-2]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[b:bag(A)].  \mforall{}[x:A].    (bag-deq-member(eq;x;b)  \mmember{}  \mBbbB{})


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  BagD  (-2)
  THEN  Unfold  `bag-deq-member`  0
  THEN  (BLemma  `iff\_imp\_equal\_bool`  THEN  Auto)
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  FLemma  `member-permutation`  [-2]
  THEN  Auto)

---

Home Index