---

Step * of Lemma bm_E_wf

∀[T,Key:Type].  (bm_E() ∈ binary_map(T;Key))
BY
{ DepprodCoDatatypeConstructorWf `binary_map_size` }

---

Latex:

---

Latex:
\mforall{}[T,Key:Type].    (bm\_E()  \mmember{}  binary\_map(T;Key))


By

---

Latex:
DepprodCoDatatypeConstructorWf  `binary\_map\_size`

---

Home Index