proposition: Lemma Sort_Inf_NotIn : forall l k e, Sort l -> Inf (k,e) l -> ~In k l.
proof: Proof. intros; red; intros. destruct H1 as [e' H2]. elim (@ltk_not_eqk (k,e) (k,e')). eapply Sort_Inf_In; eauto with smtcoq_array. red; simpl; auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance