## Stream: General

### Topic: Schematic variables in goal after intro

#### Lukas Stevens (Apr 07 2020 at 09:15):

I'm trying to use `apply(intro transI relcompI)` on a goal of the form `trans (r O s)` but this gives me schematic variables in the goal. How can I avoid this?

#### Manuel Eberl (Apr 07 2020 at 09:35):

Huh? "intro" shouldn't introduce any schematic variables ever.

But it does :O

#### Manuel Eberl (Apr 07 2020 at 09:42):

can you show a minimal example

#### Lukas Stevens (Apr 07 2020 at 09:43):

```lemma "trans (r O s)"
apply(intro transI relcompI)
```

#### Lukas Stevens (Apr 07 2020 at 09:44):

For me, it produces:

```proof (prove)
goal (2 subgoals):
1. ⋀x y z. ⟦(x, y) ∈ r O s; (y, z) ∈ r O s⟧ ⟹ (x, ?b1 x y z) ∈ r
2. ⋀x y z. ⟦(x, y) ∈ r O s; (y, z) ∈ r O s⟧ ⟹ (?b1 x y z, z) ∈ s
```

#### Manuel Eberl (Apr 07 2020 at 09:50):

I can try to investigate later. I thought "intro" wasn't supposed to produce schematic variables.

#### Manuel Eberl (Apr 07 2020 at 09:50):

I would just use "rule" and "assumption" by hand, or "rule" and "erule"

#### Manuel Eberl (Apr 07 2020 at 09:51):

apply (rule transI) apply (erule (1) relcompI)

err no

#### Manuel Eberl (Apr 07 2020 at 09:51):

you'll first have to eliminate the "o" in the assumptions

#### Manuel Eberl (Apr 07 2020 at 09:52):

apply (elim relcompE), probably. And then "erule (2) relcompI"

Last updated: Aug 15 2022 at 04:16 UTC