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 = SchemaVar("x", smt.IntSort()) >>> y = SchemaVar("y", smt.IntSort()) >>> generalize([x, y], prove(x == x)) |- ForAll([x!..., y!...], x!... == x!...)