kdrag.kernel.substitute_fresh_vars
- kdrag.kernel.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 = FreshVar("x", smt.IntSort()) >>> y = FreshVar("y", smt.IntSort()) >>> substitute_fresh_vars(prove(x == x), (x, smt.IntVal(42)), (y, smt.IntVal(43))) |= 42 == 42