proposition: Lemma subst_poly_type_SU_term_to_poly_type {ζ n t} : poly_var_bound (SU_term_to_poly_type t) < n -> subst_poly_type (fold_right scons poly_var (map (fun x => SU_term_to_poly_type (ζ x)) (seq 0 n))) (SU_term_to_poly_type t) = SU_term_to_poly_type (SU.substitute ζ t).
proof: Proof. move=> ?. rewrite subst_poly_type_map_seq; first by lia. by apply: SU_term_to_poly_type_SU_substitute. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts pure_typing_facts pure_typable_prenex) ssreflect ssrbool ssrfun