Proving7

    type t
    relation succ(X:t,Y:t)

    schema existsE = {
        type t
    relation p(X:t)
        property exists X. p(X)
    fresh function n:t
    #----------------------
    property p(n)
    }

    axiom exists Y. succ(X,Y)

    function next(X:t):t

    property succ(X,next(X))
    proof existsE with n = next(X), p(Y) = succ(X,Y)