proposition: Lemma remove_trickle : forall {elt : Type} (k k' : M.key) (v' : elt) (m : M.t elt), k = k' -> Equal (remove k ([k' |> v']::m)) (remove k m).
proof: Proof. intros. rewrite Equal_mapsto_iff; intros; map_iff. intuition (subst; congruence). Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils