proposition: Lemma for_all_add_true : ∀ (m : M.t elt) k e, ~ M.In k m → (P.for_all P (M.add k e m) = true <-> P.for_all P m = true /\ P k e = true).
proof: Proof. unfold P.for_all. remember (fun _ _ _ => _) as f. assert (Proper (E.eq ==> eq ==> eq ==> eq) f). relational. rewrite H; reflexivity. assert (P.transpose_neqkey eq f). rewrite Heqf; intros ??????. destruct (P k e), (P k' e'); auto. assert (Proper (E.eq ==> eq ==> eq --> flip eq) f). unfold flip; relational. rewrite H1; reflexivity. assert (P.transpose_neqkey (flip eq) f). unfold flip; rewrite Heqf; intros ??????. destruct (P k e), (P k' e'); auto. split; intros. rewrite P.fold_Add with (k:=k) (e:=e) (m1:=m) in H4; eauto. rewrite Heqf in *. destruct (P k e); now firstorder. constructor. rewrite P.fold_Add with (k:=k) (e:=e) (m1:=m); eauto. rewrite Heqf in *. destruct (P k e); now firstorder. constructor. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts