proposition: Lemma MapsTo_add_eq_inv : forall T {k v v' m}, @MapsTo T k v' (add k v m) -> v = v'.
proof: Proof. intros *. map_iff; intros. intuition. exfalso; eauto using E.eq_refl. Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils