proposition: Lemma for_all_remove : ∀ (m : M.t elt) (k : M.key), P.for_all P m = true → P.for_all P (M.remove k m) = true.
proof: Proof. intros. apply P.for_all_iff; trivial; intros. apply F.remove_mapsto_iff in H0. eapply P.for_all_iff in H. - exact H. - exact P_Proper. - tauto. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts