proposition: Lemma inv_typ_conv_kind : forall e t T, conv t (Srt kind) -> ~ typ e t T.
proof: Proof. intros. apply typ_mem_kind. apply red_sort_mem. elim church_rosser with t (Srt kind); intros; auto with coc core arith datatypes. rewrite (red_normal (Srt kind) x); auto with coc core arith datatypes. red in |- *; red in |- *; intros. inversion_clear H2. Qed.
imports: Termes Conv MyList