proposition: Lemma Ered1_sort_mem : forall (t : term) (s : sort), Ered1 t (Srt s) -> mem_sort s t.
proof: Proof. intros. inversion H. elim mem_sort_subst with M N 0 s; intros; auto with coc core arith sets. unfold subst in H2; rewrite H2. auto with coc. Qed.
imports: Termes Conv