proposition: Lemma Sort_In_cons_3 x l k e : Sort ((k,e)::l) -> In x l -> ~O.eq x k.
proof: Proof. intros; invlist sort; red; intros. eapply Sort_Inf_NotIn; eauto using In_eq. Qed.
imports: RelationPairs SetoidList Orders EqualitiesFacts