fix(lean): Add trait-level arguments as explicit arguments to trait items

[clementblaudeau]

Trait-level arguments are marked as always explicit for each trait item, ensuring a regular treatment at call sites.

Overview

Considering the following rust code :

trait T1<A, B> {
    fn f1<C, D>(&self) -> (); // A and B do not appear
    fn f2<C, D>(&self, x: &A) -> (); // A appears
    fn f3<C, D>(&self, x: &A, y: &B) -> (); // Both appear
}

Previously, the Lean backend would translate it as :

class T1 (Self : Type) (A : Type) (B : Type) where
  f1 (C : Type) (D : Type) : (Self -> RustM Rust_primitives.Hax.Tuple0)
  f2 (C : Type) (D : Type) : (Self -> A -> RustM Rust_primitives.Hax.Tuple0)
  f3 (C : Type) (D : Type) : (Self -> A -> B -> RustM Rust_primitives.Hax.Tuple0)

However, f1 and f3 would not have the same arguments : the trait-level parameters are explicit for f1 and implicit for f3. Now the Lean backend produces :

class T1 (Self : Type) (A : Type) (B : Type) where
  f1 (A B) (C : Type) (D : Type) : (Self -> RustM Rust_primitives.Hax.Tuple0)
  f2 (A B) (C : Type) (D : Type) : (Self -> A -> RustM Rust_primitives.Hax.Tuple0)
  f3 (A B) (C : Type) (D : Type) : (Self -> A -> B -> RustM Rust_primitives.Hax.Tuple0)

This, using leanprover/lean4#7742, ensures that the trait-level params A and B are always explicit.

fixes #1796

[abentkamp]

Why not remove these attributes completely?