Hi Stephan,
Thank you for the response. I understand that CHOOSE is deterministic, but it's still not clear to me that TLC's response is correct. Logically, TLC successfully verified the implication:
Spec(CHOOSE f: f \in F) => Inv (let's call this Imp)
You seem to be saying that, since
\E f \in F: Spec(f) => Inv
(which is true) then TLC was right to declare (Imp) as verified? That doesn't seem correct to me. Or am I misunderstanding what you're saying?
I'd expect that, given that F # {}, we'd have to prove
\A f \in F: Spec(f) => Inv
instead. Though I'm not sure if this is equivalent to (Imp) (I think it's stronger than Imp, given that F # {}, but not sure about equivalence).
Cheers,
Ognjen