proposition: Lemma iipc2_poly_absI (x: nat) {Gamma t} : Forall (fresh_in x) Gamma -> fresh_in (S x) t -> iipc2 Gamma (ren_poly_type (scons x id) t) -> iipc2 Gamma (poly_abs t).
proof: Proof. pose ξ := fun y => if PeanoNat.Nat.eq_dec x y then 0 else S y. move=> HG Ht /(iipc2_ren_poly_type ξ). have -> : map (ren_poly_type ξ) Gamma = (map (ren_poly_type S) Gamma). { elim: Gamma HG; first done. move=> s Gamma H /Forall_cons_iff [Hx /H{H} /= ->]. congr cons. apply: ext_ren_poly_type_allfv_poly_type. apply: allfv_poly_type_impl Hx => ? ?. rewrite /ξ. by case: (PeanoNat.Nat.eq_dec _ _). } move=> [?] /typing_ty_abs /iipc2I. congr iipc2. congr poly_abs. rewrite poly_type_norm /ξ /= ren_poly_type_allfv_id; last done. apply: allfv_poly_type_impl Ht. clear. move=> [|y]; case: (PeanoNat.Nat.eq_dec _ _); move=> /=; by lia. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts typing_facts) ssreflect ssrbool ssrfun