'rewrite' doesn't want to match large expression

Using Coq
1

I have a proven lemma which goes something along the lines of:

Lemma my_lemma : forall (x y : some_type), Foo x y = expression .
Proof.
actual proof
Qed.

And I want to use it in a goal that contains:

Foo (large_expression1) (large_expression2)

However, rewrite * -> my_lemma doesn’t seem to identify that particular occurrence. To further complicate things, expression, large_expression1 and large_expression2 all contain occurrences of the pattern.

Is there any way I could rewrite those without explicitly passing them to replace and then proving the equality? Those large expressions are really large.

2

Well, turns out ‘rewrite’ was perfectly fine. One of the inner expressions contained a term from a forall at the top level, when I expected the opposite. Using ‘intros’ fixed the problem, but now I’ll need to rethink my proof…