proposition: Lemma red_sort_mem : forall t s, red t (Srt s) -> mem_sort s t.
proof: Proof. intros. pattern t in |- *. apply red1_red_ind with (Srt s); auto with coc core arith sets. do 4 intro. elim H0; intros. elim mem_sort_subst with M0 N 0 s; intros; auto with coc core arith sets. inversion_clear H4; auto with coc core arith sets. inversion_clear H4; auto with coc core arith sets. inversion_clear H4; auto with coc core arith sets. inversion_clear H4; auto with coc core arith sets. inversion_clear H4; auto with coc core arith sets. inversion_clear H4; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations