---

Step * of Lemma bm_map_wf

∀[T,Key:Type]. ∀[f:T ⟶ T]. ∀[m:binary-map(T;Key)].  (bm_map(f;m) ∈ binary-map(T;Key))
BY
{ ProveWfLemma }

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index