feat(lean): associated types with equality constraints

[abentkamp]

This PR implements associated types with equality constraints for the Lean backend.

This fixes one part of #1710. Some uses of associated types such as (A as T)::B are not supported.

Implementation Details

Problem

Associated types would be most straight-forwardly modeled by Lean type classes that contain fields of type Type. However, Rust allows us to put equality constraints on associated types, for example in function definitions. This is hard to reproduce in Lean.

Solution

For every Rust trait, we generate:

• a Lean class that contains the associated types of the Rust trait. This is just an empty struct if there are no associated types.
• a Lean class that takes two parameters: Self : Type and an instance of the class containing the associated types. To make type inference work, we must mark the second parameter as outParam. The class fields are all non-type fields of the Rust trait.

Every function with a trait parameter will receive two parameters in Lean:

• an instance of the associated type class
• an instance of the class containing the other fields, taking the associated type class instance as a parameter. If equality constraints are present, we override fields in the associated type class instance instance.

[maximebuyse]

This looks good though it is a bit hard to review backend code so we should make sure there is enough testing. Can you update the snapshots so that we can see the results of the tests you added? This should also fix the CI!

[maximebuyse]

I added a few suggestions to improve the style, but otherwise this looks fine. Trying this on Core models could be the best way to test if it really does what we want!