proposition: Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
proof: Proof. intros l; induction l as [|x l' H]; auto. intros H0. inv. constructor; auto. intro. apply (StrictOrder_Irreflexive x). eapply SortA_InfA_InA; eauto. Qed.
imports: List Sorted Setoid Basics Morphisms