proposition: Lemma int_sound : forall e t T, typ e t T -> forall (ip : intP) (it : intt), int_adapt e ip it -> int_typ T ip PROP (int_term t it 0).
proof: Proof. simple induction 1; simpl in |- *; intros. red in |- *; apply Acc_intro; intros. inversion_clear H2. red in |- *; apply Acc_intro; intros. inversion_clear H2. elim (le_gt_dec 0 v); [ intro Hle | intro Hgt ]. rewrite lift0. elim minus_n_O with v. elim H1; intros. rewrite H3. generalize ip it H2. clear H3 Hle H2 it ip H1 t0. elim H4. intros l ip it (in_interp, p, q); revert p q; inversion_clear in_interp; simpl in |- *; intros ip_can_adapted same_classes. apply eq_cand_incl with (int_typ x ip0 PROP); auto with coc core arith datatypes. unfold lift in |- *. apply lift_int_typ with y; auto with coc core arith datatypes. intros l n y H1 H2 ip it (in_interp, p, q); revert p q; inversion_clear in_interp; simpl in |- *; intros ip_can_adapted same_classes. simpl in |- *. rewrite simpl_lift. apply eq_cand_incl with (int_typ (lift (S n) x) ip0 PROP). unfold lift at 2 in |- *. apply lift_int_typ with y0; auto with coc core arith datatypes. apply H2. apply Build_int_adapt; auto with coc core arith datatypes. inversion_clear ip_can_adapted; auto with coc core arith datatypes. injection same_classes; auto with coc core arith datatypes. inversion_clear Hgt. elim H6; intros in_interp ip_can_adapted same_classes. apply Abs_sound; intros; auto with coc core arith datatypes. apply int_typ_cr; auto with coc core arith datatypes. simpl in |- *; intros. change (is_can PROP (int_typ U (int_cons T0 ip (cv_skel (cl_term T0 (cls_of_int ip))) X) PROP)) in |- *. apply int_typ_cr. unfold int_cons, ext_ik in |- *. generalize X H7 H8. elim (cl_term T0 (cls_of_int ip)); auto with coc core arith datatypes. unfold subst in |- *. rewrite int_term_subst; auto with coc core arith datatypes. apply H5. unfold int_cons, ext_ik in |- *. apply Build_int_adapt; auto with coc core arith datatypes. generalize C H8 H9. elim (cl_term T0 (cls_of_int ip)); auto with coc core arith datatypes. simpl in |- *. pattern (cls_of_int ip) at 1 in |- *. rewrite same_classes. unfold cls_of_int in |- *. pattern (cl_term T0 (class_env e0)) in |- *. apply class_typ_ord with s1; elim same_classes; simpl in |- *; auto with coc core arith datatypes. rewrite same_classes. elim skel_sound with e0 T0 (Srt s1); simpl in |- *; auto with coc core arith datatypes. elim same_classes; auto with coc core arith datatypes. apply H1 with ip; auto with coc core arith datatypes. elim H4; intros in_interp ip_can_adapted same_classes. elim type_case with e0 u (Prod V Ur); intros; auto with coc core arith datatypes. inversion_clear H5. apply inv_typ_prod with e0 V Ur (Srt x); auto with coc core arith datatypes; intros. apply eq_cand_incl with (int_typ Ur (int_cons V ip (cv_skel (cl_term V (cls_of_int ip))) (int_typ v ip _)) PROP). replace PROP with (skel_int Ur (int_cons V ip (cv_skel (cl_term V (cls_of_int ip))) (int_typ v ip (cv_skel (cl_term V (cls_of_int ip)))))). unfold subst, int_cons in |- *. apply subst_int_typ with ip (ext_ik V ip (cv_skel (cl_term V (cls_of_int ip))) (int_typ v ip (cv_skel (cl_term V (cls_of_int ip))))) (V :: e0) (Srt s2); auto with coc core arith datatypes. unfold ext_ik in |- *. rewrite same_classes. cut (cl_term v (cls_of_int ip) = cl_term v (class_env e0)). elim class_sound with e0 v V (Srt s1); intros; auto with coc core arith datatypes. elim same_classes; auto with coc core arith datatypes. simpl in |- *. unfold ext_ik in |- *. rewrite same_classes. unfold cls_of_int in |- *. apply class_typ_ord with s1; elim same_classes; simpl in |- *; auto with coc core arith datatypes. rewrite same_classes. elim skel_sound with e0 V (Srt s1); simpl in |- *; auto with coc core arith datatypes. elim same_classes; auto with coc core arith datatypes. unfold ext_ik in |- *. red in |- *; red in |- *; auto with coc core arith datatypes. apply Tfa2_cs; auto with coc core arith datatypes. elim (cl_term V (cls_of_int ip)); auto with coc core arith datatypes. change (int_inv ip) in |- *. apply adapt_int_inv; auto with coc core arith datatypes. replace (cls_of_int (TCs Int_K (ext_ik V ip (cv_skel (cl_term V (cls_of_int ip))) (int_typ v ip (cv_skel (cl_term V (cls_of_int ip))))) ip)) with (class_env (V :: e0)). apply class_typ_ord with s2; auto with coc core arith datatypes. discriminate. discriminate. simpl in |- *. unfold cls_of_int at 1, ext_ik in |- *. rewrite same_classes. pattern (cl_term V (class_env e0)) in |- *. apply class_typ_ord with s1; elim same_classes; simpl in |- *; auto with coc core arith datatypes. rewrite same_classes. elim skel_sound with e0 V (Srt s1); simpl in |- *; auto with coc core arith datatypes. elim same_classes; auto with coc core arith datatypes. unfold int_cons, skel_int in |- *. replace (cls_of_int (TCs Int_K (ext_ik V ip _ (int_typ v ip (cv_skel (cl_term V (cls_of_int ip))))) ip)) with (class_env (V :: e0)). elim skel_sound with (V :: e0) Ur (Srt s2); simpl in |- *; auto with coc core arith datatypes. simpl in |- *. unfold ext_ik in |- *. rewrite same_classes. unfold cls_of_int in |- *. elim class_sound with e0 v V (Srt s1); auto with coc core arith datatypes. simpl in |- *. elim same_classes; auto with coc core arith datatypes. simpl in |- *. elim same_classes; auto with coc core arith datatypes. unfold Pi in H3. apply H3; auto with coc core arith datatypes. apply int_typ_cr; auto with coc core arith datatypes. discriminate H5. apply sn_prod. apply H1 with ip; auto with coc core arith datatypes. apply sn_subst with (Ref 0). unfold subst in |- *. rewrite int_term_subst. elim H4; intros in_interp ip_can_adapted same_classes. apply H3 with (def_cons T0 ip). unfold def_cons, int_cons in |- *. apply Build_int_adapt. apply int_cs; auto with coc core arith datatypes. apply (var_in_cand 0 (int_typ T0 ip PROP)); auto with coc core arith datatypes. exact (int_typ_cr T0 ip ip_can_adapted PROP). red in |- *. apply Tfa_cs; auto with coc core arith datatypes. unfold ext_ik in |- *. elim (cl_term T0 (cls_of_int ip)); auto with coc core arith datatypes. unfold ext_ik in |- *. rewrite same_classes. unfold cls_of_int in |- *. simpl in |- *. pattern (cl_term T0 (class_env e0)) in |- *. apply class_typ_ord with s1; simpl in |- *; elim same_classes; auto with coc core arith datatypes. rewrite same_classes. elim skel_sound with e0 T0 (Srt s1); simpl in |- *; auto with coc core arith datatypes. elim same_classes; auto with coc core arith datatypes. cut (typ e0 U (Srt s)); auto with coc core arith datatypes. intros. apply eq_cand_incl with (int_typ U ip PROP); auto with coc core arith datatypes. replace PROP with (skel_int U ip). elim H5; intros in_interp ip_can_adapted same_classes. apply conv_int_typ with e0 (Srt s); auto with coc core arith datatypes. apply class_typ_ord with s; auto with coc core arith datatypes. discriminate. discriminate. unfold skel_int in |- *. elim H5; intros in_interp ip_can_adapted same_classes. rewrite same_classes. elim skel_sound with e0 U (Srt s); simpl in |- *; auto with coc core arith datatypes. elim type_case with e0 t0 U; intros; auto with coc core arith datatypes. inversion_clear H6. 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 H6; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_term Int_typ Int_stab