Proving9c

    type t
    function f(X:t) : t

    isolate extra = {

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

    isolate t_theory = {

        object spec = {
            property [expanding] f(X) > X
            property [transitivity] X:t < Y & Y < Z -> X < Z
        }

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

    }
    }