kdrag.theories.logic.axioms.exists_cong

kdrag.theories.logic.axioms.exists_cong(vs: list[ExprRef], pf: Proof) → Proof

Congruence for exists binders

>>> x = smt.Bool("x")
>>> exists_cong([x], kd.prove(x | x == x))
|= (Exists(x, Or(x, x))) == (Exists(x, x))

Parameters:

• vs (list[ExprRef])

• pf (Proof)

Return type:

Proof