# 'rewrite' doesn't want to match large expression

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.

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…