proposition: Lemma inv_Etyp_Econv_kind : forall (e : env) (t T : term), Econv t (Srt kind) -> ~ Etyp e t T.
proof: Proof. intros. apply Etyp_mem_kind. apply Ered_sort_mem. elim Econv_church_rosser with t (Srt kind); intros; auto with ecoc coc core arith datatypes. rewrite (Ered_Enormal (Srt kind) x); auto with ecoc coc core arith datatypes. red in |- *; red in |- *; intros. inversion_clear H2. Qed.
imports: Termes Conv Ered MyList Types