Proving7a

    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)

    property exists Y. succ(X,Y) named next(X)