`∀[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k1,k2:ℤ]. ∀[v:Value].`
`  (int-decr-map-find(k1;int-decr-map-add(k2;v;m))`
`  = if (k1 =z k2) ∧b (¬bint-decr-map-inDom(k2;m)) then inl v else int-decr-map-find(k1;m) fi `
`  ∈ (Value?))`

Proof

Definitions occuring in Statement :  int-decr-map-add: `int-decr-map-add(k;v;m)` int-decr-map-inDom: `int-decr-map-inDom(k;m)` int-decr-map-find: `int-decr-map-find(k;m)` int-decr-map-type: `int-decr-map-type(Value)` band: `p ∧b q` bnot: `¬bb` ifthenelse: `if b then t else f fi ` eq_int: `(i =z j)` uall: `∀[x:A]. B[x]` unit: `Unit` inl: `inl x` union: `left + right` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Lemmas :  list_ind_nil_lemma list_ind_cons_lemma value-type-has-value int-value-type subtract_wf bool_cases_sqequal eq_int_wf sqequal-tt-to-assert assert_of_eq_int sqequal-ff-to-assert neg_assert_of_eq_int lt_int_wf assert_of_lt_int it_wf less_than_wf insert-combine-cons int-decr-map-inDom_wf l-ordered_wf gt_wf find-combine-cons int-decr-map-inDom-prop2 l_all_iff l_member_wf not_wf equal-wf-base-T int_subtype_base cons_member unit_wf2 or_wf equal_wf l-ordered-cons find-combine_wf int-decr-map-inDom-cons subtype_base_sq bool_wf bool_subtype_base iff_imp_equal_bool eqtt_to_assert bnot_wf bfalse_wf equal-wf-base assert_wf false_wf iff_transitivity iff_weakening_uiff assert_of_band assert_of_bnot assert_elim btrue_neq_bfalse iff_wf
\mforall{}[Value:Type].  \mforall{}[m:int-decr-map-type(Value)].  \mforall{}[k1,k2:\mBbbZ{}].  \mforall{}[v:Value].