如何表達「Coq中存在唯一的X」？

Question

我想知道是否有一個簡潔寫作的方式，存在一個獨特的東西（即寫獨特的存在量詞）在Coq？

例如，說有一個x s.t. 2 + x = 4：

Goal exists x, 2 + x = 4. 

如何我寫了存在獨特x具有相同的屬性？

我知道我可以在s.t.部分這樣的複製謂詞：

Goal exists x, 2 + x = 4 /\ forall y, 2 + y = 4 -> y = x. 

但是，這是一個很多普通的重複的，並且是有辦法以某種方式編碼一個新的量詞，並寫：

Goal exists1, 2 + x = 4. 

表達相同的目標？

Answer 1

Coq已經提供了exists!表示法。例如：

Goal exists! x, 2 + x = 4. 
Proof. 
exists 2. split. 
+ reflexivity. 
+ intros. injection H; intro. 
    symmetry; assumption. 
Qed.