kdrag.notation.QExists

kdrag.notation.QExists(vs: list[ExprRef], *concs) → BoolRef

Quantified Exists

Shorthand for ForAll(vars, And(conc[0], conc[1], …))

If variables have a property wf attached, this is anded into the properties.

Parameters:

vs (list[ExprRef])

Return type:

BoolRef