I’m trying to prove the following lemma about functions on natural numbers

```
Lemma nat_funcs :
forall (f : nat -> nat -> nat) (P : (nat -> nat) -> Prop),
(forall n, P (fun m => (f n m))) -> P (fun m => f (m + 1) m).
```

When I proceed and introduce variables to the context, I end up with a hypothesis:

```
H : forall n, P (fun m => (f n m))
```

and my goal is:

```
P (fun m => f (m + 1) m)
```

I would like to apply H and instantiate n with m + 1 but the problem is, m is out of scope, is there a way I can do that?

I tried eapply and rapply but this doesn’t work either.