#lang ivy1.7
type t = {f,g,h}
var x : t
invariant x = f
after init {
x := f
}
action a = {
x := g
export a