kdrag.kernel.generalize

kdrag.kernel.generalize(vs: list[ExprRef], pf: Proof) → Proof

Generalize a theorem with respect to a list of schema variables. This introduces a universal quantifier for schema variables.

>>> x = FreshVar("x", smt.IntSort())
>>> y = FreshVar("y", smt.IntSort())
>>> generalize([x, y], prove(x == x))
|= ForAll([x!..., y!...], x!... == x!...)

Parameters:

• vs (list[ExprRef])

• pf (Proof)

Return type:

Proof