generalised some results using type classes
unregister lifting setup following the best practice of Lifting
new rule for making rsp theorem more readable
simplify a proof due to 6c95a39348bd