Mechanism to associate "laws" to a type/identifier/etc

[Armael]

Feature request: a mechanism to declare lemmas associated with a type/... to automatically load in the proof context.
Example of usecase: if I define a Seq::map function, then a number of natural compatibility lemmas follows (wrt cons, snoc, concat, etc). It would be convenient for these lemmas to be loaded in the proof context automatically.

An idea from @xldenis is to allow specifying #[law] on a type, but allow refining it with #[law(for = identifier)], in which case the law is only loaded if the given identifier is actually used in the proof.