---

Step * of Lemma bag-size-cons

∀[b:bag(Top)]. ∀[x:Top].  (#(x.b) ~ 1 + #(b))
BY
{ (Auto THEN RepUR ``bag-size cons-bag`` 0 THEN Try (Fold `bag-size` 0⋅) THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[b:bag(Top)].  \mforall{}[x:Top].    (\#(x.b)  \msim{}  1  +  \#(b))


By

---

Latex:
(Auto  THEN  RepUR  ``bag-size  cons-bag``  0  THEN  Try  (Fold  `bag-size`  0\mcdot{})  THEN  Auto')

---

Home Index