---

Step * of Lemma binary_mapco_size_wf

∀[T,Key:Type]. ∀[p:binary_mapco(T;Key)].  (binary_mapco_size(p) ∈ partial(ℕ))
BY
{ ProveCoSizeWf }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[p:binary\_mapco(T;Key)].    (binary\_mapco\_size(p)  \mmember{}  partial(\mBbbN{}))


By

ProveCoSizeWf

---

Home Index