proposition: Lemma for_all_add : Reflexive eq -> Proper (E.eq ==> eq ==> Logic.eq) f -> forall k m, ~In k m -> forall x, for_all f (add k x m) = f k x && for_all f m.
proof: Proof. intros heq fm k m n x. rewrite for_all_eq. rewrite fold_add; intuition. clear - heq fm. intros k k' kk' x x' xx' b b' bb'. apply for_all_aux_m; intuition. subst x'. refl. apply for_all_aux_transp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)