fact: Definition up_poly_type_poly_type (sigma : ( nat ) -> poly_type ) : ( nat ) -> poly_type := scons ((poly_var ) var_zero) (funcomp (ren_poly_type shift) sigma).
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms