proposition: Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l).
proof: Proof. intros l; induction l. - simpl; auto. - simpl; intros. inv. apply NoDupA_app; auto. + constructor; auto. intro; inv. + intros x. rewrite InA_alt. intros (x1,(H2,H3)). intro; inv. match goal with H0 : ~ InA _ _ |- _ => destruct H0 end. match goal with H4 : eqA x ?x' |- InA ?x' _ => rewrite <- H4, H2 end. apply In_InA. rewrite In_rev; auto. Qed.
imports: List Sorted Setoid Basics Morphisms