I don't use Capture(x, Action)', but rather Action(t) is my subaction, _within which_ I can now use the parameter t in any formula -- primed or not -- and know that it's a constant that is equal to the current value of x.
So, if
VARIABLE x, y
Foo(a) == a + y
I can do:
Next == Capture(x, LAMBDA t:
/\ ... Foo(t) .... \* = x + y
/\ ...
/\ ... Foo(t)' ....) \* = x + y'
So Capture is a capturing/lowering LET (with the caveat that it can only be used in binary valued formulas), which is exactly what I wanted.
Ron