Is there a way to provide a witness to a goal of the form `[exists _, _]`

without first applying `existsP`

? Basically something analogous to rewriting with a hypothesis `H : b = true`

when our goal is `b && b'`

instead of going through `apply/andP; split=> //`

.

Not that I know of, but we could add

```
Lemma existsb (T : finType) (P : {pred T}) (x : T) : P x -> [exists x, P x].
Proof. by move=> Px; apply/existsP; exists x. Qed.
Arguments existsb {T P}.
```

So that `rewrite (existsb x).`

would do what you want?

Yes! Thanks

Cyril Cohen has marked this topic as resolved.

@Ana de Almeida Borges added: https://github.com/math-comp/math-comp/pull/941

Awesome!

Last updated: Jul 15 2024 at 21:02 UTC