feat: record simp theorems with bad keys

When `Simp.Config.index := false` and `set_option diagnostics true`,
for every `simp` theorem that is used to rewrite an expression,
`simp` checks whether the theorem would have been applied if
`Simp.Config.index := true`. If it would not, we record it,
and display it at diagnostics message.