proposition: Lemma find_spec m x e {Hm:Ok m} : find x m = Some e <-> MapsTo x e m.
proof: Proof. unfold P.MapsTo. induction m as [ | (k,v) m IH]; simpl. - split; inversion 1. - rewrite InA_cons. change (eqke (x,e) (k,v)) with (K.eq x k /\ e = v). inversion_clear Hm. dec. + setoid_replace (Some v = Some e) with (v = e) by (split; congruence). intuition. elim H. apply InA_eqk with (x,e); auto. + rewrite IH; intuition. Qed.
imports: Coq(EqualitiesFacts)