proposition: Lemma class_knd : forall (e : env) (t T : term), typ e t T -> T = Srt kind -> cl_term t (class_env e) = Knd (cv_skel (cl_term t (class_env e))).
proof: Proof. simple induction 1; intros. simpl in |- *; auto with coc core arith datatypes. simpl in |- *; auto with coc core arith datatypes. elim H1; intros. elim item_trunc with term v e0 x; auto with coc core arith datatypes; intros. elim wf_sort with v e0 x0 x; auto with coc core arith datatypes; intros. elim inv_typ_kind with e0 (Srt x1). elim H2. rewrite H3. replace (Srt x1) with (lift (S v) (Srt x1)); auto with coc core arith datatypes. apply thinning_n with x0; auto with coc core arith datatypes. discriminate H6. elim type_case with e0 u (Prod V Ur); auto with coc core arith datatypes; intros. inversion_clear H5. apply inv_typ_prod with e0 V Ur (Srt x); auto with coc core arith datatypes. intros. elim inv_typ_kind with e0 (Srt s2); auto with coc core arith datatypes. elim H4. 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 H5. simpl in H3. simpl in |- *. rewrite H3; auto with coc core arith datatypes. elim (cl_term T0 (class_env e0)); auto with coc core arith datatypes. elim inv_typ_kind with e0 (Srt s); auto with coc core arith datatypes. elim H5; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType