proposition: Lemma filter_add_true_r : ∀ elt k (e : elt) m m' P, Proper (E.eq ==> eq ==> eq) P → ~ M.In (elt:=elt) k m → M.Equal (M.add k e (P.filter P m)) m' → P k e = true → M.Equal (P.filter P (M.add k e m)) m'.
proof: Proof. intros. rewrite <- H1; clear H1. apply F.Equal_mapsto_iff; split; intros. simplify_maps. simplify_maps. simplify_maps. simplify_maps. right; intuition. simplify_maps. simplify_maps. simplify_maps. intuition. rewrite <- H3. assumption. simplify_maps. simplify_maps. intuition. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts