Link: add automation for the traits #756
Description
Context: for now, we need to to a lot of destruct to introduce the trait instances needed by the run_symbolic tactic. It is hard to scale this approach, as it can be hard to look for the name of the instances and find the right parameters for those that have some.
In this task, we want to find a way to use the inference mechanism of Rocq to find the correct instances. We should be able to infer automatically an example of link with several destruct of trait instances, including some with parameters.
We should obtain a proof of concept, but we will migrate the other trait definitions to this new mode in a separate task.