proposition: Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
proof: Proof. inversion 1; intros; eapply Sort_Inf_In; eauto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance