kdrag.kernel.cong
- kdrag.kernel.cong(f: FuncDeclRef, *args: Proof) Proof
Congruence of function symbols. If f is a function symbol, then f(x) == f(y) if x == y.
>>> x = smt.Int("x") >>> y = smt.Real("y") >>> f = smt.Function("f", smt.IntSort(), smt.RealSort(), smt.IntSort()) >>> cong(f, eqrefl(x), eqrefl(y)) |- f(x, y) == f(x, y)