@Kha `hygienicIntro` is true by default. `hygienicIntro == false` is
the Lean3 behavior. If we find `hygienicIntro` too inconvenient in
practice, we set the default to false.
@Kha This is a first attempt to improve the error message for examples
like the one Andrew Kent posted on Zulip.
I created a simpler example using "vectors".
