linter.constructorNameAsVariable false in turnExistsIntoForall

[awalterschulze]

Amazing library, thanks so much for the amazing work.

We are just attempting to update and we are having a problem:

In #49 the option was added set_option linter.constructorNameAsVariable false in above the test for turnExistsIntoForall.

We use Qoute4 on exists here https://github.com/katydid/proofs/blob/main/Katydid/Std/Balistic.lean#L283 in a tactic called wreck_exists, but we get this error:
error: ././././Katydid/Std/Balistic.lean:280:0: unknown free variable '_fvar.33580'

When we use set_option linter.constructorNameAsVariable false in above then the tactic is not created, the error goes away, but we cannot use wreck_exists anymore, because we get
error: ././././Katydid/Std/Balistic.lean:326:31: unknown tactic

This is where we are attempting to upgrade to the newest version of lean and it is breaking
katydid/regex-deriv-lean@3789860#diff-d996139c0cef6f145df4d12efca1d12573666cd1b14e87d1ba4e4addf7fd2949R279

I hope this is a useful issue report.

[awalterschulze]

I found a temporary work around katydid/regex-deriv-lean@33c67f5

But it would still be great to get this lint error fixed, so I hope it is worth keeping the issue open, until a fix is found