proposition: Lemma inv_Etyp_kind : forall (e : env) (t : term), ~ Etyp e (Srt kind) t.
proof: Proof. red in |- *; intros. apply Etyp_inversion with e (Srt kind) t; simpl in |- *; auto with coc ecoc core arith datatypes. Qed.
imports: Termes Conv Ered MyList Types