proposition: Lemma fold_commutes : forall i m k e, ~In k m -> eqA (fold f m (f k e i)) (f k e (fold f m i)).
proof: Proof. intros i m k e Hnotin. apply fold_rel with (R:= fun a b => eqA a (f k e b)); auto. - reflexivity. - intros. transitivity (f k0 e0 (f k e b)). + apply Comp; auto. + apply Tra; auto. contradict Hnotin; rewrite <- Hnotin; exists e0; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface