---

Step * of Lemma bm_T_wf

∀[T,Key:Type]. ∀[key:Key]. ∀[value:T]. ∀[cnt:ℤ]. ∀[left,right:binary_map(T;Key)].
  (bm_T(key;value;cnt;left;right) ∈ binary_map(T;Key))
BY
{ DepprodCoDatatypeConstructorWf `binary_map_size` }

---

Latex:

---

Latex:
\mforall{}[T,Key:Type].  \mforall{}[key:Key].  \mforall{}[value:T].  \mforall{}[cnt:\mBbbZ{}].  \mforall{}[left,right:binary\_map(T;Key)].
    (bm\_T(key;value;cnt;left;right)  \mmember{}  binary\_map(T;Key))


By

---

Latex:
DepprodCoDatatypeConstructorWf  `binary\_map\_size`

---

Home Index