#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