I hope it is unprovable manually as well, since it's false. See Section 16.1.9 in Specifying Systems.
Yes I see: the semantics doesn't specify if S and << S >> are equal or not.
Thank you.
By the way Z3 accepts
ASSUME NEW S, NEW T \in S
PROVE << T >> \in [ 1..1 -> S ]
But not Isabelle nor CVC3.
--
FL