对您的第一个问题的简短回答是：一般来说，这是不可能的，但在您的特定情况下，是的。
在 Coq 的理论中，命题（即Props）及其证明具有非常特殊的地位。特别是，通常不可能编写提取存在证明的见证的选择运算符。这样做是为了使理论与某些公理和原则兼容，例如证明无关性，即给定命题的所有证明彼此相等。如果您希望能够做到这一点，则需要将此选择运算符作为附加公理添加到您的理论中，如 standard library。
但是，在某些特定情况下，可以从抽象存在证明中提取证人，而无需重复任何其他公理。特别是，当所讨论的属性是可判定的时，可以对可数类型（例如Z）执行此操作。例如，您可以使用Ssreflect 库中的choiceType 接口来获得您想要的内容（查找xchoose 函数）。
话虽如此，我通常会建议反对以这种方式做事，因为这会导致不必要的复杂性。直接定义Good 可能更容易，无需借助存在性证明，然后单独证明Good 具有所寻求的属性。
Definition Good : Z := (* ... *)
Definition IsGood (z : Z) : Prop := (* ... *)
Lemma GoodIsGood : IsGood Good.
Proof. (* ... *) Qed.
Lemma GoodUnique : forall z : Z, IsGood z -> z = Good.
如果您绝对想用存在证明来定义Good，您还可以更改Lemma_GoodExistsUnique 的证明以在Type 中使用连接词而不是Prop，因为它允许您直接提取见证使用proj1_sig 函数：
Lemma Lemma_GoodExistsUnique : {z : Z | Good z /\ forall z', Good z' -> z' = z}.
Proof. (* ... *) Qed.
关于你的第二个问题，是的，和第一点有点关系。再一次，我建议你写下一个函数y_from_x，类型为Z -> Z，它将在给定x 的情况下计算y，然后分别证明该函数以特定方式关联输入和输出。然后，通过证明y_from_x 是单射的，你可以说ys 对于不同的xs 是不同的。
另一方面，我不确定您的最后一个示例与第二个问题有何关系。如果我理解您想要正确执行的操作，您可以编写类似
Definition ThereAreNGoodIntegers (N : Z) (IsGood : Z -> Prop) :=
exists zs : list Z,
Z.of_nat (length zs) = N
/\ NoDup zs
/\ Forall IsGood zs.
这里，Z.of_nat : nat -> Z 是从自然数到整数的规范注入，NoDup 是断言列表不包含重复元素的谓词，Forall 是断言给定谓词 (在这种情况下，IsGood) 包含列表的所有元素。
作为最后一点，我建议不要将Z 用于只能涉及自然数的事物。在您的示例中，您使用整数来谈论集合的基数，并且该数字始终是自然数。