this is a pass that takes care of the problem with `MUT?`, which is a
non-functional expression (denotes multiple values), and thus cannot be
compiled like this to functional backends (proof backends).

Here is its effect:
```diff
 relation Global_ok: `%|-%:%`(context, global, globaltype)
   ;; 3-typing.watsup:414.1-418.40
-  rule _ {C : context, expr : expr, gt : globaltype, t : valtype}:
+  rule _ {C : context, expr : expr, gt : globaltype, t : valtype, w0 : ()?}:
     `%|-%:%`(C, GLOBAL(gt, expr), gt)
     -- Globaltype_ok: `|-%:OK`(gt)
-    -- if (gt = `MUT%?%`(()?{}, t))
+    -- if (gt = `MUT%?%`(w0, t))
     -- Expr_ok_const: `%|-%:%CONST`(C, expr, t)
```