kdrag.theories.logic.axioms.lambda_cong

kdrag.theories.logic.axioms.lambda_cong(vs: list[ExprRef], pf: Proof) → Proof

>>> x = smt.Int("x")
>>> lambda_cong([x], kd.prove(x + 1 == 1 + x))
|= (Lambda(x, x + 1)) == (Lambda(x, 1 + x))

Parameters:

• vs (list[ExprRef])

• pf (Proof)

Return type:

Proof