---

Step * of Lemma binary_map_case_E_reduce_lemma

∀F,E:Top.  (binary_map_case(bm_E();E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ~ E)
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `binary_map_case` 0
   THEN Unfold `binary_map_ind` 0
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:


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


By

((UnivCD  THENA  Auto)
  THEN  Unfold  `binary\_map\_case`  0
  THEN  Unfold  `binary\_map\_ind`  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index