proposition: Lemma lift_int_typ : forall (y : Int_K) (T : term) (k : nat) (ipe ipf : intP), TIns _ y k ipe ipf -> int_inv ipf -> forall s : skel, eq_can s (int_typ T ipe s) (int_typ (lift_rec 1 T k) ipf s).
proof: Proof. simple induction T. simpl in |- *; auto with coc core arith datatypes. intros. elim nth_lift_int with y s ipe ipf n k; intros; auto with coc core arith datatypes. simpl in |- *; intros. unfold def_cons, int_cons, ext_ik in |- *. elim cl_term_lift with (class_of_ik y) t k (cls_of_int ipe) (cls_of_int ipf); auto with coc core arith datatypes. elim (cl_term t (cls_of_int ipe)); auto with coc core arith datatypes. case s; simpl in |- *; intros; auto with coc core arith datatypes. apply eq_can_trans with (int_typ (lift_rec 1 t0 (S k)) (TCs _ (iK s0 X1) ipf) s1); auto 10 with coc core arith datatypes. apply ins_in_cls with y; auto with coc core arith datatypes. simpl in |- *; intros. elim cl_term_lift with (class_of_ik y) t k (cls_of_int ipe) (cls_of_int ipf); auto with coc core arith datatypes. elim cl_term_lift with (class_of_ik y) t0 k (cls_of_int ipe) (cls_of_int ipf); auto with coc core arith datatypes. elim (cl_term t0 (cls_of_int ipe)); auto with coc core arith datatypes. intros. generalize (H k ipe ipf H1 H2 (PROD s0 s)). simpl in |- *; intros. apply H3; auto with coc core arith datatypes. apply int_equiv_int_typ. apply int_inv_int_eq_can. apply ins_int_inv with ipf k y; auto with coc core arith datatypes. apply ins_in_cls with y; auto with coc core arith datatypes. apply ins_in_cls with y; auto with coc core arith datatypes. simpl in |- *; intros. case s; simpl in |- *; intros; auto with coc core arith datatypes. unfold def_cons, int_cons, ext_ik in |- *. elim cl_term_lift with (class_of_ik y) t k (cls_of_int ipe) (cls_of_int ipf); auto with coc core arith datatypes. apply eq_can_Pi; auto with coc core arith datatypes. simpl in |- *; intros. replace eq_cand with (eq_can PROP); auto with coc core arith datatypes. pattern (cl_term t (cls_of_int ipe)) at 1 3 in |- *. elim (cl_term t (cls_of_int ipe)); auto with coc core arith datatypes; intros. apply eq_can_trans with (int_typ (lift_rec 1 t0 (S k)) (TCs _ (iK _ X1) ipf) PROP); auto 10 with coc core arith datatypes. apply ins_in_cls with y; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_typ