proposition: Theorem type_case : forall e t T, typ e t T -> (exists s : sort, typ e T (Srt s)) \/ T = Srt kind.
proof: Proof. simple induction 1; intros; auto with coc core arith datatypes. left. elim wf_sort_lift with v e0 t0; auto with coc core arith datatypes; intros. exists x; auto with coc core arith datatypes. left. exists s2. apply type_prod with s1; auto with coc core arith datatypes. left. elim H3; intros. elim H4; intros. apply inv_typ_prod with e0 V Ur (Srt x); auto with coc core arith datatypes; intros. exists s2. replace (Srt s2) with (subst v (Srt s2)); auto with coc core arith datatypes. apply substitution with V; auto with coc core arith datatypes. discriminate H4. case s2; auto with coc core arith datatypes. left. exists kind. apply type_prop. apply typ_wf with T0 (Srt s1); auto with coc core arith datatypes. left. exists kind. apply type_set. apply typ_wf with T0 (Srt s1); auto with coc core arith datatypes. left. exists s; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList