Fail repeat match goal with H:_ |- _ => setoid_rewrite X in H end.