@[expose] instance implementations via `deriving`

We sometimes need to add @[expose] to instances created via deriving, because the bodies will be reduced by the kernel in proof terms generated by tactics.

Currently the only mechanism to achieve this is

@[expose] section

deriving instance BEq for Poly

end

which works but is clunky. Ideally the deriving handler here would use @[expose] as much as possible (i.e. when not prevented by private fields).

Find the deriving handler and inspect how it generates instances such as deriving instance BEq for Poly, then compare that with the existing @[expose] section behavior. Determine when generated implementations can receive @[expose] and when private fields prevent it; done means the handler applies the attribute where permitted without requiring the surrounding section workaround.