feat(exporter/traits): parent bounds on impl and associated types

[W95Psp]

This PR:

• exporter:
  • decorate the paths to impl expressions with clause_ids;
  • refactor/clean/fixes some code;
  • resolve impl expressions and clauses for parent bounds and associated bounds on impl blocks;
• engine:
  • renames the trait_ref AST type into trait_goal;
  • introduces impl_ident in the AST;
  • propagate/add the impl idents introduced in the exporter.

In a more high-level view, this PR adds the things missing in the exporter for fully supporting explicit implementation expressions.
I think now we have all the information in hax' AST to extract code with already resolved traits. For instance, we should be able to rework the F* backend so that we don't rely on TC inference on F* side any longer.

[franziskuskiefer]

Thanks

• I'm not annotating all changes, but please add comments to all code you touch that doesn't have comments yet.
• Comments/messages like "make more ergonomic" or "update x" are not useful. What is the change doing?
• There seem to be some renamings in here. Please split out mass changes like this in future.

[W95Psp]

Thanks for the review!

I added some documentation. For copied.rs, I added minimal comments linking to the "mirrored" item in rustc crates + documenting additions, wdyt?

Yeah, such vague commit messages aren't great. though, here by update owner_id I actually meant that the code is now updating the field owner_id 😅 I should make that more obvious though!