proposition: Lemma introduce_Pts (n n1 n2: nat) (Gamma: environment): n1 <= S n -> n2 <= S n -> n1 * n2 <= S n -> iipc2 (locked Gamma0 ++ GammaUSP n ++ (Pt (poly_num n1, poly_num n2, poly_num (n1*n2)) :: Gamma)) (poly_var tt) -> iipc2 (locked Gamma0 ++ GammaUSP n ++ Gamma) (poly_var tt).
proof: Proof. elim: n2 Gamma => [| n2 IH] Gamma ? ? ?. - apply: iipc2_weakening => t. rewrite ?in_app_iff /=. case; first by tauto. case; first by tauto. case; last by tauto. move=> <-. right. left. rewrite /GammaUSP -lock. apply /in_app_r /in_app_r. apply /in_map_iff. exists n1. have ->: n1 * 0 = 0 by lia. constructor; first done. apply /in_seq. by lia. - move=> H. apply: (introduce_Sts n (n1 * n2) n1); first by lia. apply: IH; [by lia | by lia | by lia |]. rewrite -[_ Gamma0]lock. apply: (iipc2_poly_varI 2 (ts := [poly_num (n1 * (S n2)); poly_num (S n2); poly_num (n1 * n2); poly_num n2; poly_num n1])); first by reflexivity. rewrite [Gamma0]lock /map ?subst_poly_type_Ut' ?subst_poly_type_St' subst_poly_type_Pt' /(subst_poly_type _ (poly_arr _ _)) -/subst_poly_type subst_poly_type_Pt' /subst_poly_type /=. have HUSP t Gamma' : In t (GammaUSP n) -> iipc2 (locked Gamma0 ++ GammaUSP n ++ Gamma') t. { move=> ?. apply: iipc2_var_InI. by apply /in_app_r /in_app_l. } constructor. { apply: iipc2_poly_arrI. apply: iipc2_weakening H => ?. rewrite /= ?app_comm_cons ?in_app_iff /=. clear. by tauto. } do 5 (constructor; first by (apply: HUSP; apply: in_Ut_GammaUSP; by lia)). constructor. { apply: iipc2_var_InI. rewrite ?in_app_iff /=. by tauto. } constructor; first by (apply: HUSP; apply: in_St1_GammaUSP; by lia). constructor; last done. have ->: n1 * n2 + n1 = n1 * S n2 by lia. apply: iipc2_var_InI. rewrite ?in_app_iff /=. by tauto. Qed.
imports: PeanoNat List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts term_facts typing_facts iipc2_facts sn_facts) Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun