`∀[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`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` int-decr-map-type: `int-decr-map-type(Value)` all: `∀x:A. B[x]` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` not: `¬A` top: `Top` and: `P ∧ Q` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` pi1: `fst(t)` so_apply: `x[s1;s2]` gt: `i > j` subtype_rel: `A ⊆r B` or: `P ∨ Q` cons: `[a / b]` colength: `colength(L)` guard: `{T}` decidable: `Dec(P)` nil: `[]` it: `⋅` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` int-decr-map-find: `int-decr-map-find(k;m)` int-decr-map-add: `int-decr-map-add(k;v;m)` find-combine: `find-combine(cmp;l)` list_ind: list_ind insert-combine: `insert-combine(cmp;f;x;l)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` has-value: `(a)↓` ifthenelse: `if b then t else f fi ` btrue: `tt` pi2: `snd(t)` uiff: `uiff(P;Q)` band: `p ∧b q` bnot: `¬bb` int-decr-map-inDom: `int-decr-map-inDom(k;m)` isl: `isl(x)` bfalse: `ff` nequal: `a ≠ b ∈ T ` int-minus-comparison: `int-minus-comparison(f)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` assert: `↑b` true: `True` le: `A ≤ B` bool: `𝔹` unit: `Unit`

Latex:
\mforall{}[Value:Type].  \mforall{}[m:int-decr-map-type(Value)].  \mforall{}[k1,k2:\mBbbZ{}].  \mforall{}[v:Value].