CutRedImports = HOL_Rls + HOL_Cut