reorder premisses in J rule
working on J -- R_IdRecursion