Proving9a

    type t
    function f(X:t) : t

    isolate t_theory = {

        object impl = {
            interpret t -> int
        definition f(X) = X + 1
        }

        property [expanding] f(X) > X
    property [transitivity] X:t < Y & Y < Z -> X < Z

    }


    isolate extra = {

        property [prop] f(f(X)) > X

    }
    with t_theory