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.