proposition: Lemma Ered_sort_mem2 : forall (t : term) (s : sort), Ered t (Srt s) -> mem_sort2 s t.
proof: Proof. intros. pattern t in |- *. apply Ered1_Ered_ind with (Srt s); auto with ecoc coc core arith sets. do 4 intro. elim H0; intros. elim mem_sort2_subst with M0 N 0 s; intros; auto with ecoc coc core arith sets. inversion H2; auto with ecoc. inversion H4; auto with ecoc. inversion H4; auto with ecoc. inversion H4; auto with ecoc. inversion H4; auto with ecoc. inversion H4; auto with ecoc. inversion H4; auto with ecoc. Qed.
imports: Termes Conv