proposition: Lemma fold_commutes : forall i s x, eqA (fold f s (f x i)) (f x (fold f s i)).
proof: Proof. intros. apply fold_rel with (R:=fun u v => eqA u (f x v)); intros. - reflexivity. - transitivity (f x0 (f x b)); auto. apply Comp; auto. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide