kdrag.tactics.open_binder

kdrag.tactics.open_binder(pf: Proof) → tuple[list[ExprRef], Proof]

Open a proof with schematic variables so that it can be reconstructed.

>>> x,y,z = smt.Reals("x y z")
>>> pf = kd.prove(smt.ForAll([x,y], x + y + 1 > x + y))
>>> open_binder(pf)
([x!..., y!...], |= x!... + y!... + 1 > x!... + y!...)

Parameters:

pf (Proof)

Return type:

tuple[list[ExprRef], Proof]