---

Step * of Lemma bm_numItems_E_reduce_lemma

bm_numItems(bm_E()) ~ 0
BY
{ ((UnivCD THENA Auto) THEN Unfold `bm_numItems` 0 THEN Reduce 0 THEN Auto) }

---

Latex:


bm\_numItems(bm\_E())  \msim{}  0


By

((UnivCD  THENA  Auto)  THEN  Unfold  `bm\_numItems`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index