proposition: Lemma iipc2_Pt_soundness {xs tSs tPs t1 t2 t3 n1 n2 n3} : iipc2 (Gamma0 ++ map Ut (map (fun x : nat => poly_var (x + zt)) xs) ++ map St tSs ++ map Pt tPs) (Pt (t1, t2, t3)) -> Forall encodes_prod tPs -> encodes_nat t1 n1 -> encodes_nat t2 n2 -> encodes_nat t3 n3 -> n1 * n2 = n3.
proof: Proof. move=> /generalize_Gamma0 /generalize_GammaU /generalize_GammaS. move=> + HtSs /= => /iipc2_poly_arrE /iipc2_poly_arrE /iipc2_poly_arrE /iipc2_is_safe_environment. apply: unnest. { do 6 (constructor; first by move=> /=; lia). by apply: is_safe_environment_Pt. } move=> [ss'] [ts'] [+ Hss] => /=. rewrite in_map_iff. do 6 (case; first by move=> /last_poly_var_safe_poly_type). move=> [[[s1 s2] s3]] /= [/(congr1 parameters_poly_arr)]. rewrite parameters_poly_arr_safe_poly_type /=. move=> Hss'. case: ts' Hss' Hss; last done. rewrite /length => <-. under [map (subst_poly_type _) _]map_ext => ? do (rewrite subst_poly_type_poly_var). rewrite map_id ?app_comm_cons. move=> /Forall_cons_iff [/generalize_GammaP H1] /Forall_cons_iff [/generalize_GammaP H2] /Forall_cons_iff [/generalize_GammaP H3] _. move: HtSs => /Forall_forall => H /H{H} /= [n1'] [n2'] [n3'] [Hn1'] [Hn2'] [Hn3'] + Hn1 Hn2 Hn3. have := encodes_nat_transport' H1 Hn1 Hn2 Hn3 Hn1'. have := encodes_nat_transport' H2 Hn1 Hn2 Hn3 Hn2'. have := encodes_nat_transport' H3 Hn1 Hn2 Hn3 Hn3'. clear. rewrite /b1t /b2t /b3t. by lia. 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