proposition: Lemma Sort_In_cons_2 l p q : Sort (p::l) -> InA eqk q (p::l) -> ltk p q \/ eqk p q.
proof: Proof. intros; invlist InA; auto with relations. left; apply Sort_In_cons_1 with l; auto with relations. Qed.
imports: RelationPairs SetoidList Orders EqualitiesFacts