proposition: Lemma type_kind_not_conv : forall e t T, typ e t T -> typ e t (Srt kind) -> T = Srt kind.
proof: Proof. intros. elim type_case with e t T; intros; auto with coc core arith datatypes. elim H1; intros. elim inv_typ_conv_kind with e T (Srt x); auto with coc core arith datatypes. apply typ_unique with e t; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList