proposition: Lemma InA_eqke_eqk k k' e e' l : K.eq k k' -> InA eqke (k,e) l -> InA eqk (k',e') l.
proof: Proof. intros Hk. rewrite 2 InA_alt. intros ((k'',e'') & (Hk'',He'') & H); simpl in *; subst e''. exists (k'',e); split; auto. compute. now transitivity k. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)