proposition: Lemma foldkeys_commutes i m k : ~In k m -> eqA (foldkeys m (f k i)) (f k (foldkeys m i)).
proof: Proof. Proof using st Hf'. intros NI. apply fold_rel with (R:= fun a b => eqA a (f k b)); auto. - reflexivity. - intros k' e' b a Hm K. set (g := fun _ _ => _) in Hf'. change (f k') with (g k' e'). change (f k) with (g k e'). 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)