simp being silly again

Stream: general

[Reid Barton]

Is there a reason that simp could fail to apply a simp lemma, but rw with that lemma works fine?
Normally when simp fails it means I have to apply erw, but it seems to be getting dumber

[Mario Carneiro]

simp and rw use different ways of rewriting, and this can affect when one can succeed over another. Generally the congr approach to using rewrite lemmas works better, but there are some locations in a term that are not traversed, while rw will rewrite everywhere uniformly and hope for the best.