proposition: Lemma for_all_remove_inv_2 : ∀ (m : M.t elt) (k : M.key), P.for_all P (M.remove k m) = true → ∀ k' e, M.MapsTo k' e m → ~ E.eq k' k → P k' e = true.
proof: Proof. intros. eapply P.for_all_iff; eauto. simplify_maps. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts