Make choice of handler deterministic.
Fix order of variables in typing environments.
Type preservation proof.