Questions tagged [witness]
In mathematical logic, a witness is a specific value t to be substituted for variable x of an existential statement of the form ∃x φ(x) such that φ(t) is true. (from Wikipedia)
1
question
14
votes
4
answers
1k
views
How to extract the witness from exists in Coq in function notation/without destructing?
Assuming I have some definition with a forall and an exists like so:
Definition fooable A B P := forall a : A, exists b : B, P a b.
Then on an intuitive level, I ...
- 243