---

Step * of Lemma bm_empty_wf

∀[T,Key:Type].  (bm_empty() ∈ binary-map(T;Key))
BY
{ (Auto THEN RepUR ``bm_empty binary-map`` 0 THEN MemTypeCD THEN Auto THEN RepUR ``bm_cnt_prop`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,Key:Type].    (bm\_empty()  \mmember{}  binary-map(T;Key))


By

---

Latex:
(Auto
  THEN  RepUR  ``bm\_empty  binary-map``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepUR  ``bm\_cnt\_prop``  0
  THEN  Auto)

---

Home Index