proposition: Lemma InA_rev : forall p m, InA p (rev m) <-> InA p m.
proof: Proof. intros; do 2 rewrite InA_alt. split; intros (y,H); exists y; intuition. - rewrite In_rev; auto. - rewrite <- In_rev; auto. Qed.
imports: List Sorted Setoid Basics Morphisms