proposition: Lemma generalize_GammaC {s t t1 t2 t3}: iipc2 (to_d s :: [poly_arr (to_d t3) (poly_var b3t); poly_arr (to_d t2) (poly_var b2t); poly_arr (to_d t1) (poly_var b1t); poly_var tt] ++ [poly_var ut] ++ [poly_var st] ++ [poly_var pt]) (to_d t) -> iipc2 GammaC (poly_arr (to_d s) (to_d t)).
proof: Proof. move=> [?] /typing_abs /iipc2I /iipc2_generalization. apply. by do 7 (constructor; first by (apply: last_poly_var_typingI; firstorder done)). 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