Frag11

type t
interpret t -> int

function f(X:t) : t

function foo(X:t) = f(X) = X

definition f(X) = X

function g(X:t) : t
var p : t

function h(X:t) : t
definition h(Z) =  Z
function bar(X:t) = f(X) = h(X)

var q : bool


object test1 = {
    function f(X:t) : t
    function g(X:t,Y:t) : t
    function h(X:t) : t
    var a : t
    var b : t
    axiom g(X1, X2) = 0 | h(X2) = 0
    axiom g(f(X1), b) + 1 <= f(X1)
    axiom h(b) = 1
    axiom f(a) = 0
}

result: OK