在以下证明脚本中：
Theorem foo : exists p, p = (1, 1).
Proof. eexists ?[p]. destruct ?p.
我们最终的目标是：
n, n0 : nat
============================
(n, n0) = (1, 1)
有没有一种方法可以让?p我们最终得到和 相同的目标？eexists (?[p1], ?[p2]).例如：eexists ?[p].
(?p1, ?p2) = (1, 1)