simproc equivalent of apply_ite for match statements

Stream: Is there code for X?

[Geoffrey Irving]

Often I have expressions like

`f (match e with | Exit.large => x | _ => y)

and I would like to push the f application inside each match branch. Is there a way to do this within a single simp invocation, in the same way that docs#apply_ite can do this for ifs within simp?

I can do this by writing down a version of apply_ite specialised to the particular type I'm matching over, but it is a bit sad to do so. I'm imagining that it would have to be a simproc, since presumably one can't write down a lemma that understands all the different kinds of matches.

[Aaron Liu]

does split help?

[Ruben Van de Velde]

Not with the question as asked, no

[Geoffrey Irving]

I will look into split then, thank you!