#lang ivy1.6
type t
type q
function f(X:t) : q
individual a:t, b:t
axiom f(X) = f(Y) + Z
interpret q->int