proposition: Lemma In_MapsTo : forall A m key, In key m -> exists (value: A), MapsTo key value m.
proof: Proof. intros A m key H; apply in_find_iff in H. destruct (find key m) as [value | ] eqn:eq_option; try rewrite <- find_mapsto_iff in eq_option; intuition eauto. Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils