SetoidReasoning is no longer needed