proposition: Lemma for_all_impl : ∀ (P' : M.key → elt → bool) m, P.for_all P m = true → Proper (E.eq ==> eq ==> eq) P' → (∀ k e, P k e = true → P' k e = true) → P.for_all P' m = true.
proof: Proof. intros. apply P.for_all_iff; trivial; intros. eapply P.for_all_iff in H; eauto. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts