---

Step * of Lemma bm_singleton_wf

∀[T,Key:Type]. ∀[x:Key]. ∀[v:T].  (bm_singleton(x;v) ∈ binary-map(T;Key))
BY
{ (ProveWfLemma THEN MemTypeCD THEN Auto THEN BLemma `bm_cnt_prop_T` THEN Reduce 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Auto  THEN  BLemma  `bm\_cnt\_prop\_T`  THEN  Reduce  0  THEN  Auto)

---

Home Index