proposition: Lemma introduce_φ (n: nat): ϵ <= S n -> iipc2 (Gamma0 ++ GammaUSP n ++ Gammaφ) (poly_var tt) -> iipc2 (Gamma0 ++ GammaUSP n) (poly_var tt).
proof: Proof. Proof using Hφ. move: (Hφ). have := δP. rewrite /Gammaφ [Gamma0]lock => + /Forall_forall + Hn. elim: (h10cs); first by rewrite app_nil_r. move=> [x | x y z | x y z] cs IH /Forall_cons_iff [Hδ /IH {}IH] /Forall_cons_iff /= [Hφc /IH {}IH]. - rewrite Hφc. by move=> /introduce_Sts => /(_ ltac:(lia)) /IH. - rewrite -Hφc. move=> /introduce_Sts H. apply /IH /H. have := ϵP z. by lia. - rewrite -Hφc. move=> /introduce_Pts H. apply /IH /H; [have := ϵP x | have := ϵP y | have := ϵP z]; 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