proposition: Lemma introduce_Uts (n: nat) : iipc2 (Gamma0 ++ GammaUSP n) (poly_var tt) -> iipc2 GammaH (poly_var tt).
proof: Proof. elim: n; first by rewrite /GammaUSP; unlock. move=> n + HSn. apply. apply: (iipc2_poly_varI 0 (ts := [poly_num (1+n)])); first by reflexivity. rewrite [Gamma0]lock /map subst_poly_type_Ut' [many_poly_arr]lock /=. move=> [:HUt0]. constructor. { abstract: HUt0. by apply /iipc2_var_InI /in_app_r /in_Ut_GammaUSP. } do 3 (constructor; first done). clear HUt0. constructor; last done. apply: (iipc2_poly_absI (S (S n) + zt)). - clear. have ->: S (S n) + zt = S (S zt) + n by lia. apply /Forall_appI. { rewrite -lock. do 3 (constructor; first by apply /fresh_inP). constructor; last done. rewrite /t_cs /tt. apply /fresh_in_many_poly_absI /fresh_in_many_poly_arrI; last by lia. apply /Forall_appI. + apply /Forall_map /Forall_seqP => x ?. rewrite /fresh_in /= /dt /b1t /b2t /ut. by lia. + have := δP. move=> H. apply /Forall_map. apply: Forall_impl H. case=> > /=; rewrite /fresh_in /= /dt /b1t /b2t /b3t /ut /st /pt /zt /zt'; by lia. } rewrite /GammaUSP -lock. apply /Forall_appI; [| apply /Forall_appI; [apply /Forall_appI |]]; apply /Forall_map /Forall_seqP; firstorder (by [|move=> /=; lia]). - set σ := (σ in subst_poly_type σ _). have Hσ: forall x, σ x = (scons (poly_var 0) (scons (poly_var (S (S n) + zt)) (funcomp poly_var S))) x by move=> [|[|x]]. under ext_poly_type => ? do rewrite Hσ. have ->: S (S n) + zt = S (S zt) + n by lia. unlock. by firstorder by [|lia]. - rewrite poly_type_norm. set σ := (σ in subst_poly_type σ _). have Hσ: forall x, σ x = fold_right scons poly_var [poly_var (S (S n) + zt); poly_var (S n + zt)] x by move=> [|[|x]]. under ext_poly_type => ? do rewrite Hσ. clear σ Hσ. set σ := (σ in subst_poly_type σ _). rewrite -[locked many_poly_arr]lock [Ut']lock [St']lock [Pt']lock /= -[locked Ut']lock -[locked St']lock -[locked Pt']lock ?subst_poly_type_Ut' ?subst_poly_type_St' ?subst_poly_type_Pt' /=. do 4 (apply: iipc2_poly_arrI). apply: iipc2_weakening HSn. clear. move=> t. rewrite /GammaUSP -?lock [Gamma0]lock GammaUSn GammaS0Sn GammaS1Sn GammaP0Sn. rewrite [GammaU]lock [GammaS0]lock [GammaS1]lock [GammaP0]lock /= ?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