kdrag.kernel.eqtrans

kdrag.kernel.eqtrans(eq1: Proof, eq2: Proof) → Proof

Prove transitivity of equality

>>> x, y, z = smt.Ints("x y z")
>>> eq1 = axiom(x == y)
>>> eq2 = axiom(y == z)
>>> eqtrans(eq1, eq2)
|- x == z

Parameters:

Return type:

Proof