I can easily prove this goal

```
schematic_goal "⋀x. P x ⟹ P ?x"
```

via

```
by (rule someI)
```

I can also prove

```
schematic_goal "⋀x y. P x y ⟹ P ?x ?y"
```

using for example

```
"P x y ⟹ P (fst (Eps (λ(x, y). P x y))) (snd (Eps (λ(x, y). P x y)))"
```

But what do I do for the following?

```
schematic_goal "⋀x y. P x y ⟹ P ?x y"
```

For, I assume technical, reasons that I don't quite understand `?x`

can't be instantiated with `x`

in all these cases, which is why I have to resort to `Eps`

. In the last case I'd have to instantiate `?x`

with something that doesn't depend on `y`

, but I in general no value for `?x`

has to exist that satisfies `P x y`

for all `y`

.

Do your really mean `(⋀x y. P x y) ⟹ P ?x ?y`

?

that is also the reason why `x`

cannot be instantiated with `x`

: they don't live in the same scope…

```
schematic_goal "(P x y ⟹ P ?x y)"
by assumption
```

Are you saying that `⋀x y. P x y ⟹ P ?x ?y`

is the same as `(⋀x y. P x y) ⟹ P ?x ?y`

because it really doesn't seem like it from the syntax highlighting in jedit. Also, `⋀x y. (P x y ⟹ P ?x ?y)`

still doesn't work `by assumption`

.

oh no sorry you are right

`⋀x y. (P x y ⟹ P ?x ?y) `

: this is a scope problem: you are trying to instantiate the global variable `?x`

with a local variable that only exists under `⋀`

this is also why you don't have that problem with the `P x y ⟹ P ?x ?y`

: you instantiate the global variable with a global variable

Yeah, that's why I have to come up with a constant through `Eps`

and why the following works, where I make `?x`

explicitly dependent on the local `x`

.

```
schematic_goal "(⋀x y. P x y ⟹ P (?x x) y)"
by assumption
```

I have some cases in "real code" where I have schematics in the conclusion like `P ?x`

from a rule application and a premise like `∃x. P x`

, which introduces a new local when I eliminate the quantifier which then can't be used to instantiate `?x`

. Sometimes I can mitigate this by eliminating the `∃x`

before applying the rule. But doing this automatically early enough is extremely hard.

Actually `⋀x y. P x y ⟹ P ?x y`

is the situation I encounter, that's why I'm asking about it.

As far as I understand this is an entirely technical problem, not a logical one, because `lemma "⋀x. P x"`

is equivalent to `lemma "P x"`

. So I was hoping to find a solution to turn `⋀x y. P x y ⟹ P ?x y`

into `P x y ⟹ P ?x y`

or some solution involving the choice operator.

can't you just change your theorem to require `\<exists>x. P x y`

?

It creates multiple new goals containing the schematic variable

I meant: changing the location where you actually need that theorem

because I have a hard time imagining where you could need such a theorem

After some consideration I think you're right. This issue doesn't occcur with properly written rules. I want to look into this again at some point though.

Last updated: Dec 07 2023 at 08:19 UTC