---

Step * of Lemma bm_E-wf2

∀[T,Key:Type].  (bm_E() ∈ binary-map(T;Key))
BY
{ (Auto THEN MemTypeCD THEN Reduce 0 THEN Auto) }

---

Latex:


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


By

(Auto  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index