proposition: Lemma Sort_Inf_NotIn 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. - repeat red; reflexivity. Qed.
imports: RelationPairs SetoidList Orders EqualitiesFacts