proposition: Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> ltk e e' \/ eqk e e'.
proof: Proof. inversion_clear 2; auto. left; apply Sort_In_cons_1 with l; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses