spec sp =
sort s
op f:s->s
. forall x:s . f(x) = x
then
. exists x:s . f(x) = x
with s |-> s
end
spec sp1_renamed =
sp hide f
end