In the following proof script:
Theorem foo : exists p, p = (1, 1).
Proof. eexists ?[p]. destruct ?p.
we end up with the goal:
n, n0 : nat
============================
(n, n0) = (1, 1)
Is there a way to destruct ?p such that we end up with the same goal we would get if we did eexists (?[p1], ?[p2]). instead of eexists ?[p].? I.e.:
(?p1, ?p2) = (1, 1)
destruct <term> replaces all occurrences of <term> with a constructor applied to its arguments (which are generated as variables in the context), with one goal per constructor. With an evar, you can choose which constructor should be applied by doing the instantiation yourself, e.g. with instantiate (p := (?[p1], ?[p2])).