Make the type parameters implicit in the generated functions

[sonmarcho]

The generated functions have explicit type parameters, which makes them a bit cumbersome to use in practice: we could make them implicit in most situations. Of course, we have to make sure that we can always type check the generated files. We could do so in a conservative manner, by making sure a function's implicit parameters can always be deduced from its inputs. There are two cases to take into account.

1. We would need to analyze the signature of the function, to check that the type parameters can be deduced from the input arguments. We could simply check that all the type parameters appear in some input arguments. Note that some quite common functions don't satisfy this condition, for instance fn Vec<T>::new() -> Vec<T> doesn't take any inputs. The type parameters which wouldn't appear in the input arguments would be left as explicit.

2. We might need to introduce type ascriptions when creating structure values, if there are conflicts between field names (i.e., two different structure types have fields with the same names). Note that we do use the fact that some provers like Lean leverage typing information to disambiguate such situations (for Lean, we use short names for the fields, which might collide).