proposition: Lemma MapsTo_NotIn_inv : forall T {k k' v m}, not (In k m) -> @MapsTo T k' v m -> k <> k'.
proof: Proof. intros * ? maps_to; destruct (E.eq_dec k k'); subst; apply MapsTo_In in maps_to; msubst; congruence. Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils