simpa at

Stream: general

[Kevin Kappelmann]

Is there some reason why we can do rwa [...] at some_hypothesis but not simpa [...] at some_hypothesis? I know I can use simpa [...] using some_hypothesis, but in most of my cases, I do not need to simplify the goal as well.