simp_nf failure?

Stream: general

[Mario Carneiro]

On current master, src#classical.not_imp is a simp lemma that can be proven from src#classical.not_forall and src#exists_prop . Does anyone have an idea why the simp_nf linter doesn't notice? I checked nolints and don't see any obvious reason for it to not be found, but I stumbled on this in #3812 where the only essential difference is that the names of these lemmas have changed.

[Gabriel Ebner]

This is because classical.not_imp is declared after classical.not_forall. We have quite a few of these short-circuiting simp lemmas.