Bigger

type t

relation (X:t < Y:t)
individual (X:t + Y:t) : t

axiom X:t < Y & Y < Z -> X < Z

interpret t -> int

module foo = {
    action incr(input:t) returns (output:t) = {
        output := input + 1
    }
}

module bar(f) = {
    individual x : t, y : t

    init x = y

    action step = {
    y := f.incr(y);
    assert x < y
    }

    conjecture x < y | x = y
}

instantiate f : foo
instantiate b : bar(f)

export b.step

all following here is proof

module bigger = {
    action incr(input:t) returns (output:t) = {
        assert input < output
    }
    mixin incr after f.incr
}

instantiate bg : bigger

isolate iso_b = b with bg
isolate iso_f = f with bg,t