---

Step * of Lemma bag-count-ap-map

∀[T1,T2:Type]. ∀[f:T1 ⟶ T2]. ∀[eq1:EqDecider(T1)]. ∀[eq2:EqDecider(T2)]. ∀[x:T1]. ∀[bs:bag(T1)].
  (#f x in bag-map(f;bs)) ~ (#x in bs) supposing Inj(T1;T2;f)
BY
{ (Auto
   THEN (RWO "bag-count-sqequal" 0 THENA Auto)
   THEN (RWW "bag-filter-map bag-size-map" 0⋅ THEN Auto)
   THEN (RepeatFor 2 ((EqCD THEN Auto))
         THEN RepUR ``so_apply`` 0
         THEN (BLemma `iff_imp_equal_bool` THENA Auto)
         THEN RW assert_pushdownC 0
         THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[f:T1  {}\mrightarrow{}  T2].  \mforall{}[eq1:EqDecider(T1)].  \mforall{}[eq2:EqDecider(T2)].  \mforall{}[x:T1].  \mforall{}[bs:bag(T1)].
    (\#f  x  in  bag-map(f;bs))  \msim{}  (\#x  in  bs)  supposing  Inj(T1;T2;f)


By

---

Latex:
(Auto
  THEN  (RWO  "bag-count-sqequal"  0  THENA  Auto)
  THEN  (RWW  "bag-filter-map  bag-size-map"  0\mcdot{}  THEN  Auto)
  THEN  (RepeatFor  2  ((EqCD  THEN  Auto))
              THEN  RepUR  ``so\_apply``  0
              THEN  (BLemma  `iff\_imp\_equal\_bool`  THENA  Auto)
              THEN  RW  assert\_pushdownC  0
              THEN  Auto)\mcdot{})

---

Home Index