# Applying hypothesis with unknown variables

**URL:** <https://discourse.rocq-prover.org/t/applying-hypothesis-with-unknown-variables/987>\
**Category:** Using Rocq\
**Created:** [July 31, 2020, 10:22pm UTC](https://discourse.rocq-prover.org/t/applying-hypothesis-with-unknown-variables/987 "2020-07-31T22:22:49Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![LailaElbeheiry](https://avatars.discourse-cdn.com/v4/letter/l/67e7ee/32.png) [@LailaElbeheiry](https://discourse.rocq-prover.org/u/LailaElbeheiry)\
**Post date:** [July 31, 2020, 10:22pm UTC](https://discourse.rocq-prover.org/t/applying-hypothesis-with-unknown-variables/987/1 "2020-07-31T22:22:49Z")

</div>

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

```auto
  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:

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

```

and my goal is:

```auto
 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.

---

<div class="post-metadata">

**Author:** ![jashug](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jashug/32/411_2.png) [@jashug](https://discourse.rocq-prover.org/u/jashug)\
**Post date:** [July 31, 2020, 10:31pm UTC](https://discourse.rocq-prover.org/t/applying-hypothesis-with-unknown-variables/987/2 "2020-07-31T22:31:40Z")

</div>

This lemma is false.

Consider what happens when `P g` is the proposition that `g` is a constant function.  
Then when `f x y = x`, we have `forall n, (fun m => f n m) = (fun m => n)` which is a constant function, while `(fun m => f (m + 1) m) = (fun m => m + 1)` which is not a constant function.