proposition: Lemma SortA_InfA_InA : forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
proof: Proof. intros l; induction l as [|a l IHl]. - intros x a **. inv. - intros x a0 **. inv. + setoid_replace x with a; auto. + eauto. Qed.
imports: List Sorted Setoid Basics Morphisms