Allow all hax-lib attributes on impl elements

[karthikbhargavan]

Currently, we only allow requires and ensures on inherent impl items (and then only if the impl itself is labeled with attributes. We cannot e.g. add fstar::before or fstar::verification-status to these items which should be very easy to support since these are translated to top-level items in F*.