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.