Warn on unused variables during validation not just in SMTPat

[briangmilnes]

I just goofed up some lemmas by leaving an unused (i:nat) in the arguments. I missed this in validation as it does not warn (like to does nicely for rec when not recursive).

It would be a good idea to help provers catch this in validation.

Low priority though.