proposition: Fact subst_poly_type_many_poly_arr {σ args target} : subst_poly_type σ (many_poly_arr args target) = many_poly_arr (map (subst_poly_type σ) args) (subst_poly_type σ target).
proof: Proof. elim: args; first done. move=> s args IH /=. congr poly_arr. by apply: IH. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun