proposition: Lemma findA_rev l k : NoDupA eqk l -> findA (eqb k) l = findA (eqb k) (rev l).
proof: Proof. intros H. apply eq_option_alt. intros e. unfold eqb. rewrite <- !findA_NoDupA, InA_rev; eauto with map. reflexivity. change (NoDupA eqk (rev l)). apply NoDupA_rev; auto using eqk_equiv. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)