proposition: Lemma class_typ : forall (e : env) (t T : term), typ e t T -> typ e T (Srt kind) -> cl_term t (class_env e) = Typ (typ_skel (cl_term t (class_env e))).
proof: Proof. simple induction 1; intros. elim inv_typ_kind with e0 (Srt kind); auto with coc core arith datatypes. elim inv_typ_kind with e0 (Srt kind); auto with coc core arith datatypes. elim H1; intros. simpl in |- *. elim item_trunc with term v e0 x; auto with coc core arith datatypes; intros. elim nth_class_env with x e0 x0 v; auto with coc core arith datatypes. elim cl_trunc with (S v) (class_env e0) (class_env x0) x; auto with coc core arith datatypes. elim H3. rewrite (class_knd e0 t0 (Srt kind)); auto with coc core arith datatypes. simpl in |- *. simpl in H5. rewrite H5. elim (cl_term T0 (class_env e0)); intros; auto with coc core arith datatypes. apply inv_typ_prod with e0 T0 U (Srt kind); intros; auto with coc core arith datatypes. elim conv_sort with s3 kind; auto with coc core arith datatypes. simpl in |- *. elim type_case with e0 u (Prod V Ur); auto with coc core arith datatypes; intros. inversion_clear H5. rewrite H3. case (typ_skel (cl_term u (class_env e0))); auto with coc core arith datatypes. elim (cl_term v (class_env e0)); auto with coc core arith datatypes. apply inv_typ_prod with e0 V Ur (Srt x); intros; auto with coc core arith datatypes. apply type_prod with s1; auto with coc core arith datatypes. elim conv_sort with s2 kind; auto with coc core arith datatypes. apply typ_unique with e0 (subst v Ur); auto with coc core arith datatypes. 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 |- *. simpl in H3. rewrite H3; auto with coc core arith datatypes. replace (Srt s2) with (lift 1 (Srt s2)); auto with coc core arith datatypes. replace (Srt kind) with (lift 1 (Srt kind)); auto with coc core arith datatypes. apply thinning; auto with coc core arith datatypes. apply wf_var with s1; auto with coc core arith datatypes. apply H1. elim type_case with e0 t0 U; auto with coc core arith datatypes; intros. inversion_clear H6. elim conv_sort with x kind; auto with coc core arith datatypes. apply typ_conv_conv with e0 U V; auto with coc core arith datatypes. elim inv_typ_conv_kind with e0 V (Srt kind); auto with coc core arith datatypes. elim H6; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType