proposition: Fact subst_poly_type_many_poly_abs {σ n target} : subst_poly_type σ (many_poly_abs n target) = many_poly_abs n (subst_poly_type (Nat.iter n up_poly_type_poly_type σ) target).
proof: Proof. elim: n σ; first done. move=> n IH σ /=. congr poly_abs. by rewrite IH iter_last. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun