proposition: Lemma skel_sound : forall (e : env) (t T : term), typ e t T -> cv_skel (cl_term T (class_env e)) = typ_skel (cl_term t (class_env e)).
proof: Proof. simple induction 1; intros; auto with coc core arith datatypes. inversion_clear H1. rewrite H2. simpl in |- *. clear H2 t0. elim H3; simpl in |- *; intros. unfold lift in |- *. elim cl_term_lift with (cl_term x (class_env l)) x 0 (class_env l) (TCs class (cl_term x (class_env l)) (class_env l)); auto with coc core arith datatypes. elim (cl_term x (class_env l)); auto with coc core arith datatypes. rewrite simpl_lift. unfold lift at 1 in |- *. elim cl_term_lift with (cl_term y (class_env l)) (lift (S n) x) 0 (class_env l) (TCs class (cl_term y (class_env l)) (class_env l)); auto with coc core arith datatypes. simpl in |- *. replace (TCs class (cl_term T0 (class_env e0)) (class_env e0)) with (class_env (T0 :: e0)); auto with coc core arith datatypes. rewrite (commut_case _ _ cv_skel) with (bK := fun s => match cl_term T0 (class_env e0) with | Trm => Knd s | Typ _ => Knd s | Knd s0 => Knd (PROD s0 s) end). rewrite (commut_case _ _ typ_skel) with (bT := fun s => match cl_term T0 (class_env e0) with | Trm => Typ s | Typ _ => Typ s | Knd s0 => Typ (PROD s0 s) end) (bK := fun s : skel => Knd PROP). simpl in |- *. replace (TCs class (cl_term T0 (class_env e0)) (class_env e0)) with (class_env (T0 :: e0)); auto with coc core arith datatypes. pattern (cl_term M (class_env (T0 :: e0))) at 1, (cl_term U (class_env (T0 :: e0))) at 1 in |- *. elim cl_term_sound with (T0 :: e0) M U (Srt s2); intros; auto with coc core arith datatypes. rewrite (commut_case _ _ cv_skel) with (bT := fun s : skel => Knd (cv_skel (cl_term U (class_env (T0 :: e0))))) (bK := fun s => Knd (PROD s (cv_skel (cl_term U (class_env (T0 :: e0)))))). rewrite (commut_case _ _ typ_skel) with (bT := fun s : skel => Typ (typ_skel (cl_term M (class_env (T0 :: e0))))) (bK := fun s => Typ (PROD s (typ_skel (cl_term M (class_env (T0 :: e0)))))). elim (cl_term T0 (class_env e0)); auto with coc core arith datatypes. elim H5; auto with coc core arith datatypes. elim type_case with e0 u (Prod V Ur); intros; auto with coc core arith datatypes. inversion_clear H4. apply inv_typ_prod with e0 V Ur (Srt x); intros; auto with coc core arith datatypes. unfold subst in |- *. generalize H3. cut (adj_cls (cl_term u (class_env e0)) (cl_term (Prod V Ur) (class_env e0))). simpl in |- *. elim cl_term_subst with (cl_term V (class_env e0)) (class_env e0) v Ur 0 (class_env e0) (TCs class (cl_term V (class_env e0)) (class_env e0)); simpl in |- *; auto with coc core arith datatypes. intros. inversion_clear H8. intros. inversion_clear H8. auto with coc core arith datatypes. elim cl_term_sound with e0 v V (Srt s1); simpl in |- *; intros; auto with coc core arith datatypes. rewrite H9. inversion_clear H8; auto with coc core arith datatypes. elim s3; auto with coc core arith datatypes. generalize H9. inversion_clear H8; intros; auto with coc core arith datatypes. simpl in H8. elim H8; auto with coc core arith datatypes. apply cl_term_sound with (Srt s1); auto with coc core arith datatypes. apply cl_term_sound with (Srt x); auto with coc core arith datatypes. discriminate H4. simpl in |- *. simpl in H3. simpl in H1. rewrite (commut_case _ _ typ_skel) with (bK := fun s => match cl_term T0 (class_env e0) with | Trm => Knd s | Typ _ => Knd s | Knd s0 => Knd (PROD s0 s) end). simpl in |- *. elim H3. elim (cl_term U (TCs class (cl_term T0 (class_env e0)) (class_env e0))); auto with coc core arith datatypes. elim (cl_term T0 (class_env e0)); auto with coc core arith datatypes. elim H1. elim cl_term_conv with e0 U V (Srt s) (Srt s); auto with coc core arith datatypes. elim type_case with e0 t0 U; auto with coc core arith datatypes; intros. inversion_clear H5. elim conv_sort with x s; 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 s); auto with coc core arith datatypes. elim H5; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType