assertpf3.ivy

#lang ivy1.7

type t


relation r(X:t,Y:t)

definition r(X,Y) = (X = Y)
theorem [foo] {property exists Y. r(X,Y)}


action a(x:t) = {
    var y : t;
    assert exists Z. r(y,Z) proof assume foo with X=y

}

export a