proposition: Lemma Sort_Inf_NotIn : forall l k e, Sort l -> Inf (k,e) l -> ~In k l.
proof: Proof. intros l k e H H0; red; intros H1. destruct H1 as [e' H2]. elim (@ltk_not_eqk (k,e) (k,e')). - eapply Sort_Inf_In; eauto with ordered_type. - red; simpl; auto with ordered_type. Qed.
imports: SetoidList Morphisms OrdersTac