Is there a way to tell Coq to rewrite a goal/hypothesis of the form
f (match e with p1 => e1 | ... | pn => en end)
match e with p1 => f e1 | ... | pn => f en end
Similarly, is there a way to get Coq to rewrite
match e with p1 | ... | pn => e' end
When reasoning with functions defined using
Fixpoint which contain nested pattern matching, I find myself doing a lot of
destruct e in order to achieve the same effect, which is tedious and repetitive.
Any additional advice on reasoning about
match ... with is welcome. Thanks!