proposition: Lemma findA_rev : forall l k, NoDupA eqk l -> findA (eqb k) l = findA (eqb k) (rev l).
proof: Proof. intros. case_eq (findA (eqb k) l). - intros. symmetry. unfold eqb. rewrite <- findA_NoDupA, InA_rev, findA_NoDupA by (eauto using NoDupA_rev with *); eauto. - case_eq (findA (eqb k) (rev l)); auto. intros e. unfold eqb. rewrite <- findA_NoDupA, InA_rev, findA_NoDupA by (eauto using NoDupA_rev with *). intro Eq; rewrite Eq; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface