proposition: Lemma map_contains_MapsTo env x y f m : Some f = map_contains env x y m → M.MapsTo (x, y) (term_denote env f) (map_expr_denote env m).
proof: Proof. induction m; simpl; intros. - discriminate. - simplify_maps. destruct ((x =? term_denote env t)%N && (y =? term_denote env t0)%N)%bool eqn:?. + inversion_clear H. clear IHm. apply andb_true_iff in Heqb. destruct Heqb. apply N.eqb_eq in H. apply N.eqb_eq in H0. intuition. + right. apply andb_false_iff in Heqb. destruct Heqb; apply N.eqb_neq in H0; intuition. Qed.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt