proposition: Lemma MapsTo_remove : forall {av} k k' v (m: t av), MapsTo k v (remove k' m) -> MapsTo k v m.
proof: Proof. intros * H; map_iff_in H. intuition eauto using MapsTo_In. Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils