---

Step * of Lemma binary_map_size_wf

∀[T,Key:Type]. ∀[p:binary_map(T;Key)].  (binary_map_size(p) ∈ ℕ)
BY
{ ProveCoSizeWf2 `binary_mapco_size` }

---

Latex:

---

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


By

---

Latex:
ProveCoSizeWf2  `binary\_mapco\_size`

---

Home Index