Hi all,

I'm trying to understand how proofs in https://github.com/GeoCoq/GeoCoq work by re-writing them without using custom tactics or notation (or at least using fewer of them).

I got to a point where I've resolved all goals in the "first" lemma - `lemma_localextension`

, but I can't close the proof because "some unresolved existential variables remain".

At some point in the proof I have a goal of the following form:

```
exists X Y U V W, CI J U V W /\ (eq P U \/ (BetS U Y X /\ Cong U X V W /\ Cong U P U Y));
```

I can only provide witnesses for U V W, but that is also sufficient, so I use the following, which resolves the goal:

```
eexists.
eexists.
exists B.
exists B.
exists Q.
split.
exact h_postulate_Euclid3.
left.
reflexivity.
```

This leaves two existential variables introduced by eexists, how do I get rid of them?

Just in case, here is the full proof with all dependencies in a single file: https://gist.github.com/blin/d2bca64d034ac70905b933952cc3b23c . Comments on doing things differently/better would be appreciated.

that is also sufficient

the system is telling you that it's not

you can do `Unshelve`

to get the remaining goals, then solve them

or you can provide the value to `exists`

instead of using `eexists`

Thanks Gaëtan, doing Unshelve showed that supplying *any* two points is sufficient by the end of the proof so the following works

```
Unshelve.
auto.
auto.
```

But also supplying unrelated points instead of eexists works:

```
exists B.
exists B.
exists B.
exists B.
exists Q.
```

Evgenii Petrov has marked this topic as resolved.

Last updated: Oct 04 2023 at 20:01 UTC