proposition: Lemma generalize_Gamma0 {GammaU GammaS GammaP t} : iipc2 (Gamma0 ++ GammaU ++ GammaS ++ GammaP) t -> iipc2 ([poly_var tt] ++ GammaU ++ GammaS ++ GammaP) t.
proof: Proof. move: (GammaU ++ GammaS ++ GammaP) => ?. apply: iipc2_generalization. do 3 (constructor; first by (apply: last_poly_var_typingI; left)). constructor; first by (apply: last_poly_var_typingI; rewrite last_poly_var_t_cs; left). by apply /Forall_forall => ? ?; apply /iipc2_var_InI /in_app_r. 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