kdrag.theories.set.Choose

kdrag.theories.set.Choose(A: ArrayRef | QuantifierRef, auto=False) → tuple[list[ExprRef], Proof]

Choose an arbitrary element from set A.

>>> x = smt.Int("x")
>>> Choose(smt.Lambda([x], x > 0))
([c!...], |= Implies(Exists(c!..., c!... > 0), c!... > 0))