Correctly namespace default trait methods

[Nadrieril]

trafficstars

Aeneas translates trait methods that have a default body because in the future we may want to refer to them. These methods are named Trait::method, which in Lean causes a name clash with the method field of Trait: both would be named Trait.method. To avoid this clash, in https://github.com/AeneasVerif/aeneas/pull/437 we rename these methods to Trait::default::method.

This however could still cause clashes with a method named default. We should find a naming scheme that is unlikely to clash with other names.