---

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:

---

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

---

Latex:
Auto

---

Home Index