---

Step * of Lemma binary_map_case_wf

∀[X,T,Key:Type]. ∀[x:binary_map(T;Key)]. ∀[E:X]. ∀[F:key:Key
                                                     ─→ value:T
                                                     ─→ cnt:ℤ
                                                     ─→ left:binary_map(T;Key)
                                                     ─→ right:binary_map(T;Key)
                                                     ─→ X].
  (binary_map_case(x;E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ∈ X)
BY
{ Auto }

---

Latex:


\mforall{}[X,T,Key:Type].  \mforall{}[x:binary\_map(T;Key)].  \mforall{}[E:X].  \mforall{}[F:key:Key
                                                                                                          {}\mrightarrow{}  value:T
                                                                                                          {}\mrightarrow{}  cnt:\mBbbZ{}
                                                                                                          {}\mrightarrow{}  left:binary\_map(T;Key)
                                                                                                          {}\mrightarrow{}  right:binary\_map(T;Key)
                                                                                                          {}\mrightarrow{}  X].
    (binary\_map\_case(x;E;key,value,cnt,left,right.F[key;value;cnt;left;right])  \mmember{}  X)


By

Auto

---

Home Index