RPImports = HOL_Rls + HOL_Cut + HOL_Rep + newSub