If I have a variable `(x : a)`

in the context and a hypothesis `H : exists (y : a), P`

how can I instantiate y with x? With forall I would do `specialize (H x)`

but with exists this do not work, here is a minimal example

```
Section Foo.
Parameter a : Set.
Parameter P : Prop.
Context (x : a).
Context (H : exists (y : a), P).
Goal P.
specialize (H x). (* want to do something like this *)
``
```

When `exists`

is in an assumption, you don't get to choose the witness.

Indeed; what you can do is destruct H to get the witness out and use it in a proof

Hmm, thanks I think I misunderstood the exists

Last updated: Jun 16 2024 at 02:41 UTC