Lettac1

type t

var x : t

invariant true proof let X = x, Y = x

action a =
{
}

export a