The file `tests/lean/lakefile.lean` is regerenated in the Lean CI, but not tested for diff

[sonmarcho]

@R1kM noticed that the following line should be removed: https://github.com/AeneasVerif/aeneas/blob/852977db16ae4a8fecd4597097a2d98f5bd11a18/tests/lean/lakefile.lean#L33 because otherwise lake build in tests/lean fails (the file MutuallyRecursiveTraits.lean is not present, and should not be), and this issue is not caught in CI because the lakefile.lean is regenerated through script.sh and we do not test whether there is a diff.