proposition: Lemma iipc2_poly_varI x {Gamma ts ss y} : nth_error Gamma x = Some (many_poly_abs (length ts) (many_poly_arr ss (poly_var (length ts + y)))) -> Forall (iipc2 Gamma) (map (subst_poly_type (fold_right scons poly_var (rev ts))) ss) -> iipc2 Gamma (poly_var y).
proof: Proof. move=> /typing_var /typing_many_ty_appI => /(_ ts ltac:(done)). rewrite subst_poly_type_many_poly_arr /subst_poly_type -rev_length fold_right_length_ts -/subst_poly_type. move=> /iipc2I. move: (map _ ss) => {}ss. move: (poly_var y) => t. elim: ss t; first done. by move=> s ss IH t /= [?] /typing_app H /Forall_cons_iff [[?] /H{H} /iipc2I /IH]. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts typing_facts) ssreflect ssrbool ssrfun