proposition: Lemma foldkeys_init m i i' : eqA i i' -> eqA (foldkeys m i) (foldkeys m i').
proof: Proof. Proof using Hf. intros Hi. apply fold_rel with (R:=eqA); auto. intros. now apply Hf. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)