theorem-2 works with EqR rather than SetoidReasoning again