kdrag.theories.logic.axioms.eqtrans

kdrag.theories.logic.axioms.eqtrans(eq1: Proof, eq2: Proof) → Proof

Prove transitivity of equality

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

Parameters:

Return type:

Proof