proposition: Lemma subst_int_typ : forall (v : term) (ipg : intP) (i : Int_K), int_var_sound v ipg i -> forall (e : env) (T K : term), typ e T K -> forall (k : nat) (ipe ipf : intP), TIns _ i k ipf ipe -> TTrunc _ k ipf ipg -> cls_of_int ipe = class_env e -> int_inv ipe -> cl_term T (cls_of_int ipe) <> Trm -> eq_can (skel_int T ipe) (int_typ T ipe _) (int_typ (subst_rec v T k) ipf _).
proof: Proof. simple induction 2; intros. simpl in |- *; auto with coc core arith datatypes. simpl in |- *; auto with coc core arith datatypes. unfold subst_rec in |- *. elim (lt_eq_lt_dec k v0); [ intro Hlt_eq | intro Hlt ]. elim Hlt_eq; clear Hlt_eq; [ idtac | intro Heq ]. case v0; [ intro Hlt | intros n Hlt ]. inversion_clear Hlt. unfold pred in |- *. elim nth_lift_int with i (skel_int (Ref (S n)) ipe) ipf ipe n k; auto with coc core arith datatypes. rewrite lift_ref_ge; auto with coc core arith datatypes. generalize H4 H6 H7. elim Heq. clear H4 H6 H7 Heq. elim H3; simpl in |- *; intros. rewrite lift0. unfold skel_int in |- *. simpl in |- *. generalize H7. inversion_clear H; intros; simpl in H9. unfold class_of_ik, typ_skel in |- *. apply extr_eq with (P := fun s c => eq_can s c (int_typ v l s)). generalize H6. inversion_clear H4; intros. inversion_clear H4; auto with coc core arith datatypes. elim H9; auto with coc core arith datatypes. replace (skel_int (Ref (S n)) (TCs Int_K y il)) with (skel_int (Ref n) il); auto with coc core arith datatypes. rewrite simpl_lift. apply eq_can_trans with (int_typ (lift n v) l (skel_int (Ref n) il)). apply H6; auto with coc core arith datatypes. inversion_clear H7; auto with coc core arith datatypes. inversion_clear H8; auto with coc core arith datatypes. inversion_clear H8. apply int_equiv_int_typ. apply int_inv_int_eq_can. apply ins_int_inv with il n i; auto with coc core arith datatypes. unfold lift at 2 in |- *. apply lift_int_typ with y; auto with coc core arith datatypes. apply ins_int_inv with (TCs _ y il) (S n) i; auto with coc core arith datatypes. elim nth_lift_int with i (skel_int (Ref v0) ipe) ipf ipe v0 k; auto with coc core arith datatypes. rewrite lift_ref_lt; auto with coc core arith datatypes. unfold skel_int in |- *. simpl in |- *. replace (cl_term M (TCs class (cl_term T0 (cls_of_int ipe)) (cls_of_int ipe))) with (Typ (typ_skel (cl_term M (class_env (T0 :: e0))))). unfold def_cons, int_cons, ext_ik in |- *. elim class_subst with (class_of_ik i) (cls_of_int ipg) v T0 k (cls_of_int ipf) (cls_of_int ipe); auto with coc core arith datatypes. generalize H11. simpl in |- *. generalize (refl_equal (cl_term T0 (class_env e0))). rewrite H9. pattern (cl_term T0 (class_env e0)) at 1 in |- *. apply class_typ_ord with s1; auto with coc core arith datatypes; simple induction 1; auto with coc core arith datatypes. simpl in |- *. rewrite H12. replace (typ_skel (cl_term M (TCs class (cl_term T0 (class_env e0)) (class_env e0)))) with (skel_int M (TCs Int_K iT ipe)). intros. apply H6; auto with coc core arith datatypes. simpl in |- *. elim H12. elim skel_sound with e0 T0 (Srt s1); auto with coc core arith datatypes. unfold cls_of_int in |- *; simpl in |- *; elim H9; auto with coc core arith datatypes. unfold cls_of_int in |- *. simpl in |- *. red in |- *; intros; apply H13. elim H12. elim skel_sound with e0 T0 (Srt s1); simpl in |- *; auto with coc core arith datatypes. elim H9. unfold cls_of_int in |- *. rewrite H14. auto with coc core arith datatypes. elim H12. elim skel_sound with e0 T0 (Srt s1); simpl in |- *; auto with coc core arith datatypes. unfold skel_int, cls_of_int in |- *; simpl in |- *; auto with coc core arith datatypes; elim H9; auto with coc core arith datatypes. simpl in |- *. intros. replace (typ_skel (cl_term M (TCs class (Knd (cv_skel (cl_term T0 (class_env e0)))) (class_env e0)))) with (skel_int M (TCs _ (iK _ X2) ipe)). apply eq_can_trans with (int_typ M (TCs _ (iK _ X2) ipe) (skel_int M (TCs _ (iK _ X2) ipe))); auto with coc core arith datatypes. apply H6; auto with coc core arith datatypes. unfold cls_of_int in |- *. simpl in |- *. elim H12. elim H9; auto with coc core arith datatypes. unfold cls_of_int in |- *. simpl in |- *. elim H9. unfold cls_of_int in |- *. red in |- *; intros; apply H13. elim H9. unfold cls_of_int in |- *. rewrite H17; auto with coc core arith datatypes. unfold skel_int in |- *. unfold cls_of_int in |- *. simpl in |- *. elim H9; auto with coc core arith datatypes. apply ins_in_cls with i; auto with coc core arith datatypes. unfold cls_of_int in |- *. elim H8; simpl in |- *; auto with coc core arith datatypes. generalize H11. simpl in |- *. rewrite H9. replace (TCs class (cl_term T0 (class_env e0)) (class_env e0)) with (class_env (T0 :: e0)); auto with coc core arith datatypes. elim class_sound with (T0 :: e0) M U (Srt s2); auto with coc core arith datatypes; intros. elim H12; auto with coc core arith datatypes. elim type_case with e0 u (Prod V Ur); intros; auto with coc core arith datatypes. inversion_clear H10. apply inv_typ_prod with e0 V Ur (Srt x); auto with coc core arith datatypes; intros. unfold skel_int in |- *. simpl in |- *. elim class_subst with (class_of_ik i) (cls_of_int ipg) v u k (cls_of_int ipf) (cls_of_int ipe); auto with coc core arith datatypes. cut (cl_term u (cls_of_int ipe) = Typ (typ_skel (cl_term u (cls_of_int ipe)))). intro. rewrite H14. elim class_subst with (class_of_ik i) (cls_of_int ipg) v v0 k (cls_of_int ipf) (cls_of_int ipe); auto with coc core arith datatypes. rewrite H7. generalize (refl_equal (cl_term v0 (class_env e0))). pattern (cl_term v0 (class_env e0)) at 1, (cl_term V (class_env e0)) in |- *. elim class_sound with e0 v0 V (Srt s1); auto with coc core arith datatypes; intros. elim H15. replace (typ_skel match typ_skel (cl_term u (class_env e0)) with | PROP => Typ (typ_skel (cl_term u (class_env e0))) | PROD _ _ => Typ (typ_skel (cl_term u (class_env e0))) end) with (skel_int u ipe). apply H4; auto with coc core arith datatypes. rewrite H14. discriminate. unfold skel_int in |- *. elim H7. case (typ_skel (cl_term u (cls_of_int ipe))); auto with coc core arith datatypes. elim H15. elim skel_sound with e0 u (Prod V Ur); auto with coc core arith datatypes. cut (cl_term V (class_env e0) = Knd s); intros. cut (cl_term Ur (TCs class (cl_term V (class_env e0)) (class_env e0)) = Knd (cv_skel (cl_term Ur (class_env (V :: e0))))); intros. simpl in |- *. rewrite H17. rewrite H16. simpl in |- *. generalize (H4 k ipe ipf H5 H6 H7 H8). replace (skel_int u ipe) with (PROD s (cv_skel (cl_term Ur (TCs class (cl_term V (class_env e0)) (class_env e0))))). simpl in |- *; intros. apply H18; auto with coc core arith datatypes. rewrite H14. discriminate. replace s with (skel_int v0 ipe). apply H2; auto with coc core arith datatypes. rewrite H7. elim H15. discriminate. unfold skel_int in |- *. rewrite H7. elim H15; simpl in |- *; auto with coc core arith datatypes. apply int_equiv_int_typ. apply int_inv_int_eq_can. apply ins_int_inv with ipe k i; auto with coc core arith datatypes. unfold skel_int in |- *. rewrite H7. elim skel_sound with e0 u (Prod V Ur); auto with coc core arith datatypes. simpl in |- *. rewrite H17. rewrite H16. simpl in |- *; auto with coc core arith datatypes. generalize (class_sound e0 u (Prod V Ur) H3 (Srt x) H11). simpl in |- *. rewrite H16. elim H7. rewrite H14. elim (cl_term Ur (TCs class (Knd s) (cls_of_int ipe))); simpl in |- *; intros; auto with coc core arith datatypes. inversion_clear H17. inversion_clear H17. replace s with (cv_skel (cl_term V (class_env e0))). generalize H15. elim class_sound with e0 v0 V (Srt s1); simpl in |- *; auto with coc core arith datatypes; intros. inversion_clear H16. generalize H15. rewrite (skel_sound e0 v0 V); auto with coc core arith datatypes. elim (cl_term v0 (class_env e0)); simpl in |- *; intros. discriminate H16. injection H16; auto with coc core arith datatypes. discriminate H16. unfold cls_of_int in |- *. elim H5; simpl in |- *; auto with coc core arith datatypes. unfold cls_of_int in |- *. elim H6; simpl in |- *; auto with coc core arith datatypes. generalize H9. rewrite H7. simpl in |- *. elim class_sound with e0 u (Prod V Ur) (Srt x); simpl in |- *; auto with coc core arith datatypes; intros. elim H14; auto with coc core arith datatypes. unfold cls_of_int in |- *. elim H5; simpl in |- *; auto with coc core arith datatypes. unfold cls_of_int in |- *. elim H6; simpl in |- *; auto with coc core arith datatypes. discriminate H10. replace (skel_int (Prod T0 U) ipe) with PROP. simpl; fold Can. elim class_subst with (class_of_ik i) (cls_of_int ipg) v T0 k (cls_of_int ipf) (cls_of_int ipe); auto with coc core arith datatypes. apply eq_can_Pi; simpl in |- *; intros; auto with coc core arith datatypes. replace eq_cand with (eq_can PROP); auto with coc core arith datatypes. replace PROP with (skel_int T0 ipe). apply H2; auto with coc core arith datatypes. rewrite H7. apply class_typ_ord with s1; auto with coc core arith datatypes. discriminate. discriminate. unfold skel_int in |- *. rewrite H7. elim skel_sound with e0 T0 (Srt s1); simpl in |- *; auto with coc core arith datatypes. replace eq_cand with (eq_can PROP); auto with coc core arith datatypes. apply eq_can_trans with (int_typ U (int_cons T0 ipe (cv_skel (cl_term T0 (cls_of_int ipe))) X2) PROP); auto with coc core arith datatypes. apply int_equiv_int_typ. unfold int_cons, ext_ik in |- *. pattern (cl_term T0 (cls_of_int ipe)) at 1 3 in |- *. elim (cl_term T0 (cls_of_int ipe)); auto with coc core arith datatypes. apply int_equiv_int_typ. unfold int_cons, ext_ik in |- *. pattern (cl_term T0 (cls_of_int ipe)) at 1 3 in |- *. elim (cl_term T0 (cls_of_int ipe)); auto with coc core arith datatypes. replace PROP with (skel_int U (int_cons T0 ipe (cv_skel (cl_term T0 (cls_of_int ipe))) X2)). apply H4; auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. elim class_subst with (class_of_ik i) (cls_of_int ipg) v T0 k (cls_of_int ipf) (cls_of_int ipe); auto with coc core arith datatypes. unfold cls_of_int in |- *. elim H5; simpl in |- *; auto with coc core arith datatypes. unfold cls_of_int in |- *. elim H6; simpl in |- *; auto with coc core arith datatypes. unfold int_cons in |- *; auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. unfold cls_of_int at 1 in |- *. simpl in |- *. cut (typ_skel (cl_term T0 (class_env e0)) = PROP). generalize X2. rewrite H7. pattern (cl_term T0 (class_env e0)) in |- *. apply class_typ_ord with s1; simpl in |- *; auto with coc core arith datatypes. intros. rewrite H13. elim H7; auto with coc core arith datatypes. intros. elim H7; auto with coc core arith datatypes. elim skel_sound with e0 T0 (Srt s1); simpl in |- *; auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. pattern (cl_term T0 (cls_of_int ipe)) at 1 in |- *. elim (cl_term T0 (cls_of_int ipe)); auto with coc core arith datatypes. replace (cls_of_int (int_cons T0 ipe (cv_skel (cl_term T0 (cls_of_int ipe))) X2)) with (class_env (T0 :: e0)). apply class_typ_ord with s2; auto with coc core arith datatypes. discriminate. discriminate. unfold cls_of_int, int_cons, ext_ik in |- *. unfold int_cons, ext_ik in |- *. simpl in |- *. rewrite H7. cut (typ_skel (cl_term T0 (class_env e0)) = PROP). generalize X2. unfold cls_of_int in |- *. replace (Tmap Int_K class class_of_ik ipe) with (cls_of_int ipe); auto with coc core arith datatypes. rewrite H7. pattern (cl_term T0 (class_env e0)) in |- *. apply class_typ_ord with s1; simpl in |- *; auto with coc core arith datatypes. intros. rewrite H13; auto with coc core arith datatypes. elim skel_sound with e0 T0 (Srt s1); simpl in |- *; auto with coc core arith datatypes. unfold skel_int in |- *. replace (cls_of_int (int_cons T0 ipe (cv_skel (cl_term T0 (cls_of_int ipe))) X2)) with (class_env (T0 :: e0)). elim skel_sound with (T0 :: e0) U (Srt s2); simpl in |- *; auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. unfold cls_of_int at 1 in |- *. simpl in |- *. cut (typ_skel (cl_term T0 (class_env e0)) = PROP). generalize X2. rewrite H7. pattern (cl_term T0 (class_env e0)) in |- *. apply class_typ_ord with s1; simpl in |- *; auto with coc core arith datatypes. intros. rewrite H13. elim H7; auto with coc core arith datatypes. intros. elim H7; auto with coc core arith datatypes. elim skel_sound with e0 T0 (Srt s1); simpl in |- *; auto with coc core arith datatypes. unfold cls_of_int in |- *. elim H5; simpl in |- *; auto with coc core arith datatypes. unfold cls_of_int in |- *. elim H6; simpl in |- *; auto with coc core arith datatypes. unfold skel_int. generalize (skel_sound (T0 :: e0) U (Srt s2) H3). simpl in |- *. rewrite H7. elim (cl_term U (TCs class (cl_term T0 (class_env e0)) (class_env e0))); simpl in |- *; auto with coc core arith datatypes. elim (cl_term T0 (class_env e0)); simpl in |- *; auto with coc core arith datatypes. apply H2; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_typ