This is slightly different from simple implication, as shown in this toy example.

```
Inductive R : nat -> nat -> Prop :=
| Base1: R 0 1
| Base2: R 0 2
| Ind: forall n m,
R n m -> R (n+1) (m+1).
```

Given this definition, we have three provable statements: `R 2 3`

, `R 3 5`

, and `(R 2 3) -> (R 3 5)`

. What I'm looking for is some way to formulate the following: "there does not exist a derivation path (i.e. a sequence of inductive constructor applications) that starts at `R 2 3`

and ends at `R 3 5`

.

Is there a way to do this in Coq?

`R 3 5`

as a hypothesis, you can "move back" in the implicit derivation path by using`inversion`

, and observe that`R 2 3`

does not appear. But in order to actually state this result I think you would need to explicitly define the notion of derivation path.requiresuse of another in its proof?"`R 2 3`

,`R 3 5`

, and`(R 2 3) -> (R 3 5)`

.” Should the last 5 be a 4?`R 2 3`

and`R 3 5`

, but the logical implication is still true. If you imagine proving this in Coq, this amounts to bringing`R 2 3`

into your context but never using it, and then just proving`R 3 5`

directly.