an be significant in various situations. You might like to
try to figure what those differences are, and decide if they matter to you in
general and/or in your specific goal
Michael
From: Haitao Zhang
Date: Wednesday, 27 February 2019 at 16:02
To: hol-info
Subject: [Hol-info] Exists unique quanti
I have trouble figuring out the best way to deal with exists unique
quantifers. The existing theorems rewrite it in a way that does not work
with CHOOSE_TAC or X_CHOOSE_TAC:
EXISTS_UNIQUE_DEF;
|val it = ⊢ $?! = (λP. $? P ∧ ∀x y. P x ∧ P y ⇒ (x = y)): thm
The top level connective is a conjunction
