kdrag.kernel.subst

kdrag.kernel.subst(eq: Proof, t: ExprRef) → Proof

Substitute subterms using equality proof

>>> x, y = smt.Ints("x y")
>>> eq = prove(x == ((x + 1) - 1))
>>> subst(eq, x + 3)
|- x + 3 == x + 1 - 1 + 3

Parameters:

Return type:

Proof