#lang ivy1.6
type t
relation p(X:t)
init p(X) <-> X = 1
action foo = {
if some x:t. p(x) {
call bar(x)
}
action bar(x:t)
interpret t -> bv[1]
export foo
import bar