simp lemmas and reducible definitions

Stream: general

[Johan Commelin]

If I have a @[reducible] def X := Y, do simp-lemmas for Y also trigger for X? Or do I need to restate them?

[Chris Hughes]

They do trigger, I believe.

[Simon Hudon]

I don't think they trigger. Head symbols are matched strictly with simp

[Johan Commelin]

Thanks, that confirms my suspicion.