proposition: Lemma red_sort_sort : forall s t, red (Srt s) t -> t <> Srt s -> False.
proof: Proof. simple induction 1; intros; auto with coc core arith sets. apply H1. generalize H2. case P; intros; try discriminate. inversion_clear H4. Qed.
imports: Arith Compare_dec Relations