kdrag.theories.logic.axioms.substitute_fresh_vars

kdrag.theories.logic.axioms.substitute_fresh_vars(pf: Proof, *subst) → Proof

Substitute schematic variables in a theorem. This is is single step instead of generalizing to a Forall and then eliminating it.

>>> x = kd.FreshVar("x", smt.IntSort())
>>> y = kd.FreshVar("y", smt.IntSort())
>>> substitute_fresh_vars(kd.kernel.prove(x == x), (x, smt.IntVal(42)), (y, smt.IntVal(43)))
|= 42 == 42

Parameters:

pf (Proof)

Return type:

Proof