proposition: Lemma eliminate_φ: iipc2 (Gamma0 ++ GammaUSP (S ϵ) ++ Gammaφ) (poly_var tt).
proof: Proof. apply: (iipc2_poly_varI 3 (ts := rev (map (fun x => poly_num (φ x)) (seq 0 δ)))); first by rewrite rev_length map_length seq_length. rewrite map_app rev_involutive. apply /Forall_appI. - apply /Forall_map /Forall_map /Forall_seqP => x Hx. set ts := (map _ _). have ->: δ = length ts by rewrite /ts map_length seq_length. rewrite subst_poly_type_Ut' /subst_poly_type /ts fold_right_map_seq; first by lia. apply /iipc2_var_InI /in_app_r /in_app_l /in_Ut_GammaUSP. have := ϵP x. by lia. - apply /Forall_map /Forall_map. rewrite /Gammaφ. clear. have := δP. elim: (h10cs); first done. move=> c cs IH. move=> /Forall_cons_iff [Hc /IH {}IH]. constructor. + set ts := (map _ (seq _ _)). have Hδ: δ = length ts by rewrite /ts map_length seq_length. move: c Hc {IH} => []; rewrite /h10c_poly_type. * move=> x ?. have ->: δ + 1 + zt = δ + (1 + zt) by lia. rewrite Hδ subst_poly_type_St' /subst_poly_type ?fold_right_length_ts fold_right_map_seq; first by lia. apply /iipc2_var_InI /in_app_r /in_app_r. by left. * move=> x y z ?. rewrite Hδ subst_poly_type_St' /subst_poly_type. do 3 (rewrite fold_right_map_seq; first by lia). apply /iipc2_var_InI /in_app_r /in_app_r. by left. * move=> x y z ?. rewrite Hδ subst_poly_type_Pt' /subst_poly_type. do 3 (rewrite fold_right_map_seq; first by lia). apply /iipc2_var_InI /in_app_r /in_app_r. by left. + apply: Forall_impl IH => ?. apply: iipc2_weakening => ?. move: (Gamma0) (GammaUSP _) => ? ?. clear. rewrite ?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