Full abstraction for the new corrected semantics, proven!
Defined contextual equivalence.
Correct usage of returnback entry point via the stack.