proposition: Lemma fold_commutes i m k e : ~In k m -> eqA (fold f m (f k e i)) (f k e (fold f m i)).
proof: Proof. Proof using st Hf'. intros NI. apply fold_rel with (R:= fun a b => eqA a (f k e b)); auto. - reflexivity. - intros k' e' b a Hm K. apply Hf' with a; try easy. contradict NI; rewrite <- NI. now exists e'. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)