Types.14.expect

text.dfy(3,2): Error: a forall expression involved in a predicate definition is not allowed to depend on the set of allocated references, but values of 'x' (of type 'X') may contain references (perhaps declare its type as 'X(!new)') (see documentation for 'older' parameters)
text.dfy(3,2): Error: a forall expression involved in a predicate definition is not allowed to depend on the set of allocated references, but values of 'y' (of type 'X') may contain references (perhaps declare its type as 'X(!new)') (see documentation for 'older' parameters)
2 resolution/type errors detected in text.dfy