proposition: Lemma for_all_remove_inv : ∀ (m : M.t elt) (k : M.key), P.for_all P (M.remove k m) = true → ~ M.In k m → P.for_all P m = true.
proof: Proof. intros. apply P.for_all_iff; trivial; intros. eapply P.for_all_iff in H. - exact H. - exact P_Proper. - simplify_maps. split; trivial. unfold not; intros. rewrite <- H3 in H1. contradiction H0. apply in_mapsto_iff. exists e. assumption. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts