it may help
to observe that if Foo is defined by
Foo(a, b) == a' = e1 /\ b' = e2
Then \E t : (t=x) /\ Foo(t,y)' is equivalent to Foo(x, y').
Thosetwo formulas are not equivalent. The second determines the value of
x'. The first tells you very little about the value of x'. All it tells
you are the values of x'[t] for t \in DOMAIN x. It tells you nothing
about the domain of x'. It doesn't even tell you if x' is a function.
Hence, it's not a sensible formula--at least, not by itself. The following
formula is equivalent to the second one:
/\ x' = [t \in DOMAIN x |-> x'[t]]
/\ \A t \in DOMAIN x : x'[t] = e
but it's hardly simper than the second one.
So, as I wrote before, when TLC doesn't allow you to write something
you think it should, then it's often the case that what you wrote
isn't what you meant to write. You should learn to read what a
formula says rather than what you want it to say. This requires that
you stop thinking of TLA+ formula as a program and start thinking of
it as a mathematical assertion.
Occasionally, this is difficult. For
example, if you writef[n \in Nat] == IF n = 0 THEN x ELSE f[n-1]'
it's not easy to realize that if x is a variable, then f is not
equal to the illegal _expression_ (x')'.