simpNF linter does not handle conditional simp lemmas correctly

[eric-wieser]

The linter fails here, but I claim it should succeed:

import Std

@[simp] theorem cast_fin_h {n m : Nat} (h : m = n) (a : Fin (m + 2)) : (cast (by rw [h]) a : Fin (n + 2)) = (a : Nat) := by cases h; rfl

#lint
#check @cast_fin_h /- Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.
 -/

-- but `simp` works just fine
example {n m : Nat} (h : m = n) (a : Fin (m + 2)) : (cast (by rw [h]) a : Fin (n + 2)) = (a : Nat) := by
  simp [h]

I think this code is falsely concluding that this is not a conditional simp lemma:
https://github.com/leanprover/std4/blob/c14f6a65b2c08caa38e1ab5db83451460d6cde3e/Std/Tactic/Lint/Simp.lean#L35-L45

The check for "appears on the LHS" should not visit Prop subexpressions, as those aren't found by unification.