rfc: mispelled ident suggestion

Stream: lean4

[Alok Singh]

i think the error messages should offer similarly spelled identifiers:

2025-07-01-17-04-43.png

here it could suggest Vector.size as something in the env that's semantically/syntactically close.