proposition: Lemma Etyp_mem_kind : forall (e : env) (t T : term), mem_sort kind t -> ~ Etyp e t T.
proof: Proof. red in |- *; intros. apply Etyp_inversion with e t T; auto with coc core arith datatypes. generalize e T. clear H0. elim H; simpl in |- *; auto with coc core arith datatypes; intros. apply Etyp_inversion with e0 u (Srt s1); auto with coc core arith datatypes. apply Etyp_inversion with (u :: e0) v (Srt s2); auto with coc core arith datatypes. apply Etyp_inversion with e0 u (Srt s1); auto with coc core arith datatypes. apply Etyp_inversion with (u :: e0) v U; auto with coc core arith datatypes. apply Etyp_inversion with e0 u (Prod V Ur); auto with coc core arith datatypes. apply Etyp_inversion with e0 v V; auto with coc core arith datatypes. Qed.
imports: Termes Conv Ered MyList Types