proposition: Lemma filter_empty : ∀ elt f m, Proper (E.eq ==> eq ==> eq) f → M.Empty (elt:=elt) m → M.Equal (P.filter f m) m.
proof: Proof. intros. apply F.Equal_mapsto_iff; split; intros. simplify_maps. simplify_maps. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts