---

Step * of Lemma binary_map_case_E

∀[E,F:Top].  (binary_map_case(bm_E();E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ~ E)
BY
{ (Reduce 0 THEN Auto) }

---

Latex:


\mforall{}[E,F:Top].    (binary\_map\_case(bm\_E();E;key,value,cnt,left,right.F[key;value;cnt;left;right])  \msim{}  E)


By

(Reduce  0  THEN  Auto)

---

Home Index