Rewrite at one hypothesis and goal

Stream: new members

[Pedro Minicz]

Is there a way to simultaneously rewrite at one hypothesis and the goal? I know I can rw x at h, rw x at h₁ h₂, and rw x at *. rw x at * doesn't work in my case because not all hypothesis can be rewritten.

[Johan Commelin]

Yes, use rw [foo, bar] at h \vdash

[Johan Commelin]

You can list as many hyps as you want.

[Pedro Minicz]

Thanks!