proposition: Lemma filter_idempotent : ∀ elt (m : M.t elt) P, Proper (E.eq ==> eq ==> eq) P → M.Equal (P.filter P (P.filter P m)) (P.filter P m).
proof: Proof. intros. unfold P.filter. apply P.fold_rec; intros. intro k. apply P.elements_Empty in H0. symmetry; rewrite F.elements_o, H0. symmetry; rewrite F.elements_o, P.elements_empty. reflexivity. pose proof (P.filter_iff H). apply H4 in H0; clear H4. rewrite (proj2 H0). rewrite H3. unfold P.Add in H2. symmetry. exact H2. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts