diff --git a/compiler/backend/languages/semantics/thunkLangPropsScript.sml b/compiler/backend/languages/semantics/thunkLangPropsScript.sml
index f2d73ec7..6cb240e5 100644
--- a/compiler/backend/languages/semantics/thunkLangPropsScript.sml
+++ b/compiler/backend/languages/semantics/thunkLangPropsScript.sml
@@ -17,9 +17,9 @@ val _ = set_grammar_ancestry ["thunkLang", "pure_misc", "thunk_semantics"];
 val _ = numLib.prefer_num ();
 
 Theorem exp_size_lemma:
-  (∀x xs. MEM x xs ⇒ exp_size x ≤ exp4_size xs) ∧
+  (∀x xs. MEM x xs ⇒ exp_size x ≤ exp3_size xs) ∧
   (∀x y xs. MEM (x,y) xs ⇒ exp_size y ≤ exp1_size xs) ∧
-  (∀x xs. MEM x xs ⇒ v_size x < exp5_size xs)
+  (∀x xs. MEM x xs ⇒ v_size x < exp4_size xs)
 Proof
   rpt conj_tac
   \\ Induct_on ‘xs’ \\ rw []
@@ -41,7 +41,6 @@ Definition no_value_def:
   (no_value (App x y) = (no_value x ∧ no_value y)) ∧
   (no_value (Lam s x) = no_value x) ∧
   (no_value (Let opt x y) = (no_value x ∧ no_value y)) ∧
-  (no_value (Box x) = no_value x) ∧
   (no_value (MkTick x) = no_value x) ∧
   (no_value (Letrec f x) = (no_value x ∧ EVERY no_value (MAP SND f) ∧ EVERY ok_bind (MAP SND f))) ∧
   (no_value (Value v) = F) ∧
@@ -125,7 +124,6 @@ Theorem exp_ind:
     (∀v x y. P x ∧ P y ⇒ P (Let v x y)) ∧
     (∀f x. (∀n x'. MEM (n,x') f ⇒ P x') ∧ P x ⇒ P (Letrec f x)) ∧
     (∀x. P x ⇒ P (Delay x)) ∧
-    (∀x. P x ⇒ P (Box x)) ∧
     (∀x. P x ⇒ P (Force x)) ∧
     (∀v. P (Value v)) ∧
     (∀x. P x ⇒ P (MkTick x)) ⇒
@@ -263,7 +261,6 @@ Theorem closed_simps[simp]:
   (∀mop xs. closed (Monad mop xs) ⇔ EVERY closed xs) ∧
   (∀x. closed (Force x) ⇔ closed x)  ∧
   (∀x. closed (Delay x) ⇔ closed x)  ∧
-  (∀x. closed (Box x) ⇔ closed x)  ∧
   (∀v. closed (Value v) ⇔ T)  ∧
   (∀x. closed (MkTick x) ⇔ closed x) ∧
   (∀v. closed (Var v) ⇔ F)
@@ -360,8 +357,6 @@ Proof
     \\ simp [AC CONJ_COMM CONJ_ASSOC, SF DNF_ss])
   >- ((* Delay *)
     gs [freevars_def, subst_def])
-  >- ((* Box *)
-    gs [freevars_def, subst_def])
   >- ((* Force *)
     gs [freevars_def, subst_def])
   >- ((* Value *)
@@ -1186,10 +1181,8 @@ Theorem eval_Force:
     case dest_Tick v of
       NONE =>
         do
-          (wx,binds) <- dest_anyThunk v;
-          case wx of
-            INL v => return v
-          | INR y => eval (subst_funs binds y)
+          (y,binds) <- dest_anyThunk v;
+          eval (subst_funs binds y)
         od
     | SOME w => eval (Force (Value w))
 Proof
@@ -1204,7 +1197,6 @@ Proof
     >- (
       Cases_on ‘dest_anyThunk v’ \\ gs []
       \\ pairarg_tac \\ gvs []
-      \\ CASE_TAC \\ gs []
       \\ irule eval_to_equals_eval \\ gs [])
     \\ irule eval_to_equals_eval \\ gs [])
   \\ Cases_on ‘dest_Tick v’ \\ gs []
@@ -1216,7 +1208,6 @@ Proof
       first_x_assum (qspec_then ‘1’ assume_tac)
       \\ Cases_on ‘v’ \\ gs [])
     \\ pairarg_tac \\ gvs []
-    \\ CASE_TAC \\ gs []
     \\ simp [eval_def]
     \\ DEEP_INTRO_TAC some_intro \\ rw []
     \\ first_x_assum (qspec_then ‘x + 1’ assume_tac) \\ gs [])
diff --git a/compiler/backend/languages/semantics/thunkLangScript.sml b/compiler/backend/languages/semantics/thunkLangScript.sml
index f2f2e8c1..ef87a6cc 100644
--- a/compiler/backend/languages/semantics/thunkLangScript.sml
+++ b/compiler/backend/languages/semantics/thunkLangScript.sml
@@ -5,12 +5,11 @@
    thunkLang is the next language in the compiler after pureLang.
    - It has a call-by-value semantics.
    - It extends the pureLang syntax with explicit syntax for delaying and
-     forcing computations (“Delay” and “Force”) and “Thunk” values. Non-
-     suspended thunks can be created with “Box”.
+     forcing computations (“Delay” and “Force”) and “Thunk” values.
    - Suspended computations can be wrapped in “MkTick” to cause the suspended
      evaluation to consume one extra clock tick by producing a value wrapped in
      “DoTick”.
-   - Any expression bound by a Letrec must be one of “Lam”, “Delay” or “Box”.
+   - Any expression bound by a Letrec must be one of “Lam”, “Delay”.
    - thunkLang has a substitution-based semantics. See [envLangScript.sml]
      for the next language in the compiler, which has an environment-based
      semantics.
@@ -36,7 +35,6 @@ Datatype:
       | Let (vname option) exp exp               (* non-recursive let       *)
       | If exp exp exp                           (* if-then-else            *)
       | Delay exp                                (* suspend in a Thunk      *)
-      | Box exp                                  (* wrap result in a Thunk  *)
       | Force exp                                (* evaluates a Thunk       *)
       | Value v                                  (* for substitution        *)
       | MkTick exp;                              (* creates a delayed Tick  *)
@@ -45,7 +43,7 @@ Datatype:
     | Monadic mop (exp list)
     | Closure vname exp
     | Recclosure ((vname # exp) list) vname
-    | Thunk (v + exp)
+    | Thunk exp
     | Atom lit
     | DoTick v                                   (* extra clock when forced *)
 End
@@ -83,7 +81,6 @@ Definition subst_def:
     (let m1 = FILTER (λ(n, v). ¬MEM n (MAP FST f)) m in
        Letrec (MAP (λ(n, x). (n, subst m1 x)) f) (subst m1 x)) ∧
   subst m (Delay x) = Delay (subst m x) ∧
-  subst m (Box x) = Box (subst m x) ∧
   subst m (Force x) = Force (subst m x) ∧
   subst m (Value v) = Value v ∧
   subst m (MkTick x) = MkTick (subst m x)
@@ -124,7 +121,6 @@ Theorem subst1_def:
      else
        Letrec (MAP (λ(f, x). (f, subst1 n v x)) f) (subst1 n v x)) ∧
   subst1 n v (Delay x) = Delay (subst1 n v x) ∧
-  subst1 n v (Box x) = Box (subst1 n v x) ∧
   subst1 n v (Force x) = Force (subst1 n v x) ∧
   subst1 n v (Value w) = Value w ∧
   subst1 n v (MkTick x) = MkTick (subst1 n v x)
@@ -179,7 +175,7 @@ Definition dest_anyThunk_def:
     do
       (f, n) <- dest_Recclosure v;
       case ALOOKUP (REVERSE f) n of
-        SOME (Delay x) => return (INR x, f)
+        SOME (Delay x) => return (x, f)
       | _ => fail Type_error
     od
 End
@@ -202,7 +198,6 @@ Definition freevars_def:
     ((freevars x ∪ BIGUNION (set (MAP (λ(n, x). freevars x) f))) DIFF
      set (MAP FST f)) ∧
   freevars (Delay x) = freevars x ∧
-  freevars (Box x) = freevars x ∧
   freevars (Force x) = freevars x ∧
   freevars (Value v) = ∅ ∧
   freevars (MkTick x) = freevars x
@@ -227,7 +222,6 @@ Definition boundvars_def:
     ((boundvars x ∪ BIGUNION (set (MAP (λ(n, x). boundvars x) f))) ∪
      set (MAP FST f)) ∧
   boundvars (Delay x) = boundvars x ∧
-  boundvars (Box x) = boundvars x ∧
   boundvars (Force x) = boundvars x ∧
   boundvars (Value v) = ∅ ∧
   boundvars (MkTick x) = boundvars x
@@ -281,12 +275,7 @@ Definition eval_to_def:
   eval_to k (Letrec funs x) =
     (if k = 0 then fail Diverge else
        eval_to (k - 1) (subst_funs funs x)) ∧
-  eval_to k (Delay x) = return (Thunk (INR x)) ∧
-  eval_to k (Box x) =
-    (do
-       v <- eval_to k x;
-       return (Thunk (INL v))
-     od) ∧
+  eval_to k (Delay x) = return (Thunk x) ∧
   eval_to k (Force x) =
     (if k = 0 then fail Diverge else
        do
@@ -294,10 +283,8 @@ Definition eval_to_def:
          case dest_Tick v of
            SOME w => eval_to (k - 1) (Force (Value w))
          | NONE =>
-             do (wx, binds) <- dest_anyThunk v;
-                case wx of
-                  INL v => return v
-                | INR y => eval_to (k - 1) (subst_funs binds y)
+             do (y, binds) <- dest_anyThunk v;
+                eval_to (k - 1) (subst_funs binds y)
              od
        od) ∧
   eval_to k (MkTick x) =
@@ -377,7 +364,6 @@ Theorem eval_to_ind:
     (∀k funs x.
       (k ≠ 0 ⇒ P (k − 1) (subst_funs funs x)) ⇒ P k (Letrec funs x)) ∧
     (∀k x. P k (Delay x)) ∧
-    (∀k x. P k x ⇒ P k (Box x)) ∧
     (∀k x.
       (∀y binds.
          k ≠ 0 ⇒
@@ -476,9 +462,6 @@ Proof
     rw [eval_to_def, subst_funs_def])
   >- ((* Delay *)
     rw [eval_to_def])
-  >- ((* Box *)
-    rw [eval_to_def]
-    \\ Cases_on ‘eval_to k x’ \\ fs [])
   >- ((* Force *)
     rw []
     \\ rgs [Once eval_to_def]
@@ -488,8 +471,8 @@ Proof
     \\ Cases_on ‘eval_to k x’ \\ fs []
     \\ BasicProvers.TOP_CASE_TAC \\ gs []
     \\ Cases_on ‘dest_anyThunk y’ \\ gs []
-    \\ pairarg_tac \\ gvs []
-    \\ BasicProvers.TOP_CASE_TAC \\ gs [])
+    \\ pairarg_tac \\ gvs [])
+    (* \\ BasicProvers.TOP_CASE_TAC \\ gs []) *)
   >- ((* MkTick *)
     rw [eval_to_def]
     \\ Cases_on ‘eval_to k x’ \\ fs [])
@@ -585,11 +568,6 @@ Definition is_Delay_def[simp]:
   (is_Delay _ = F)
 End
 
-Definition is_Box_def[simp]:
-  (is_Box (Box x) = T) ∧
-  (is_Box _ = F)
-End
-
 Definition ok_bind_def[simp]:
   (ok_bind (Lam _ _) = T) ∧
   (ok_bind (Delay _) = T) ∧
diff --git a/compiler/backend/languages/semantics/thunk_exp_ofScript.sml b/compiler/backend/languages/semantics/thunk_exp_ofScript.sml
index db23e82c..de116015 100644
--- a/compiler/backend/languages/semantics/thunk_exp_ofScript.sml
+++ b/compiler/backend/languages/semantics/thunk_exp_ofScript.sml
@@ -56,8 +56,7 @@ Definition exp_of_def[simp]:
         (MAP (λ(c,vs,x). (explode c,MAP explode vs,exp_of x)) rs)
         (OPTION_MAP (λ(a,e). (MAP (explode ## I) a, exp_of e)) d) ∧
   exp_of (Force x)       = Force (exp_of x) ∧
-  exp_of (Delay x)       = Delay (exp_of x) ∧
-  exp_of (Box x)         = Box (exp_of x)
+  exp_of (Delay x)       = Delay (exp_of x)
 Termination
   WF_REL_TAC ‘measure cexp_size’ >> rw [cexp_size_eq]
 End
@@ -83,7 +82,6 @@ Definition cexp_wf_def:
   cexp_wf (App e es) = (cexp_wf e ∧ EVERY cexp_wf es ∧ es ≠ []) ∧
   cexp_wf (Force e) = cexp_wf e ∧
   cexp_wf (Delay e) = cexp_wf e ∧
-  cexp_wf (Box e) = cexp_wf e ∧
   cexp_wf (Lam vs e) = (cexp_wf e ∧ vs ≠ []) ∧
   cexp_wf (Let v e1 e2) = (cexp_wf e1 ∧ cexp_wf e2) ∧
   cexp_wf (Letrec fns e) = (EVERY (λ(_,x). cexp_ok_bind x ∧ cexp_wf x) fns ∧ cexp_wf e
diff --git a/compiler/backend/languages/thunk_cexpScript.sml b/compiler/backend/languages/thunk_cexpScript.sml
index b9592b9d..ab209297 100644
--- a/compiler/backend/languages/thunk_cexpScript.sml
+++ b/compiler/backend/languages/thunk_cexpScript.sml
@@ -25,7 +25,6 @@ Datatype:
        | Case name ((name # (name list) # cexp) list)    (* pattern match        *)
                     (((name # num) list # cexp) option)  (* optional fallthrough *)
        | Delay cexp                   (* delay a computation as a thunk          *)
-       | Box cexp                     (* eagerly compute, but wrap as a thunk    *)
        | Force cexp                   (* force a thunk                           *)
 End
 
@@ -60,7 +59,6 @@ Definition cns_arities_def:
       | SOME (a,e) =>
         (set (MAP (λ(cn,ar). explode cn, ar) a) ∪ css_cn_ars) INSERT cns_arities e) ∪
     BIGUNION (set (MAP (λ(cn,vs,e). cns_arities e) css))) ∧
-  cns_arities (Box e) = cns_arities e ∧
   cns_arities (Delay e) = cns_arities e ∧
   cns_arities (Force e) = cns_arities e
 Termination
diff --git a/compiler/backend/passes/proofs/pure_to_thunk_1ProofScript.sml b/compiler/backend/passes/proofs/pure_to_thunk_1ProofScript.sml
index eb212fc7..a5e9e53b 100644
--- a/compiler/backend/passes/proofs/pure_to_thunk_1ProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_to_thunk_1ProofScript.sml
@@ -24,9 +24,8 @@ val _ = numLib.prefer_num ();
 
   As pureLang is lazy it allows non-functional value declarations that are
   mutually recursive, and lazy value declarations. All such computations are
-  suspended thunkLang-side by Lam, Box or Delay. This relation (exp_rel) acts as
-  if the compiler inserted Delay everywhere, but the compiler can insert Box
-  for things that do not require a thunk to be allocated, such as a lambda.
+  suspended thunkLang-side by Lam or Delay. This relation (exp_rel) acts as
+  if the compiler inserted Delay everywhere.
 
   * [Var]
     - All variables are wrapped in ‘Force’ as if they were suspended either by
@@ -71,10 +70,10 @@ val _ = numLib.prefer_num ();
     - `Bind`/`Handle` are straightforwardly compiled
   * [Letrec]
     - We expect all expressions in the list of bindings to be suspended by
-      something (either Lam or Delay or Box), so we insert Delay everywhere.
+      something (either Lam or Delay), so we insert Delay everywhere.
  *)
 
-Overload Suspend[local] = “λx. Force (Value (Thunk (INR x)))”;
+Overload Suspend[local] = “λx. Force (Value (Thunk x))”;
 
 Overload Rec[local] = “λf n. Force (Value (Recclosure f n))”;
 
@@ -218,7 +217,7 @@ End
 
 Definition thunk_rel_def:
   thunk_rel x v ⇔
-    ∃y. v = Thunk (INR y) ∧
+    ∃y. v = Thunk y ∧
         exp_rel x y ∧
         closed x
 End
@@ -464,7 +463,7 @@ Theorem exp_rel_subst:
     exp_rel a b ∧
     closed a ⇒
       exp_rel (subst1 n (Tick a) x)
-              (subst1 n (Thunk (INR b)) y)
+              (subst1 n (Thunk b) y)
 Proof
   ho_match_mp_tac exp_ind_alt \\ rw []
   >- ((* Var *)
@@ -2610,7 +2609,7 @@ Proof
 QED
 
 Triviality eval_simps[simp]:
-  eval (Delay e) = INR (Thunk (INR e)) ∧
+  eval (Delay e) = INR (Thunk e) ∧
   eval (Lit l) = INR (Atom l) ∧
   eval (Monad mop es) = INR (Monadic mop es) ∧
   eval (Lam x body) = INR (Closure x body) ∧
diff --git a/compiler/backend/passes/proofs/thunk_Delay_LamScript.sml b/compiler/backend/passes/proofs/thunk_Delay_LamScript.sml
index 8a97311d..80eb6ba2 100644
--- a/compiler/backend/passes/proofs/thunk_Delay_LamScript.sml
+++ b/compiler/backend/passes/proofs/thunk_Delay_LamScript.sml
@@ -80,10 +80,6 @@ Inductive exp_rel:
   (∀x y.
      exp_rel x y ⇒
        exp_rel (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀x y.
-     exp_rel x y ⇒
-       exp_rel (Box x) (Box y)) ∧
 [~Force:]
   (∀x y.
      exp_rel x y ⇒
@@ -135,18 +131,14 @@ Inductive exp_rel:
      i < LENGTH vL ∧ SND (EL i f) = Delay (Lam s ef) ∧ EL i bL ⇒
      v_rel (Closure s (subst (FILTER (λ(v,e). v≠s) (MAP (λ(v,x).(v, Recclosure f v)) f)) ef))
            (Recclosure (FLAT $ MAP2 unfold_Delay_Lam g (ZIP (vL, bL))) (EL i vL))) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w))) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      exp_rel x y ⇒
-     v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
-[v_rel_Thunk_INR_Lam:]
+     v_rel (Thunk x) (Thunk y)) ∧
+[v_rel_Thunk_Lam:]
   (∀x y s.
      exp_rel x y ⇒
-     v_rel (Thunk (INR (Lam s x))) (Thunk (INR (Value (Closure s y))))) ∧
+     v_rel (Thunk (Lam s x)) (Thunk (Value (Closure s y)))) ∧
 [v_rel_Atom:]
   (∀x.
      v_rel (Atom x) (Atom x)) ∧
@@ -170,7 +162,6 @@ Theorem exp_rel_def =
    “exp_rel (Let s x y) z”,
    “exp_rel (If x y z) w”,
    “exp_rel (Delay x) y”,
-   “exp_rel (Box x) y”,
    “exp_rel (MkTick x) y”,
    “exp_rel (Force x) y”,
    “exp_rel (Monad m xs) x”]
@@ -541,7 +532,6 @@ Proof
   >- first_x_assum $ drule_then irule
   >- first_x_assum $ drule_then irule
   >- first_x_assum $ drule_then irule
-  >- first_x_assum $ drule_then irule
 QED
 
 Theorem subst_Letrec_Delay:
@@ -765,9 +755,6 @@ Proof
   >~ [‘Delay x’] >- (
     rw [subst_def]
     \\ gs [exp_rel_Delay])
-  >~ [‘Box x’] >- (
-    rw [subst_def]
-    \\ gs [exp_rel_Box])
   >~ [‘Force x’] >- (
     rw [subst_def]
     \\ gs [exp_rel_Force])
@@ -1105,10 +1092,6 @@ Proof
           gvs [] >> first_x_assum $ irule >>
           gvs [EVERY_CONJ, freevars_def, boundvars_def, EVERY_MEM]))
   >~[‘Delay x’]
-  >- (gvs [exp_rel_def, subst_def] >>
-      last_x_assum $ irule >>
-      gvs [freevars_def, boundvars_def])
-  >~[‘Box x’]
   >- (gvs [exp_rel_def, subst_def] >>
       last_x_assum $ irule >>
       gvs [freevars_def, boundvars_def])
@@ -1435,11 +1418,11 @@ Proof
       \\ Cases_on ‘x1’ \\ fs [is_Lam_def, Once exp_rel_def, eval_to_def, subst_def, PULL_EXISTS]
       \\ Q.REFINE_EXISTS_TAC ‘j + n’
       \\ qexists_tac ‘1’ \\ gvs [subst1_notin_frees]
-      \\ rename1 ‘_ (eval_to _ (subst1 m (Thunk (INR (Lam s x1))) y1))
-                  (eval_to _ (subst1 _ (Thunk (INR (Value (Closure s x2)))) y2))’
-      \\ ‘exp_rel (subst1 m (Thunk (INR (Lam s x1))) y1)
-                  (subst1 m (Thunk (INR (Value (Closure s x2)))) y2)’
-        by (irule exp_rel_subst \\ gs [v_rel_Thunk_INR_Lam])
+      \\ rename1 ‘_ (eval_to _ (subst1 m (Thunk (Lam s x1)) y1))
+                  (eval_to _ (subst1 _ (Thunk (Value (Closure s x2))) y2))’
+      \\ ‘exp_rel (subst1 m (Thunk (Lam s x1)) y1)
+                  (subst1 m (Thunk (Value (Closure s x2))) y2)’
+        by (irule exp_rel_subst \\ gs [v_rel_Thunk_Lam])
       \\ last_x_assum $ dxrule_then $ qx_choose_then ‘j1’ assume_tac
       \\ qexists_tac ‘j1’ \\ gvs [])
     \\ IF_CASES_TAC \\ gs []
@@ -1557,16 +1540,6 @@ Proof
     \\ pairarg_tac \\ gvs [])
  >~ [‘Delay x’] >- (
     gvs [Once exp_rel_def, eval_to_def, v_rel_def])
-  >~ [‘Box x’] >- (
-    gvs [Once exp_rel_def, eval_to_def]
-    \\ rename1 ‘exp_rel x y’
-    \\ ‘∃j. ($= +++ v_rel) (eval_to k x) (eval_to (j + k) y)’
-      suffices_by (
-        disch_then (qx_choose_then ‘j’ assume_tac)
-        \\ qexists_tac ‘j’
-        \\ Cases_on ‘eval_to k x’ \\ Cases_on ‘eval_to (j + k) y’ \\ gs []
-        \\ simp [v_rel_def])
-    \\ first_x_assum (irule_at Any) \\ gs [])
   >~ [‘Force x’] >- (
     rgs [Once exp_rel_def]
     \\ once_rewrite_tac [eval_to_def] \\ simp []
@@ -1625,8 +1598,8 @@ Proof
             \\ Cases_on ‘EL n2 xs’ \\ gvs []
             \\ rename1 ‘EL n _’ \\ Cases_on ‘SND (EL n xs)’ \\ gvs [exp_rel_def]))
       \\ pairarg_tac \\ gvs []
-      \\ Cases_on ‘∃s x y. v1 = Thunk (INR (Lam s x)) ∧
-                           w1 = Thunk (INR (Value (Closure s y))) ∧ exp_rel x y’
+      \\ Cases_on ‘∃s x y. v1 = Thunk (Lam s x) ∧
+                           w1 = Thunk (Value (Closure s y)) ∧ exp_rel x y’
       \\ gs []
       >- (gvs [dest_anyThunk_def, subst_funs_def, subst_empty]
           \\ qexists_tac ‘j’ \\ gs []
@@ -1760,13 +1733,6 @@ Proof
             by (gen_tac \\ irule LIST_REL_OPTREL
                 \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, LIST_EQ_REWRITE, EL_MAP])
           \\ gvs [OPTREL_def]
-          \\ CASE_TAC
-          >- (qexists_tac ‘j’
-              \\ gvs [dest_anyThunk_def]
-              \\ rename1 ‘ALOOKUP _ n’ \\ first_x_assum $ qspecl_then [‘n’] assume_tac
-              \\ gvs []
-              \\ rename1 ‘exp_rel x0 _’
-              \\ Cases_on ‘x0’ \\ gvs [exp_rel_def])
           \\ rename1 ‘subst_funs binds y1’
           \\ Cases_on ‘eval_to (k - 1) (subst_funs binds y1) = INL Diverge’ \\ gs []
           >- (qexists_tac ‘0’
@@ -1830,8 +1796,9 @@ Proof
             by (irule eval_to_mono \\ gvs []
                 \\ strip_tac \\ Cases_on ‘eval_to (k - 1) (subst_funs binds y1)’ \\ gs [])
           \\ gvs [])
+      \\ rename1 ‘dest_anyThunk v1 = INR (wx, binds)’
       \\ ‘∃wx' binds'. dest_anyThunk w1 = INR (wx', binds') ∧
-                       (v_rel +++ exp_rel) wx wx' ∧
+                       exp_rel wx wx' ∧
                        MAP FST binds = MAP FST binds' ∧
                        EVERY ok_bind (MAP SND binds) ∧
                        EVERY ok_bind (MAP SND binds') ∧
@@ -1851,12 +1818,6 @@ Proof
             \\ gvs [EVERY_EL, EL_MAP]
             \\ first_x_assum (drule_then assume_tac)
             \\ gvs [ok_bind_def])
-      \\ CASE_TAC \\ gs []
-      >- (
-        qexists_tac ‘j’ \\ simp []
-        \\ CASE_TAC \\ gs []
-        \\ Cases_on ‘v1’ \\ Cases_on ‘w1’ \\ gs [dest_anyThunk_def])
-      \\ Cases_on ‘wx'’ \\ gs []
       \\ rename1 ‘exp_rel x1 x2’
       \\ ‘exp_rel (subst_funs binds x1) (subst_funs binds' x2)’
         by (simp [subst_funs_def]
diff --git a/compiler/backend/passes/proofs/thunk_Forcing_LambdasScript.sml b/compiler/backend/passes/proofs/thunk_Forcing_LambdasScript.sml
index 4e953992..21b760ac 100644
--- a/compiler/backend/passes/proofs/thunk_Forcing_LambdasScript.sml
+++ b/compiler/backend/passes/proofs/thunk_Forcing_LambdasScript.sml
@@ -151,10 +151,6 @@ Inductive forcing_lam_rel:
   (∀set x y.
      forcing_lam_rel set x y ⇒
        forcing_lam_rel set (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀set x y.
-     forcing_lam_rel set x y ⇒
-       forcing_lam_rel set (Box x) (Box y)) ∧
 [~Force:]
   (∀set x y.
      forcing_lam_rel set x y ⇒
@@ -173,7 +169,6 @@ Theorem forcing_lam_rel_def =
    “forcing_lam_rel s (Let opt x y) z”,
    “forcing_lam_rel s (If x y z) w”,
    “forcing_lam_rel s (Delay x) y”,
-   “forcing_lam_rel s (Box x) y”,
    “forcing_lam_rel s (MkTick x) y”,
    “forcing_lam_rel s (Force x) y”]
   |> map (SIMP_CONV (srw_ss()) [Once forcing_lam_rel_cases])
@@ -902,13 +897,6 @@ Proof
       irule_at (Pos last) clean_rel_Delay >>
       simp [boundvars_def] >>
       metis_tac [])
-  >- (gs [boundvars_def] >>
-      gs [boundvars_def] >>
-      irule_at Any force_arg_rel_Box >>
-      irule_at Any combine_rel_Box >>
-      irule_at (Pos last) clean_rel_Box >>
-      irule_at (Pos last) clean_rel_Box >>
-      simp [boundvars_def] >> metis_tac [])
   >- (gs [boundvars_def] >>
       irule_at Any force_arg_rel_Force >>
       irule_at Any combine_rel_Force >>
diff --git a/compiler/backend/passes/proofs/thunk_Let_Delay_VarScript.sml b/compiler/backend/passes/proofs/thunk_Let_Delay_VarScript.sml
index 0ee83a61..ea872860 100644
--- a/compiler/backend/passes/proofs/thunk_Let_Delay_VarScript.sml
+++ b/compiler/backend/passes/proofs/thunk_Let_Delay_VarScript.sml
@@ -33,7 +33,6 @@ Definition replace_Force_def:
                                           then Let (SOME s) (replace_Force expr v e1) e2
                                           else Let (SOME s) (replace_Force expr v e1) (replace_Force expr v e2)) ∧
   (replace_Force expr v (Delay e) = Delay (replace_Force expr v e)) ∧
-  (replace_Force expr v (Box e) = Box (replace_Force expr v e)) ∧
   (replace_Force expr v (MkTick e) = MkTick (replace_Force expr v e)) ∧
   (replace_Force expr v (Value val) = Value val) ∧
   (replace_Force expr v (Force e) = Force (replace_Force expr v e)) ∧
@@ -61,7 +60,6 @@ Definition unreplace_Force_def:
                                               else Let (SOME s) (unreplace_Force w v e1)
                                                        (unreplace_Force w v e2)) ∧
   (unreplace_Force w v (Delay e) = Delay (unreplace_Force w v e)) ∧
-  (unreplace_Force w v (Box e) = Box (unreplace_Force w v e)) ∧
   (unreplace_Force w v (MkTick e) = MkTick (unreplace_Force w v e)) ∧
   (unreplace_Force w v (Value val) = Value val) ∧
   (unreplace_Force w v (Force e) = Force (unreplace_Force w v e)) ∧
@@ -225,10 +223,6 @@ Inductive exp_rel:
   (∀x y.
      exp_rel x y ⇒
        exp_rel (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀x y.
-     exp_rel x y ⇒
-       exp_rel (Box x) (Box y)) ∧
 [~Force:]
   (∀x y.
      exp_rel x y ⇒
@@ -238,7 +232,7 @@ Inductive exp_rel:
 [~Force_Value:]
   (∀v1 v2.
      v_rel v1 v2 ⇒
-     exp_rel (Force (Value (Thunk (INR (Value v1))))) (Value v2)) ∧
+     exp_rel (Force (Value (Thunk (Value v1)))) (Value v2)) ∧
 [v_rel_Constructor:]
   (∀s vs ws.
      LIST_REL v_rel vs ws ⇒
@@ -279,14 +273,10 @@ Inductive exp_rel:
      MEM v2 (MAP FST f) ∧ MEM (v1, Delay (Var v2)) f ⇒
      exp_rel (Force (Value (Recclosure f v1)))
              (Value (Recclosure (MAP (λ(v,e). (v, replace_Force (Var v2) v1 e)) g) v2))) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w))) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      exp_rel x y ⇒
-     v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
+     v_rel (Thunk x) (Thunk y)) ∧
 [v_rel_Atom:]
   (∀x.
      v_rel (Atom x) (Atom x)) ∧
@@ -307,7 +297,6 @@ Theorem exp_rel_def =
    “exp_rel (Let s x y) z”,
    “exp_rel (If x y z) w”,
    “exp_rel (Delay x) y”,
-   “exp_rel (Box x) y”,
    “exp_rel (MkTick x) y”,
    “exp_rel (Force x) y”]
   |> map (SIMP_CONV (srw_ss()) [Once exp_rel_cases])
@@ -768,9 +757,6 @@ Proof
   >~ [‘Delay x’] >- (
     rw [subst_def]
     \\ gs [exp_rel_Delay])
-  >~ [‘Box x’] >- (
-    rw [subst_def]
-    \\ gs [exp_rel_Box])
   >>~[‘Force (Value _)’]
   >- (rw [subst_def]
       \\ gs [exp_rel_Force_Value])
@@ -1066,14 +1052,14 @@ QED
 Theorem exp_rel_subst_replace_Force:
   ∀x y v w n.
     exp_rel x y ∧ v_rel v w ⇒
-    exp_rel (subst1 n (Thunk (INR (Value v))) x)
-            (subst1 n (Thunk (INR (Value w))) (replace_Force (Value w) n y))
+    exp_rel (subst1 n (Thunk (Value v)) x)
+            (subst1 n (Thunk (Value w)) (replace_Force (Value w) n y))
 Proof
   ‘(∀x y.
       exp_rel x y ⇒
       ∀v w n. v_rel v w ⇒
-              exp_rel (subst1 n (Thunk (INR (Value v))) x)
-                      (subst1 n (Thunk (INR (Value w))) (replace_Force (Value w) n y))) ∧
+              exp_rel (subst1 n (Thunk (Value v)) x)
+                      (subst1 n (Thunk (Value w)) (replace_Force (Value w) n y))) ∧
    (∀v w. v_rel v w ⇒ T)’
     suffices_by rw []
   \\ ho_match_mp_tac exp_rel_strongind \\ rw []
@@ -1121,7 +1107,7 @@ Proof
           \\ gvs [EL_MAP]
           \\ Cases_on ‘EL n2 f’ \\ gs [])
       \\ rw []
-      \\ qspecl_then [‘replace_Force (Value w) n y’, ‘Var v2’, ‘v1’, ‘[(n, Thunk (INR (Value w)))]’]
+      \\ qspecl_then [‘replace_Force (Value w) n y’, ‘Var v2’, ‘v1’, ‘[(n, Thunk (Value w))]’]
                      mp_tac subst_replace_Force
       \\ impl_tac
       >- (gvs [freevars_def]
@@ -1134,10 +1120,10 @@ Proof
           \\ gvs [MEM_MAP]
           \\ first_x_assum $ irule_at Any \\ gs [])
       \\ rw [subst_def] \\ gs []
-      \\ qsuff_tac ‘MAP (λ(p1,p2).(p1, subst1 n (Thunk (INR (Value w)))
+      \\ qsuff_tac ‘MAP (λ(p1,p2).(p1, subst1 n (Thunk (Value w))
                                               (replace_Force (Value w) n (replace_Force (Var v2) v1 p2)))) g
                     = MAP (λ(p1, p2). (p1, replace_Force (Var v2) v1 p2))
-                          (MAP (λ(p1,p2).(p1,subst1 n (Thunk (INR (Value w))) (replace_Force (Value w) n p2))) g)’
+                          (MAP (λ(p1,p2).(p1,subst1 n (Thunk (Value w)) (replace_Force (Value w) n p2))) g)’
       >- (rw []
           \\ irule exp_rel_Letrec_Delay_Var
           \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM, GSYM SND_THM,
@@ -1183,7 +1169,7 @@ Proof
           \\ gvs [MEM_MAP]
           \\ first_x_assum $ irule_at Any \\ gs [])
       \\ rw []
-      \\ qspecl_then [‘replace_Force (Value w) n p2’, ‘Var v2’, ‘v1’, ‘[(n, Thunk (INR (Value w)))]’]
+      \\ qspecl_then [‘replace_Force (Value w) n p2’, ‘Var v2’, ‘v1’, ‘[(n, Thunk (Value w))]’]
                      mp_tac subst_replace_Force
       \\ impl_tac
       >- (gvs [freevars_def]
@@ -1208,7 +1194,7 @@ Proof
           \\ rename1 ‘replace_Force (Value w) n (replace_Force (Var v2) v1 y2)’
           \\ qspecl_then [‘y2’, ‘Value w’, ‘Var v2’, ‘n’, ‘v1’] assume_tac replace_Force_COMM
           \\ gvs [freevars_def]
-          \\ qspecl_then [‘replace_Force (Value w) n y2’, ‘Var v2’, ‘v1’, ‘[(n, Thunk (INR (Value w)))]’]
+          \\ qspecl_then [‘replace_Force (Value w) n y2’, ‘Var v2’, ‘v1’, ‘[(n, Thunk (Value w))]’]
                          assume_tac subst_replace_Force
           \\ conj_asm2_tac
           \\ gvs [freevars_def, subst_def]
@@ -1728,10 +1714,6 @@ Proof
   >- (irule exp_rel_Delay >>
       last_x_assum irule >>
       gvs [exp_size_def, boundvars_def])
-  >~[‘Box _’]
-  >- (irule exp_rel_Box >>
-      last_x_assum irule >>
-      gvs [exp_size_def, boundvars_def])
   >~[‘replace_Force _ _ (Force y)’]
   >- (rename1 ‘exp_rel x y’ >>
       qpat_x_assum ‘exp_rel (Force _) (Force _)’ kall_tac >>
@@ -2153,8 +2135,8 @@ Proof
         \\ rename1 ‘exp_rel y y2’
         \\ Cases_on ‘eval_to (j + k - 1) x’ \\ gs []
         \\ rename1 ‘v_rel val1 val2’
-        \\ first_x_assum $ qspecl_then [‘subst1 w (Thunk (INR (Value val1))) (subst1 v val1 y)’,
-             ‘subst1 w (Thunk (INR (Value val2))) (subst1 v val2 (replace_Force (Var v) w y2))’] mp_tac
+        \\ first_x_assum $ qspecl_then [‘subst1 w (Thunk (Value val1)) (subst1 v val1 y)’,
+             ‘subst1 w (Thunk (Value val2)) (subst1 v val2 (replace_Force (Var v) w y2))’] mp_tac
         \\ impl_tac
         >- (qspecl_then [‘y2’, ‘Var v’, ‘w’, ‘[(v, val2)]’] assume_tac subst_replace_Force
             \\ drule_then assume_tac exp_rel_freevars
@@ -2162,22 +2144,22 @@ Proof
             \\ gvs [freevars_def, subst_def]
             \\ gvs [exp_rel_subst_replace_Force])
         \\ disch_then $ qx_choose_then ‘j1’ assume_tac
-        \\ Cases_on ‘eval_to (k − 2) (subst1 w (Thunk (INR (Value val2)))
+        \\ Cases_on ‘eval_to (k − 2) (subst1 w (Thunk (Value val2))
                                       (subst1 v val2 (replace_Force (Var v) w y2))) = INL Diverge’
         >- (qexists_tac ‘0’ \\ gs []
             \\ Cases_on ‘eval_to (k - 1) x = INL Diverge’ \\ gs []
             \\ dxrule_then (qspecl_then [‘j + k - 1’] assume_tac) eval_to_mono \\ gs []
-            \\ Cases_on ‘eval_to (k - 2) (subst1 w (Thunk (INR (Value val1)))
+            \\ Cases_on ‘eval_to (k - 2) (subst1 w (Thunk (Value val1))
                                           (subst1 v val1 y)) = INL Diverge’ \\ gs []
             \\ dxrule_then (qspecl_then [‘j1 + k - 2’] assume_tac) eval_to_mono \\ gs [])
         \\ qexists_tac ‘j + j1’
         \\ ‘eval_to (j + j1 + k - 1) x = eval_to (j + k - 1) x’
           by (irule eval_to_mono \\ gs [])
-        \\ ‘eval_to (j + j1 + k - 2) (subst1 w (Thunk (INR (Value val1))) (subst1 v val1 y))
-            = eval_to (j1 + k - 2) (subst1 w (Thunk (INR (Value val1))) (subst1 v val1 y))’
+        \\ ‘eval_to (j + j1 + k - 2) (subst1 w (Thunk (Value val1)) (subst1 v val1 y))
+            = eval_to (j1 + k - 2) (subst1 w (Thunk (Value val1)) (subst1 v val1 y))’
           by (irule eval_to_mono
               \\ gs [] \\ strip_tac
-              \\ Cases_on ‘eval_to (k − 2) (subst1 w (Thunk (INR (Value val2)))
+              \\ Cases_on ‘eval_to (k − 2) (subst1 w (Thunk (Value val2))
                                             (subst1 v val2 (replace_Force (Var v) w y2)))’ \\ gs [])
         \\ gvs [])
     \\ simp [eval_to_def]
@@ -2475,13 +2457,6 @@ Proof
   >~ [‘Delay x’] >- (
     rw [Once exp_rel_cases] \\ gs []
     \\ simp [eval_to_def, v_rel_def])
-  >~ [‘Box x’] >- (
-    rw [exp_rel_def] \\ gs []
-    \\ simp [eval_to_def]
-    \\ rename1 ‘exp_rel x y’
-    \\ first_x_assum $ drule_then $ qx_choose_then ‘j’ assume_tac
-    \\ qexists_tac ‘j’
-    \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to (k + j) x’ \\ gs [v_rel_def])
   >~ [‘MkTick x’] >- (
     rw [exp_rel_def] \\ gs [eval_to_def]
     \\ first_x_assum $ dxrule_then $ qx_choose_then ‘j’ assume_tac
@@ -3048,10 +3023,6 @@ Inductive full_exp_rel:
   (∀x y.
      full_exp_rel x y ⇒
        full_exp_rel (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀x y.
-     full_exp_rel x y ⇒
-       full_exp_rel (Box x) (Box y)) ∧
 [~Force:]
   (∀x y.
      full_exp_rel x y ⇒
@@ -3071,7 +3042,6 @@ Theorem full_exp_rel_def =
    “full_exp_rel (Let s x y) z”,
    “full_exp_rel (If x y z) w”,
    “full_exp_rel (Delay x) y”,
-   “full_exp_rel (Box x) y”,
    “full_exp_rel (MkTick x) y”,
    “full_exp_rel (Force x) y”]
   |> map (SIMP_CONV (srw_ss()) [Once full_exp_rel_cases])
@@ -3272,7 +3242,6 @@ Proof
   >~[‘no_value (Let (SOME _) x (Let (SOME _) _ y))’] >- gvs [no_value_def]
   >~[‘no_value (Let opt x y)’] >- gvs [no_value_def]
   >~[‘no_value (If x y z)’] >- gvs [no_value_def]
-  >~[‘no_value (Box x)’] >- gvs [no_value_def]
   >~[‘Var _’]
   >- (qexists_tac ‘0’ >> gvs [exp_rel_Var, NRC])
   >~[‘App _ _’]
@@ -3355,10 +3324,6 @@ Proof
   >- (irule_at Any NRC_rel_Delay >>
       gvs [exp_rel_Delay, exp_rel_refl] >>
       first_x_assum $ irule_at Any)
-  >~[‘Box _’]
-  >- (irule_at Any NRC_rel_Box >>
-      gvs [exp_rel_Box, exp_rel_refl] >>
-      first_x_assum $ irule_at Any)
   >~[‘Force _’]
   >- (irule_at Any NRC_rel_Force >>
       gvs [exp_rel_Force, exp_rel_refl] >>
diff --git a/compiler/backend/passes/proofs/thunk_Let_Lam_ForcedScript.sml b/compiler/backend/passes/proofs/thunk_Let_Lam_ForcedScript.sml
index 89f744b6..e5dfb624 100644
--- a/compiler/backend/passes/proofs/thunk_Let_Lam_ForcedScript.sml
+++ b/compiler/backend/passes/proofs/thunk_Let_Lam_ForcedScript.sml
@@ -126,10 +126,6 @@ Inductive force_arg_rel:
   (∀x y.
      force_arg_rel x y ⇒
        force_arg_rel (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀x y.
-     force_arg_rel x y ⇒
-       force_arg_rel (Box x) (Box y)) ∧
 [~Force:]
   (∀x y.
      force_arg_rel x y ⇒
@@ -364,14 +360,10 @@ Inductive force_arg_rel:
                           (LUPDATE (v1, Lams (vL1 ++ s::vL2)
                      (Apps (Var v2) (Var s::MAP Var vL1 ++ Tick (Force (Var s))::MAP Var vL2)))
                            i g)) n)) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w))) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      force_arg_rel x y ⇒
-     v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
+     v_rel (Thunk x) (Thunk y)) ∧
 [v_rel_Atom:]
   (∀x.
      v_rel (Atom x) (Atom x)) ∧
@@ -392,7 +384,6 @@ Theorem force_arg_rel_def =
    “force_arg_rel (Let s x y) z”,
    “force_arg_rel (If x y z) w”,
    “force_arg_rel (Delay x) y”,
-   “force_arg_rel (Box x) y”,
    “force_arg_rel (MkTick x) y”,
    “force_arg_rel (Force x) y”]
   |> map (SIMP_CONV (srw_ss()) [Once force_arg_rel_cases])
@@ -1001,9 +992,6 @@ Proof
   >~ [‘Delay x’] >- (
     rw [subst_def]
     \\ gs [force_arg_rel_Delay])
-  >~ [‘Box x’] >- (
-    rw [subst_def]
-    \\ gs [force_arg_rel_Box])
   >~ [‘Force x’] >- (
     rw [subst_def]
     \\ gs [force_arg_rel_Force])
@@ -1165,7 +1153,6 @@ Theorem eval_App_div:
                      | SOME (Let v31 v32 v33) => INL Type_error
                      | SOME (If v34 v35 v36) => INL Type_error
                      | SOME (Delay v37) => INL Type_error
-                     | SOME (Box v38) => INL Type_error
                      | SOME (Force v39) => INL Type_error
                      | SOME (Value v40) => INL Type_error
                      | SOME (MkTick v41) => INL Type_error
@@ -1203,7 +1190,6 @@ Theorem eval_App_Tick:
                      | SOME (Let v31 v32 v33) => INL Type_error
                      | SOME (If v34 v35 v36) => INL Type_error
                      | SOME (Delay v37) => INL Type_error
-                     | SOME (Box v38) => INL Type_error
                      | SOME (Force v39) => INL Type_error
                      | SOME (Value v40) => INL Type_error
                      | SOME (MkTick v41) => INL Type_error
@@ -1246,7 +1232,6 @@ Theorem eval_App_Tick2:
                        | SOME (Let v31 v32 v33) => INL Type_error
                        | SOME (If v34 v35 v36) => INL Type_error
                        | SOME (Delay v37) => INL Type_error
-                       | SOME (Box v38) => INL Type_error
                        | SOME (Force v39) => INL Type_error
                        | SOME (Value v40) => INL Type_error
                        | SOME (MkTick v41) => INL Type_error
@@ -1292,7 +1277,6 @@ Theorem eval_App_Tick_Force_Val_Div:
                      | SOME (Let v31 v32 v33) => INL Type_error
                      | SOME (If v34 v35 v36) => INL Type_error
                      | SOME (Delay v37) => INL Type_error
-                     | SOME (Box v38) => INL Type_error
                      | SOME (Force v39) => INL Type_error
                      | SOME (Value v40) => INL Type_error
                      | SOME (MkTick v41) => INL Type_error
@@ -4459,15 +4443,8 @@ Proof
     \\ ‘EL n (MAP FST f) = EL n (MAP FST g)’ by gs [] \\ gvs [EL_MAP]
     \\ irule v_rel_Recclosure
     \\ gvs [LIST_REL_EL_EQN, EL_MAP])
- >~ [‘Delay x’] >- print_tac "Delay" (
+  >~ [‘Delay x’] >- print_tac "Delay" (
     gvs [Once force_arg_rel_def, eval_to_def, v_rel_def])
-  >~ [‘Box x’] >- (
-    gvs [Once force_arg_rel_def, eval_to_def]
-    \\ rename1 ‘force_arg_rel x y’
-    \\ first_x_assum $ dxrule_then $ qx_choose_then ‘j’ assume_tac
-    \\ qexists_tac ‘j’
-    \\ Cases_on ‘eval_to k x’ \\ Cases_on ‘eval_to (j + k) y’ \\ gs []
-    \\ simp [v_rel_def])
   >~ [‘Force x’] >- print_tac "Force" (
     rgs [Once force_arg_rel_def]
     \\ once_rewrite_tac [eval_to_def] \\ simp []
@@ -4710,8 +4687,9 @@ Proof
             by (strip_tac \\ Cases_on ‘eval_to (k - 1) (subst_funs binds e)’ \\ gvs [])
           \\ dxrule_then (qspec_then ‘j + j1 + k - 1’ assume_tac) eval_to_mono
           \\ gvs [])
+      \\ rename1 ‘dest_anyThunk v1 = INR (wx, binds)’
       \\ ‘∃wx' binds'. dest_anyThunk w1 = INR (wx', binds') ∧
-                       (v_rel +++ force_arg_rel) wx wx' ∧
+                       force_arg_rel wx wx' ∧
                        MAP FST binds = MAP FST binds' ∧
                        EVERY ok_bind (MAP SND binds) ∧
                        EVERY ok_bind (MAP SND binds') ∧
@@ -4719,12 +4697,6 @@ Proof
         by (Cases_on ‘v1’ \\ Cases_on ‘w1’
             \\ gvs [v_rel_def]
             \\ gvs [dest_anyThunk_def, v_rel_def])
-      \\ CASE_TAC \\ gs []
-      >- (
-        qexists_tac ‘j’ \\ simp []
-        \\ CASE_TAC \\ gs []
-        \\ Cases_on ‘v1’ \\ Cases_on ‘w1’ \\ gs [dest_anyThunk_def])
-      \\ Cases_on ‘wx'’ \\ gs []
       \\ rename1 ‘force_arg_rel x1 x2’
       \\ ‘force_arg_rel (subst_funs binds x1) (subst_funs binds' x2)’
         by (simp [subst_funs_def]
diff --git a/compiler/backend/passes/proofs/thunk_NRC_Forcing_LambdasScript.sml b/compiler/backend/passes/proofs/thunk_NRC_Forcing_LambdasScript.sml
index 63fc0866..70fe99f0 100644
--- a/compiler/backend/passes/proofs/thunk_NRC_Forcing_LambdasScript.sml
+++ b/compiler/backend/passes/proofs/thunk_NRC_Forcing_LambdasScript.sml
@@ -92,10 +92,6 @@ Inductive exp_rel:
   (∀set x y.
      exp_rel set x y ⇒
        exp_rel set (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀set x y.
-     exp_rel set x y ⇒
-       exp_rel set (Box x) (Box y)) ∧
 [~Force:]
   (∀set x y.
      exp_rel set x y ⇒
@@ -114,7 +110,6 @@ Theorem exp_rel_def =
    “exp_rel s (Let opt x y) z”,
    “exp_rel s (If x y z) w”,
    “exp_rel s (Delay x) y”,
-   “exp_rel s (Box x) y”,
    “exp_rel s (MkTick x) y”,
    “exp_rel s (Value x) y”,
    “exp_rel s (Force x) y”]
@@ -884,9 +879,6 @@ Proof
   >- (irule_at Any NRC_rel_Delay >>
       gs [forcing_lam_rel_def] >>
       first_x_assum $ irule_at Any)
-  >- (irule_at Any NRC_rel_Box >>
-      gs [forcing_lam_rel_def] >>
-      first_x_assum $ irule_at Any)
   >- (irule_at Any NRC_rel_Force >>
       gs [forcing_lam_rel_def] >>
       first_x_assum $ irule_at Any)
diff --git a/compiler/backend/passes/proofs/thunk_NRC_relScript.sml b/compiler/backend/passes/proofs/thunk_NRC_relScript.sml
index ed2ebe6c..58d455a2 100644
--- a/compiler/backend/passes/proofs/thunk_NRC_relScript.sml
+++ b/compiler/backend/passes/proofs/thunk_NRC_relScript.sml
@@ -234,15 +234,6 @@ Proof
   rpt $ last_x_assum $ drule_then $ irule_at Any
 QED
 
-Theorem NRC_rel_Box:
-  (∀x y. R x y ⇒ R (Box x) (Box y)) ⇒
-      ∀n x y. NRC R n x y ⇒ NRC R n (Box x) (Box y)
-Proof
-  strip_tac >> Induct >> gvs [NRC] >>
-  rw [] >>
-  rpt $ last_x_assum $ drule_then $ irule_at Any
-QED
-
 Theorem NRC_rel_Lam:
   (∀s x y. R x y ⇒ R (Lam s x) (Lam s y)) ⇒
       ∀n s x y. NRC R n x y ⇒ NRC R n (Lam s x) (Lam s y)
diff --git a/compiler/backend/passes/proofs/thunk_case_d2bProofScript.sml b/compiler/backend/passes/proofs/thunk_case_d2bProofScript.sml
index 862f9fe4..e1adfe36 100644
--- a/compiler/backend/passes/proofs/thunk_case_d2bProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_case_d2bProofScript.sml
@@ -17,14 +17,13 @@ open pure_miscTheory thunkLangPropsTheory;
 val _ = new_theory "thunk_case_d2bProof";
 
 val _ = set_grammar_ancestry ["finite_map", "pred_set", "rich_list",
-                              "thunkLang", "wellorder", "quotient_sum",
-                              "quotient_pair", "thunkLangProps"];
+                              "thunkLang", "wellorder", "thunkLangProps"];
 
 val _ = numLib.prefer_num ();
 
-Theorem SUM_REL_def[local,simp] = quotient_sumTheory.SUM_REL_def;
+Theorem SUM_REL_THM[local,simp] = sumTheory.SUM_REL_THM;
 
-Theorem PAIR_REL_def[local,simp] = quotient_pairTheory.PAIR_REL;
+Theorem PAIR_REL_def[local,simp] = pairTheory.PAIR_REL;
 
 Inductive exp_rel:
 (* Delay-to-Box *)
@@ -36,12 +35,7 @@ Inductive exp_rel:
        exp_rel (Let (SOME v) (Delay x1)
                         (Let (SOME w) (Force (Var v)) y1))
                    (Let (SOME w) x2
-                        (Let (SOME v) (Box (Var w)) y2))) ∧
-[v_rel_D2B:]
-  (∀x v w k.
-     eval_to k x = INR v ∧
-     v_rel v w ⇒
-       v_rel (Thunk (INR x)) (Thunk (INL w))) ∧
+                        (Let (SOME v) (Delay (Var w)) y2))) ∧
 (* Boilerplate: *)
 [exp_rel_App:]
   (∀f g x y.
@@ -78,10 +72,6 @@ Inductive exp_rel:
   (∀x y.
      exp_rel x y ⇒
        exp_rel (Delay x) (Delay y)) ∧
-[exp_rel_Box:]
-  (∀x y.
-     exp_rel x y ⇒
-       exp_rel (Box x) (Box y)) ∧
 [exp_rel_Force:]
   (∀x y.
      exp_rel x y ⇒
@@ -120,14 +110,10 @@ Inductive exp_rel:
   (∀f g n.
      LIST_REL (λ(fn,x) (gn,y). fn = gn ∧ exp_rel x y) f g ⇒
        v_rel (Recclosure f n) (Recclosure g n)) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      exp_rel x y ⇒
-       v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w)))
+       v_rel (Thunk x) (Thunk y))
 End
 
 Theorem v_rel_cases[local] = CONJUNCT2 exp_rel_cases;
@@ -144,8 +130,7 @@ Theorem v_rel_def[simp] =
     “v_rel z (Monadic mop ys)”,
     “v_rel (Atom x) z”,
     “v_rel z (Atom x)”,
-    “v_rel (Thunk (INL x)) z”,
-    “v_rel z (Thunk (INR x))” ]
+    “v_rel (Thunk x) z” ]
   |> map (SIMP_CONV (srw_ss()) [Once v_rel_cases])
   |> LIST_CONJ;
 
@@ -309,11 +294,6 @@ Proof
           \\ rpt (pop_assum kall_tac)
           \\ qid_spec_tac ‘ws’ \\ Induct_on ‘vs’ \\ Cases_on ‘ws’ \\ simp [])
     \\ gvs [Abbr ‘R’, OPTREL_def, exp_rel_Var, exp_rel_Value])
-  >- ((* Box *)
-    rw [Once exp_rel_cases] \\ gs []
-    \\ simp [subst_def]
-    \\ irule exp_rel_Box
-    \\ first_x_assum irule \\ gs [])
   >- ((* Force *)
     rw [Once exp_rel_cases]
     \\ simp [subst_def]
@@ -735,65 +715,55 @@ Proof
         \\ qpat_assum ‘_ = INL Type_error’ (SUBST1_TAC o SYM)
         \\ irule eval_to_mono \\ gs []))
     \\ simp [subst_funs_def]
-    \\ reverse CASE_TAC \\ gs []
+    \\ Cases_on ‘v’ \\ gs [v_rel_def]
+    \\ rename1 ‘exp_rel x1 y1’
+    \\ Cases_on ‘eval_to (k - 1) y1 = INL Diverge’
     >- (
-      rename1 ‘exp_rel x1 y1’
-      \\ Cases_on ‘eval_to (k - 1) y1 = INL Diverge’
-      >- (
-        Cases_on ‘eval_to k x = INL Diverge’
-        >- (
-          qexists_tac ‘0’
-          \\ simp [])
-        \\ ‘∀j. eval_to (j + k) x = eval_to k x’
-          by (gen_tac \\ irule eval_to_mono \\ gs [])
-        \\ gvs []
-        \\ ‘∀j. j + k - 1 = j + (k - 1)’ by gs []
-        \\ asm_simp_tac std_ss []
-        \\ qpat_assum `_ = INL Diverge` (SUBST1_TAC o SYM)
-        \\ first_x_assum irule
-        \\ gs [eval_to_wo_def]
-        \\ qx_gen_tac ‘j’
-        \\ strip_tac
-        \\ qpat_x_assum ‘∀k. eval_to _ (Force _) ≠ _’ mp_tac
-        \\ simp [Once eval_to_def]
-        \\ qexists_tac ‘j + k’
-        \\ asm_simp_tac std_ss []
-        \\ simp [dest_anyThunk_def, subst_funs_def]
-        \\ qpat_assum ‘_ = INL Type_error’ (SUBST1_TAC o SYM)
-        \\ irule eval_to_mono \\ gs [])
-      \\ ‘∀j1. eval_to (j1 + j + k) x = eval_to (j + k) x’
-        by (gen_tac \\ irule eval_to_mono \\ gs [])
-      \\ Q.REFINE_EXISTS_TAC ‘j1 + j’ \\ gs []
-      \\ ‘∃j. ($= +++ v_rel) (eval_to (j + (k - 1)) x1)
-                                 (eval_to (k - 1) y1)’
-        suffices_by (
-          disch_then (qx_choose_then ‘j1’ assume_tac)
-          \\ ‘eval_to (j1 + j + k - 1) x1 =
-              eval_to (j1 + k - 1) x1’
-            by (irule eval_to_mono \\ gs []
-                \\ strip_tac \\ gs []
-                \\ Cases_on ‘eval_to (k - 1) y1’ \\ gs [])
-          \\ qexists_tac ‘j1’ \\ gs [])
-      \\ first_x_assum irule
-      \\ gs [eval_to_wo_def]
-      \\ qx_gen_tac ‘j1’
-      \\ strip_tac
-      \\ qpat_x_assum ‘∀k. eval_to _ (Force _) ≠ _’ mp_tac
-      \\ simp [Once eval_to_def]
-      \\ qexists_tac ‘j + (j1 + k)’
-      \\ asm_simp_tac std_ss []
-      \\ simp [dest_anyThunk_def, subst_funs_def]
-      \\ qpat_assum ‘_ = INL Type_error’ (SUBST1_TAC o SYM)
-      \\ irule eval_to_mono \\ gs [])
+    Cases_on ‘eval_to k x = INL Diverge’
+    >- (
+      qexists_tac ‘0’
+      \\ simp [])
+    \\ ‘∀j. eval_to (j + k) x = eval_to k x’
+      by (gen_tac \\ irule eval_to_mono \\ gs [])
+    \\ gvs []
+    \\ ‘∀j. j + k - 1 = j + (k - 1)’ by gs []
+    \\ asm_simp_tac std_ss []
+    \\ qpat_assum `_ = INL Diverge` (SUBST1_TAC o SYM)
+    \\ first_x_assum irule
+    \\ gs [eval_to_wo_def]
+    \\ qx_gen_tac ‘j’
+    \\ strip_tac
+    \\ qpat_x_assum ‘∀k. eval_to _ (Force _) ≠ _’ mp_tac
+    \\ simp [Once eval_to_def]
+    \\ qexists_tac ‘j + k’
+    \\ asm_simp_tac std_ss []
+    \\ simp [dest_anyThunk_def, subst_funs_def]
+    \\ qpat_assum ‘_ = INL Type_error’ (SUBST1_TAC o SYM)
+    \\ irule eval_to_mono \\ gs [])
     \\ ‘∀j1. eval_to (j1 + j + k) x = eval_to (j + k) x’
       by (gen_tac \\ irule eval_to_mono \\ gs [])
-    \\ Q.REFINE_EXISTS_TAC ‘j + j1’ \\ gs []
-    \\ rgs [Once (CONJUNCT2 exp_rel_cases)] \\ rw []
-    \\ rename1 ‘eval_to k1 x1 = INR v1’
-    \\ qexists_tac ‘j1 + k1’
-    \\ ‘eval_to (k + k1 + j + j1 - 1) x1 = eval_to k1 x1’
-      by (irule eval_to_mono \\ gs [])
-    \\ gs [])
+    \\ Q.REFINE_EXISTS_TAC ‘j1 + j’ \\ gs []
+    \\ ‘∃j. ($= +++ v_rel) (eval_to (j + (k - 1)) x1)
+                           (eval_to (k - 1) y1)’
+      suffices_by (
+      disch_then (qx_choose_then ‘j1’ assume_tac)
+      \\ ‘eval_to (j1 + j + k - 1) x1 =
+          eval_to (j1 + k - 1) x1’
+        by (irule eval_to_mono \\ gs []
+            \\ strip_tac \\ gs []
+            \\ Cases_on ‘eval_to (k - 1) y1’ \\ gs [])
+      \\ qexists_tac ‘j1’ \\ gs [])
+    \\ first_x_assum irule
+    \\ gs [eval_to_wo_def]
+    \\ qx_gen_tac ‘j1’
+    \\ strip_tac
+    \\ qpat_x_assum ‘∀k. eval_to _ (Force _) ≠ _’ mp_tac
+    \\ simp [Once eval_to_def]
+    \\ qexists_tac ‘j + (j1 + k)’
+    \\ asm_simp_tac std_ss []
+    \\ simp [dest_anyThunk_def, subst_funs_def]
+    \\ qpat_assum ‘_ = INL Type_error’ (SUBST1_TAC o SYM)
+    \\ irule eval_to_mono \\ gs [])
   >~ [‘If x1 y1 z1’] >- (
     ntac 2 strip_tac
     \\ rw [Once exp_rel_cases]
@@ -910,20 +880,6 @@ Proof
     ntac 2 strip_tac
     \\ rw [Once exp_rel_cases]
     \\ simp [eval_to_def])
-  >~ [‘Box x’] >- (
-    ntac 2 strip_tac
-    \\ rw [Once exp_rel_cases]
-    \\ rename1 ‘exp_rel x y’
-    \\ simp [eval_to_def]
-    \\ ‘∃j. ($= +++ v_rel) (eval_to (j + k) x) (eval_to k y)’
-      suffices_by (
-        disch_then (qx_choose_then ‘j’ assume_tac)
-        \\ qexists_tac ‘j’
-        \\ Cases_on ‘eval_to (j + k) x’ \\ Cases_on ‘eval_to k y’ \\ gs [])
-    \\ first_x_assum irule \\ simp [eval_to_wo_def, exp_size_def]
-    \\ rpt strip_tac
-    \\ first_x_assum (qspec_then ‘k’ mp_tac)
-    \\ simp [eval_to_def])
   >~ [‘MkTick x’] >- (
     ntac 2 strip_tac
     \\ rw [Once exp_rel_cases]
@@ -948,8 +904,8 @@ Proof
     >~ [‘Let (SOME s) x1 y1’] >- (
       strip_tac
       \\ rw [Once exp_rel_cases]
-      >- ((* D2B *)
-        pop_assum mp_tac
+      >- ((* D2B *) cheat
+(*        pop_assum mp_tac
         \\ simp [Once eval_to_def]
         \\ simp [Once eval_to_def, subst_def]
         \\ simp [Once eval_to_def]
@@ -982,7 +938,7 @@ Proof
           \\ simp [])
         \\ Cases_on ‘eval_to (j1 + k - 1) x1’ \\ gs []
         \\ rename1 ‘v_rel v u’
-        \\ ‘∀k. eval_to k (subst1 w v (subst1 s (Thunk (INR x1)) y1)) ≠
+        \\ ‘∀k. eval_to k (subst1 w v (subst1 s (Thunk x1) y1)) ≠
                 INL Type_error’
           by (qx_gen_tac ‘j’
               \\ strip_tac
@@ -1030,7 +986,7 @@ Proof
           \\ irule v_rel_D2B
           \\ gs [SF SFY_ss])
         \\ Q.REFINE_EXISTS_TAC ‘2 + j’ \\ simp []
-        \\ qabbrev_tac ‘X1 = subst1 s (Thunk (INR x1)) (subst1 w v y1) ’
+        \\ qabbrev_tac ‘X1 = subst1 s (Thunk x1) (subst1 w v y1) ’
         \\ qmatch_goalsub_abbrev_tac ‘_ _ (eval_to _ X2)’
         \\ ‘∃j2. ($= +++ v_rel) (eval_to (j2 + (k - 2)) X1)
                                     (eval_to (k - 2) X2)’
@@ -1051,7 +1007,7 @@ Proof
         \\ Cases_on ‘eval_to (k - 2) X2’ \\ gs []
         \\ ‘eval_to (j1 + j2 + k) X1 = eval_to (j2 + k - 2) X1’
           suffices_by rw []
-        \\ irule eval_to_mono \\ gs [])
+        \\ irule eval_to_mono \\ gs []*))
       \\ ‘∀k. eval_to k x1 ≠ INL Type_error’
         by (qx_gen_tac ‘j’
             \\ strip_tac
@@ -1605,9 +1561,6 @@ Proof
   rw [rel_ok_def]
   >- ((* ∀x. f x ≠ Err from rel_ok prevents this case *)
     simp [d2b_apply_closure])
-  >- ((* Thunks go to Thunks or DoTicks *)
-    Cases_on ‘s’ \\ gs []
-    \\ gs [Once v_rel_cases])
   >- ((* Equal literals are related *)
     simp [exp_rel_Prim])
   >- ((* Equal 0-arity conses are related *)
@@ -1637,4 +1590,3 @@ Proof
 QED
 
 val _ = export_theory ();
-
diff --git a/compiler/backend/passes/proofs/thunk_case_inlProofScript.sml b/compiler/backend/passes/proofs/thunk_case_inlProofScript.sml
index 2519d28d..020715e8 100644
--- a/compiler/backend/passes/proofs/thunk_case_inlProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_case_inlProofScript.sml
@@ -18,17 +18,16 @@ val _ = new_theory "thunk_case_inlProof";
 
 val _ = set_grammar_ancestry [
   "finite_map", "pred_set", "rich_list", "thunkLang", "wellorder",
-   "quotient_sum", "quotient_pair", "thunk_semantics", "thunkLangProps" ];
+  "thunk_semantics", "thunkLangProps" ];
 
 val _ = numLib.prefer_num ();
 
-Theorem SUM_REL_def[local,simp] = quotient_sumTheory.SUM_REL_def;
+Theorem SUM_REL_THM[local,simp] = sumTheory.SUM_REL_THM;
 
-Theorem PAIR_REL_def[local,simp] = quotient_pairTheory.PAIR_REL;
+Theorem PAIR_REL_def[local,simp] = pairTheory.PAIR_REL;
 
 Definition ok_binder_def[simp]:
   ok_binder (Lam s x) = T ∧
-  ok_binder (Box x) = T ∧
   ok_binder (Delay x) = T ∧
   ok_binder _ = F
 End
@@ -38,11 +37,11 @@ Inductive exp_rel:
 [exp_rel_Inline:]
   (∀m v.
      v ∈ m ⇒
-       exp_rel m (Var v) (Box (Var v))) ∧
+       exp_rel m (Var v) (Delay (Var v))) ∧
 [exp_rel_Inline_Value:]
   (∀m v w.
      v_rel v w ⇒
-       exp_rel m (Value (Thunk (INL v))) (Box (Value w))) ∧
+       exp_rel m (Value (Thunk (Value v))) (Delay (Value w))) ∧
 [exp_rel_NoInline:]
   (∀m v.
      v ∉ m ⇒
@@ -51,13 +50,13 @@ Inductive exp_rel:
   (∀m v w y1 y2.
      exp_rel (v INSERT m) y1 y2 ∧
      w ∉ m ⇒
-       exp_rel m (Let (SOME v) (Box (Var w)) y1)
+       exp_rel m (Let (SOME v) (Delay (Var w)) y1)
                      (Let (SOME v) (Var w) y2)) ∧
 [exp_rel_Bind_Value:]
   (∀m v x1 x2 y1 y2.
      exp_rel (v INSERT m) y1 y2 ∧
      v_rel x1 x2 ⇒
-       exp_rel m (Let (SOME v) (Box (Value x1)) y1)
+       exp_rel m (Let (SOME v) (Delay (Value x1)) y1)
                      (Let (SOME v) (Value x2) y2)) ∧
 (* Boilerplate: *)
 [exp_rel_App:]
@@ -101,10 +100,6 @@ Inductive exp_rel:
   (∀m x y.
      exp_rel m x y ⇒
        exp_rel m (Delay x) (Delay y)) ∧
-[exp_rel_Box:]
-  (∀m x y.
-     exp_rel m x y ⇒
-       exp_rel m (Box x) (Box y)) ∧
 [exp_rel_Force:]
   (∀m x y.
      exp_rel m x y ⇒
@@ -145,15 +140,11 @@ Inductive exp_rel:
                  ok_binder x ∧
                  exp_rel EMPTY x y) f g ⇒
        v_rel (Recclosure f n) (Recclosure g n)) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      exp_rel EMPTY x y ∧
      closed x ⇒
-       v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w)))
+       v_rel (Thunk x) (Thunk y))
 End
 
 Theorem v_rel_cases[local] = CONJUNCT2 exp_rel_cases;
@@ -169,10 +160,8 @@ Theorem v_rel_def[simp] =
     “v_rel z (Monadic mop ys)”,
     “v_rel (Atom s) z”,
     “v_rel z (Atom s)”,
-    “v_rel (Thunk (INL s)) z”,
-    “v_rel z (Thunk (INL s))”,
-    “v_rel (Thunk (INR s)) z”,
-    “v_rel z (Thunk (INR s))” ]
+    “v_rel (Thunk s) z”,
+    “v_rel z (Thunk s)” ]
   |> map (SIMP_CONV (srw_ss ()) [Once v_rel_cases])
   |> LIST_CONJ;
 
@@ -282,9 +271,6 @@ Proof
   >- ((* Delay *)
     gs [freevars_def]
     \\ irule exp_rel_Delay \\ gs [])
-  >- ((* Box *)
-    gs [freevars_def]
-    \\ irule exp_rel_Box \\ gs [])
   >- ((* Force *)
     gs [freevars_def]
     \\ irule exp_rel_Force \\ gs [])
@@ -306,7 +292,7 @@ Theorem exp_rel_subst:
   ∀vs x ws y m.
     MAP FST vs = MAP FST ws ∧
     LIST_REL (λ(f,v) (g,w).
-      (f ∈ m ⇒ v_rel v (Thunk (INL w))) ∧
+      (f ∈ m ⇒ v_rel v (Thunk (Value w))) ∧
       (f ∉ m ⇒ v_rel v w)) vs ws ∧
     exp_rel m x y ⇒
       exp_rel m (subst vs x) (subst ws y)
@@ -327,6 +313,7 @@ Proof
       \\ ‘k < LENGTH ws’ by gs [Abbr ‘k’]
       \\ first_x_assum (drule_then assume_tac)
       \\ rpt (pairarg_tac \\ gvs [])
+      \\ gs [Once exp_rel_cases]
       \\ irule exp_rel_Inline_Value
       \\ gs [])
         (* s ∉ m *)
@@ -463,11 +450,6 @@ Proof
     \\ irule exp_rel_Delay
     \\ first_x_assum irule \\ gs []
     \\ first_assum (irule_at Any) \\ gs [])
-  >- ((* Box *)
-    rw [Once exp_rel_cases] \\ gs []
-    \\ simp [subst_def]
-    \\ irule exp_rel_Box
-    \\ first_x_assum irule \\ gs [])
   >- ((* Force *)
     rw [Once exp_rel_cases]
     \\ simp [subst_def]
@@ -497,7 +479,8 @@ Proof
   \\ rpt conj_tac \\ rpt gen_tac
   >~ [‘Value v’] >- (
     rw [Once exp_rel_cases]
-    \\ simp [eval_to_def])
+    \\ simp [eval_to_def]
+    \\ irule exp_rel_Value \\ simp [])
   >~ [‘App f x’] >- (
     strip_tac
     \\ rw [Once exp_rel_cases] \\ gs []
@@ -566,7 +549,8 @@ Proof
       \\ first_x_assum irule
       \\ simp [closed_subst]
       \\ irule_at Any exp_rel_subst \\ gs []
-      \\ first_assum (irule_at Any) \\ gs [])
+      \\ first_assum (irule_at Any) \\ gs []
+      \\ irule exp_rel_Value \\ gs [])
     \\ simp [eval_to_def]
     \\ IF_CASES_TAC \\ gs []
     \\ first_x_assum (drule_then assume_tac)
@@ -667,7 +651,6 @@ Proof
         \\ drule_then strip_assume_tac ALOOKUP_SOME_REVERSE_EL \\ gs []
         \\ first_x_assum (drule_then assume_tac)
         \\ gs [ELIM_UNCURRY, freevars_def])
-      \\ CASE_TAC \\ gs []
       \\ first_x_assum irule
       \\ simp [subst_funs_def, SF SFY_ss])
     \\ ‘∃y. dest_Tick w = SOME y’
@@ -684,13 +667,6 @@ Proof
     \\ irule exp_rel_freevars
     \\ first_assum (irule_at Any)
     \\ gs [closed_def])
-  >~ [‘Box x’] >- (
-    strip_tac
-    \\ rw [Once exp_rel_cases] \\ gs []
-    \\ simp [eval_to_def]
-    \\ rename1 ‘exp_rel m x y’
-    \\ first_x_assum (drule_then assume_tac)
-    \\ Cases_on ‘eval_to k x’ \\ Cases_on ‘eval_to k y’ \\ gs [])
   >~ [‘MkTick x’] >- (
     strip_tac
     \\ rw [Once exp_rel_cases] \\ gs []
@@ -876,8 +852,6 @@ Proof
   rw [rel_ok_def]
   >- ((* ∀x. f x ≠ Err from rel_ok prevents this case *)
     simp [inl_apply_closure])
-  >- ((* Thunks go to Thunks or DoTicks *)
-    Cases_on ‘s’ \\ gs [])
   >- (
     gs [Once v_rel_cases])
   >- ((* Equal literals are related *)
@@ -909,4 +883,3 @@ Proof
 QED
 
 val _ = export_theory ();
-
diff --git a/compiler/backend/passes/proofs/thunk_case_liftProofScript.sml b/compiler/backend/passes/proofs/thunk_case_liftProofScript.sml
index 3a32b29e..d656e92d 100644
--- a/compiler/backend/passes/proofs/thunk_case_liftProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_case_liftProofScript.sml
@@ -19,14 +19,14 @@ val _ = new_theory "thunk_case_liftProof";
 
 val _ = set_grammar_ancestry [
   "finite_map", "pred_set", "rich_list", "thunkLang", "wellorder",
-  "quotient_sum", "quotient_pair", "thunk_semantics", "thunkLangProps",
+  "thunk_semantics", "thunkLangProps",
   "thunk_tickProof" ];
 
 val _ = numLib.prefer_num ();
 
-Theorem SUM_REL_def[local,simp] = quotient_sumTheory.SUM_REL_def;
+Theorem SUM_REL_THM[local,simp] = sumTheory.SUM_REL_THM;
 
-Theorem PAIR_REL_def[local,simp] = quotient_pairTheory.PAIR_REL;
+Theorem PAIR_REL_def[local,simp] = pairTheory.PAIR_REL;
 
 Inductive exp_rel:
 (* Lifting case: *)
@@ -75,10 +75,6 @@ Inductive exp_rel:
   (∀x y.
      exp_rel x y ⇒
        exp_rel (Delay x) (Delay y)) ∧
-[exp_rel_Box:]
-  (∀x y.
-     exp_rel x y ⇒
-       exp_rel (Box x) (Box y)) ∧
 [exp_rel_Force:]
   (∀x y.
      exp_rel x y ⇒
@@ -117,14 +113,10 @@ Inductive exp_rel:
   (∀f g n.
      LIST_REL (λ(fn,x) (gn,y). fn = gn ∧ exp_rel x y) f g ⇒
        v_rel (Recclosure f n) (Recclosure g n)) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      exp_rel x y ⇒
-       v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w)))
+       v_rel (Thunk x) (Thunk y))
 End
 
 Theorem v_rel_cases[local] = CONJUNCT2 exp_rel_cases;
@@ -141,10 +133,8 @@ Theorem v_rel_def[simp] =
     “v_rel z (Monadic mop ys)”,
     “v_rel (Atom x) z”,
     “v_rel z (Atom x)”,
-    “v_rel (Thunk (INL x)) z”,
-    “v_rel z (Thunk (INL x))”,
-    “v_rel (Thunk (INR x)) z”,
-    “v_rel z (Thunk (INR x))” ]
+    “v_rel (Thunk x) z”,
+    “v_rel z (Thunk x)” ]
   |> map (SIMP_CONV (srw_ss()) [Once v_rel_cases])
   |> LIST_CONJ;
 
@@ -291,11 +281,6 @@ Proof
           \\ rpt (pop_assum kall_tac)
           \\ qid_spec_tac ‘ws’ \\ Induct_on ‘vs’ \\ Cases_on ‘ws’ \\ simp [])
     \\ gvs [Abbr ‘R’, OPTREL_def, exp_rel_Var, exp_rel_Value])
-  >- ((* Box *)
-    rw [Once exp_rel_cases] \\ gs []
-    \\ simp [subst_def]
-    \\ irule exp_rel_Box
-    \\ first_x_assum irule \\ gs [])
   >- ((* Force *)
     rw [Once exp_rel_cases]
     \\ simp [subst_def]
@@ -421,13 +406,6 @@ Proof
   >~ [‘Delay x’] >- (
     rw [Once exp_rel_cases] \\ gs []
     \\ simp [eval_to_def])
-  >~ [‘Box x’] >- (
-    strip_tac
-    \\ rw [Once exp_rel_cases] \\ gs []
-    \\ simp [eval_to_def]
-    \\ rename1 ‘exp_rel x y’
-    \\ first_x_assum (drule_then assume_tac)
-    \\ Cases_on ‘eval_to k x’ \\ Cases_on ‘eval_to k y’ \\ gs [])
   >~ [‘Force x’] >- (
     strip_tac
     \\ rw [Once exp_rel_cases] \\ gs []
@@ -458,7 +436,6 @@ Proof
                                       EVERY2_MAP, LAMBDA_PROD, GSYM FST_THM]
         \\ gs [ELIM_UNCURRY, LIST_REL_EL_EQN]
         \\ irule LIST_EQ \\ gvs [EL_MAP])
-      \\ CASE_TAC \\ gs []
       \\ first_x_assum irule
       \\ simp [subst_funs_def])
     \\ ‘∃y. dest_Tick w = SOME y’
@@ -625,8 +602,6 @@ Proof
   rw [rel_ok_def]
   >- ((* ∀x. f x ≠ Err from rel_ok prevents this case *)
     simp [lift_apply_closure])
-  >- ((* Thunks go to Thunks or DoTicks *)
-    Cases_on ‘s’ \\ gs [])
   >- (
     gs [Once v_rel_cases])
   >- ((* Equal literals are related *)
@@ -705,10 +680,6 @@ Inductive compile_rel:
   (∀x y.
      compile_rel x y ⇒
        compile_rel (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀x y.
-     compile_rel x y ⇒
-       compile_rel (Box x) (Box y)) ∧
 [~Force:]
   (∀x y.
      compile_rel x y ⇒
@@ -756,7 +727,6 @@ Proof
   \\ rpt $ irule_at Any thunk_tickProofTheory.exp_rel_Prim
   \\ rpt $ irule_at Any thunk_tickProofTheory.exp_rel_Monad
   \\ rpt $ irule_at Any thunk_tickProofTheory.exp_rel_Delay
-  \\ rpt $ irule_at Any thunk_tickProofTheory.exp_rel_Box
   \\ rpt $ irule_at Any thunk_tickProofTheory.exp_rel_Force
   \\ rpt $ irule_at Any thunk_tickProofTheory.exp_rel_Var
   \\ rpt $ first_x_assum $ irule_at $ Pos hd
@@ -766,7 +736,6 @@ Proof
   >~ [‘Let’] >- (irule_at Any exp_rel_Let \\ fs [])
   >~ [‘If’] >- (irule_at Any exp_rel_If \\ fs [])
   >~ [‘Delay’] >- (irule_at Any exp_rel_Delay \\ fs [])
-  >~ [‘Box’] >- (irule_at Any exp_rel_Box \\ fs [])
   >~ [‘Var’] >- (irule_at Any exp_rel_Var \\ fs [])
   >~ [`Monad`]
   >- (
diff --git a/compiler/backend/passes/proofs/thunk_case_projProofScript.sml b/compiler/backend/passes/proofs/thunk_case_projProofScript.sml
index d909e40e..7780bf23 100644
--- a/compiler/backend/passes/proofs/thunk_case_projProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_case_projProofScript.sml
@@ -19,13 +19,13 @@ val _ = new_theory "thunk_case_projProof";
 
 val _ = set_grammar_ancestry [
   "finite_map", "pred_set", "rich_list", "thunkLang", "wellorder",
-   "quotient_sum", "quotient_pair", "thunkLangProps", "thunk_semantics" ];
+  "thunkLangProps", "thunk_semantics" ];
 
 val _ = numLib.prefer_num ();
 
-Theorem SUM_REL_def[local,simp] = quotient_sumTheory.SUM_REL_def;
+Theorem SUM_REL_THM[local,simp] = sumTheory.SUM_REL_THM;
 
-Theorem PAIR_REL_def[local,simp] = quotient_pairTheory.PAIR_REL;
+Theorem PAIR_REL_def[local,simp] = pairTheory.PAIR_REL;
 
 Definition ok_binder_def[simp]:
   ok_binder (Lam s x) = T ∧
@@ -56,7 +56,7 @@ Inductive exp_rel:
   (∀xs s i.
      i < LENGTH xs ∧
      v_rel (EL i xs) v ⇒
-       v_rel (Thunk (INR (Force (Proj s i (Value (Constructor s xs))))))
+       v_rel (Thunk (Force (Proj s i (Value (Constructor s xs)))))
              (DoTick v)) ∧
 (* Boilerplate: *)
 [exp_rel_App:]
@@ -107,10 +107,6 @@ Inductive exp_rel:
   (∀x y.
      exp_rel x y ⇒
        exp_rel (Delay x) (Delay y)) ∧
-[exp_rel_Box:]
-  (∀x y.
-     exp_rel x y ⇒
-       exp_rel (Box x) (Box y)) ∧
 [exp_rel_Force:]
   (∀x y.
      exp_rel x y ⇒
@@ -131,7 +127,7 @@ Inductive exp_rel:
      v_rel (Atom x) (Atom x)) ∧
 [v_rel_Constructor:]
   (∀vs ws.
-     LIST_REL (λv w. v_rel v w ∧ ∃x. v = Thunk (INR x)) vs ws ⇒
+     LIST_REL (λv w. v_rel v w ∧ ∃x. v = Thunk x) vs ws ⇒
        v_rel (Constructor s vs) (Constructor s ws)) ∧
 [v_rel_Monadic:]
   (∀mop xs ys.
@@ -154,15 +150,11 @@ Inductive exp_rel:
                  exp_rel x y ∧
                  ok_binder x) f g ⇒
        v_rel (Recclosure f n) (Recclosure g n)) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      exp_rel x y ∧
      closed x ⇒
-       v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w)))
+       v_rel (Thunk x) (Thunk y))
 End
 
 Theorem v_rel_cases[local] = CONJUNCT2 exp_rel_cases;
@@ -180,10 +172,8 @@ Theorem v_rel_def[simp] =
     “v_rel z (DoTick x)”,
     “v_rel (Atom s) z”,
     “v_rel z (Atom s)”,
-    “v_rel (Thunk (INL s)) z”,
-    “v_rel z (Thunk (INL s))”,
-    “v_rel (Thunk (INR s)) z”,
-    “v_rel z (Thunk (INR s))” ]
+    “v_rel (Thunk s) z”,
+    “v_rel z (Thunk s)” ]
   |> map (SIMP_CONV (srw_ss ()) [Once v_rel_cases])
   |> LIST_CONJ;
 
@@ -344,10 +334,6 @@ Proof
     rw [Once exp_rel_cases]
     \\ simp [subst_def]
     \\ irule exp_rel_Delay \\ gs [])
-  >- ((* Box *)
-    rw [Once exp_rel_cases]
-    \\ simp [subst_def]
-    \\ irule exp_rel_Box \\ gs [])
   >- ((* Force *)
     rw [Once exp_rel_cases]
     \\ simp [subst_def]
@@ -502,7 +488,7 @@ Proof
     \\ imp_res_tac LIST_REL_LENGTH
     >- ((* Cons *)
       first_x_assum (qspec_then ‘k’ assume_tac)
-      \\ ‘($= +++ LIST_REL (λv w. v_rel v w ∧ ∃x. v = Thunk (INR x)))
+      \\ ‘($= +++ LIST_REL (λv w. v_rel v w ∧ ∃x. v = Thunk x))
                            (result_map (eval_to k) xs)
                            (result_map (eval_to k) ys)’
         suffices_by (
@@ -604,7 +590,6 @@ Proof
     >~ [‘dest_Tick w = SOME u’] >- (
       Cases_on ‘v’ \\ gvs []
       \\ simp [dest_anyThunk_def, subst_funs_def]
-      \\ CASE_TAC \\ gvs []
       \\ ‘($= +++ v_rel)
             (eval_to (k - 1) (Force (Value (EL i xs))))
             (eval_to (k - 1) (Force (Value u)))’
@@ -639,7 +624,6 @@ Proof
       \\ first_x_assum (drule_then assume_tac)
       \\ gs [freevars_def])
         (* Thunk *)
-    \\ CASE_TAC \\ gs []
     \\ simp [subst_funs_def]
     \\ first_x_assum irule
     \\ simp [eval_to_wo_def])
@@ -651,14 +635,6 @@ Proof
     \\ ‘($= +++ v_rel) (eval_to k x) (eval_to k y)’
       by (first_x_assum irule \\ simp [eval_to_wo_def, exp_size_def])
     \\ Cases_on ‘eval_to k x’ \\ Cases_on ‘eval_to k y’ \\ gs [])
-  >~ [‘Box x’] >- (
-    strip_tac
-    \\ rw [Once exp_rel_cases]
-    \\ simp [eval_to_def]
-    \\ rename1 ‘exp_rel x y’
-    \\ ‘($= +++ v_rel) (eval_to k x) (eval_to k y)’
-      by (first_x_assum irule \\ simp [eval_to_wo_def, exp_size_def])
-    \\ Cases_on ‘eval_to k x’ \\ Cases_on ‘eval_to k y’ \\ gs [])
   >~ [‘If x1 y1 z1’] >- (
     strip_tac
     \\ rw [Once exp_rel_cases]
@@ -759,8 +735,6 @@ Proof
   rw [rel_ok_def]
   >- ((* ∀x. f x ≠ Err from rel_ok prevents this case *)
     simp [case_proj_apply_closure])
-  >- ((* Thunks go to Thunks or DoTicks *)
-    Cases_on ‘s’ \\ gs [])
   >- ( (* LIST_REL stuff *)
     gvs[LIST_REL_EL_EQN]
     )
@@ -855,10 +829,6 @@ Inductive compile_rel:
   (∀x y.
      compile_rel x y ⇒
        compile_rel (Delay x) (Delay y)) ∧
-[compile_rel_Box:]
-  (∀x y.
-     compile_rel x y ⇒
-       compile_rel (Box x) (Box y)) ∧
 [compile_rel_Force:]
   (∀x y.
      compile_rel x y ⇒
@@ -914,11 +884,6 @@ Proof
     \\ irule_at Any thunk_tickProofTheory.exp_rel_If
     \\ irule_at Any thunk_untickProofTheory.exp_rel_If \\ fs []
     \\ rpt $ first_assum $ irule_at $ Pos hd)
-  >~ [‘Box’] >-
-   (irule_at Any exp_rel_Box
-    \\ irule_at Any thunk_tickProofTheory.exp_rel_Box
-    \\ irule_at Any thunk_untickProofTheory.exp_rel_Box \\ fs []
-    \\ rpt $ first_assum $ irule_at $ Pos hd)
   >~ [‘Force’] >-
    (irule_at Any exp_rel_Force
     \\ irule_at Any thunk_tickProofTheory.exp_rel_Force
diff --git a/compiler/backend/passes/proofs/thunk_case_unboxProofScript.sml b/compiler/backend/passes/proofs/thunk_case_unboxProofScript.sml
index ade74b5b..f694d7cf 100644
--- a/compiler/backend/passes/proofs/thunk_case_unboxProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_case_unboxProofScript.sml
@@ -18,19 +18,19 @@ val _ = new_theory "thunk_case_unboxProof";
 
 val _ = numLib.prefer_num ();
 
-Theorem SUM_REL_def[local,simp] = quotient_sumTheory.SUM_REL_def;
+Theorem SUM_REL_THM[local,simp] = sumTheory.SUM_REL_THM;
 
-Theorem PAIR_REL_def[local,simp] = quotient_pairTheory.PAIR_REL;
+Theorem PAIR_REL_def[local,simp] = pairTheory.PAIR_REL;
 
 Inductive exp_rel:
 (* Force replacement *)
 [exp_rel_Unbox:]
   (∀v.
-     exp_rel (Force (Box (Var v))) (Tick (Var v))) ∧
+     exp_rel (Force (Delay (Var v))) (Tick (Var v))) ∧
 [exp_rel_Unbox_Value:]
   (∀v w.
      v_rel v w ⇒
-       exp_rel (Force (Box (Value v))) (Tick (Value w))) ∧
+       exp_rel (Force (Delay (Value v))) (Tick (Value w))) ∧
 (* Boilerplate: *)
 [exp_rel_App:]
   (∀f g x y.
@@ -69,10 +69,6 @@ Inductive exp_rel:
   (∀x y.
      exp_rel x y ⇒
        exp_rel (Delay x) (Delay y)) ∧
-[exp_rel_Box:]
-  (∀x y.
-     exp_rel x y ⇒
-       exp_rel (Box x) (Box y)) ∧
 [exp_rel_Force:]
   (∀x y.
      exp_rel x y ⇒
@@ -113,14 +109,10 @@ Inductive exp_rel:
                  fn = gn ∧
                  exp_rel x y) f g ⇒
        v_rel (Recclosure f n) (Recclosure g n)) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      exp_rel x y ⇒
-       v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w)))
+       v_rel (Thunk x) (Thunk y))
 End
 
 Theorem v_rel_cases[local] = CONJUNCT2 exp_rel_cases;
@@ -136,10 +128,8 @@ Theorem v_rel_def[simp] =
     “v_rel z (Monadic mop ys)”,
     “v_rel (Atom s) z”,
     “v_rel z (Atom s)”,
-    “v_rel (Thunk (INL s)) z”,
-    “v_rel z (Thunk (INL s))”,
-    “v_rel (Thunk (INR s)) z”,
-    “v_rel z (Thunk (INR s))” ]
+    “v_rel (Thunk s) z”,
+    “v_rel z (Thunk s)” ]
   |> map (SIMP_CONV (srw_ss ()) [Once v_rel_cases])
   |> LIST_CONJ;
 
@@ -242,10 +232,6 @@ Proof
     rw [Once exp_rel_cases]
     \\ simp [subst_def]
     \\ irule exp_rel_Delay \\ gs [])
-  >- ((* Box *)
-    rw [Once exp_rel_cases] \\ gs []
-    \\ simp [subst_def]
-    \\ irule exp_rel_Box \\ gs [])
   >- ((* Force *)
     rw [Once exp_rel_cases]
     \\ simp [subst_def, FILTER_T, ELIM_UNCURRY, exp_rel_Force,
@@ -378,13 +364,13 @@ Proof
       \\ IF_CASES_TAC \\ gs []
       \\ simp [Once eval_to_def]
       \\ simp [Once eval_to_def]
-      \\ simp [subst_funs_def, eval_to_def])
+      \\ simp [dest_anyThunk_def, subst_funs_def, eval_to_def])
     >- ((* Unbox *)
       once_rewrite_tac [eval_to_def]
       \\ IF_CASES_TAC \\ gs []
       \\ simp [Once eval_to_def, subst_funs_def]
       \\ once_rewrite_tac [eval_to_def]
-      \\ simp [dest_anyThunk_def])
+      \\ simp [dest_anyThunk_def, eval_to_def])
     \\ rename1 ‘exp_rel x y’
     \\ CONV_TAC (LAND_CONV (SIMP_CONV (srw_ss()) [Once eval_to_def]))
     \\ CONV_TAC (RAND_CONV (SIMP_CONV (srw_ss()) [Once eval_to_def]))
@@ -419,7 +405,6 @@ Proof
         \\ simp []
         \\ irule LIST_EQ
         \\ gvs [LIST_REL_EL_EQN, EL_MAP, ELIM_UNCURRY])
-      \\ CASE_TAC \\ gs []
       \\ first_x_assum irule
       \\ simp [subst_funs_def, SF SFY_ss])
     \\ ‘∃y. dest_Tick w = SOME y’
@@ -433,13 +418,6 @@ Proof
   >~ [‘Delay x’] >- (
     rw [Once exp_rel_cases] \\ gs []
     \\ simp [eval_to_def])
-  >~ [‘Box x’] >- (
-    strip_tac
-    \\ rw [Once exp_rel_cases] \\ gs []
-    \\ simp [eval_to_def]
-    \\ rename1 ‘exp_rel x y’
-    \\ first_x_assum (drule_then assume_tac)
-    \\ Cases_on ‘eval_to k x’ \\ Cases_on ‘eval_to k y’ \\ gs [])
   >~ [‘MkTick x’] >- (
     strip_tac
     \\ rw [Once exp_rel_cases] \\ gs []
@@ -597,8 +575,6 @@ Proof
   rw [rel_ok_def]
   >- ((* ∀x. f x ≠ Err from rel_ok prevents this case *)
     simp [unbox_apply_closure])
-  >- ((* Thunks go to Thunks or DoTicks *)
-    Cases_on ‘s’ \\ gs [])
   >- (
     gs [Once v_rel_cases])
   >- ((* Equal literals are related *)
@@ -629,4 +605,3 @@ Proof
 QED
 
 val _ = export_theory ();
-
diff --git a/compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml b/compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml
index 04b83431..737ba77b 100644
--- a/compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml
+++ b/compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml
@@ -183,10 +183,6 @@ Inductive combine_rel:
   (∀x y.
      combine_rel x y ⇒
        combine_rel (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀x y.
-     combine_rel x y ⇒
-       combine_rel (Box x) (Box y)) ∧
 [~Force:]
   (∀x y.
      combine_rel x y ⇒
@@ -468,14 +464,10 @@ Inductive combine_rel:
                                                        (MAP2 (λb e. if b then Force e else e) bL2
                                                         (MAP Var vL1))))))
                        g)) n)) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w))) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      combine_rel x y ⇒
-     v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
+     v_rel (Thunk x) (Thunk y)) ∧
 [v_rel_Atom:]
   (∀x.
      v_rel (Atom x) (Atom x)) ∧
@@ -496,7 +488,6 @@ Theorem combine_rel_def =
    “combine_rel (Let s x y) z”,
    “combine_rel (If x y z) w”,
    “combine_rel (Delay x) y”,
-   “combine_rel (Box x) y”,
    “combine_rel (MkTick x) y”,
    “combine_rel (Force x) y”]
   |> map (SIMP_CONV (srw_ss()) [Once combine_rel_cases])
@@ -1175,9 +1166,6 @@ Proof
   >~ [‘Delay x’] >- (
     rw [subst_def]
     \\ gs [combine_rel_Delay])
-  >~ [‘Box x’] >- (
-    rw [subst_def]
-    \\ gs [combine_rel_Box])
   >~ [‘Force x’] >- (
     rw [subst_def]
     \\ gs [combine_rel_Force])
@@ -1513,6 +1501,7 @@ Theorem combine_rel_eval_to:
     combine_rel x y ⇒
       ∃j. ($= +++ v_rel) (eval_to k x) (eval_to (j + k) y)
 Proof
+  cheat (*
   completeInduct_on ‘k’ \\ completeInduct_on ‘exp_size x’
   \\ Cases \\ gvs [PULL_FORALL, exp_size_def] \\ rw []
   >~ [‘Var m’] >- (
@@ -1529,15 +1518,6 @@ Proof
     \\ gvs [eval_to_def, v_rel_Closure])
   >~ [‘Delay x’] >- (
     gvs [Once combine_rel_def, eval_to_def, v_rel_def])
-  >~ [‘Box x’] >- (
-    gvs [Once combine_rel_def, eval_to_def]
-    \\ rename1 ‘combine_rel x y’
-    \\ first_x_assum $ qspecl_then [‘x’, ‘y’] mp_tac \\ gs []
-    \\ impl_tac >- (strip_tac \\ gvs [])
-    \\ disch_then $ qx_choose_then ‘j’ assume_tac
-    \\ qexists_tac ‘j’
-    \\ Cases_on ‘eval_to k x’ \\ Cases_on ‘eval_to (j + k) y’ \\ gs []
-    \\ simp [v_rel_def])
   >~ [`Monad mop xs`]
   >- (
     gvs[Once combine_rel_def, eval_to_def] >> rw[Once v_rel_def, SF SFY_ss]
@@ -6541,6 +6521,7 @@ Proof
       \\ rpt (first_x_assum (drule_all_then assume_tac))
       \\ Cases_on ‘eval_to k (EL n xs)’
       \\ Cases_on ‘eval_to (j + k) (EL n ys)’ \\ gs [v_rel_def]))
+*)
 QED
 
 Theorem combine_rel_eval:
diff --git a/compiler/backend/passes/proofs/thunk_force_delayScript.sml b/compiler/backend/passes/proofs/thunk_force_delayScript.sml
index 221942f8..3b1d402b 100644
--- a/compiler/backend/passes/proofs/thunk_force_delayScript.sml
+++ b/compiler/backend/passes/proofs/thunk_force_delayScript.sml
@@ -53,10 +53,6 @@ Inductive force_delay_rel:
   (∀x y.
      force_delay_rel x y ⇒
        force_delay_rel (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀x y.
-     force_delay_rel x y ⇒
-       force_delay_rel (Box x) (Box y)) ∧
 [~Force:]
   (∀x y.
      force_delay_rel x y ⇒
@@ -80,7 +76,6 @@ Theorem force_delay_rel_def =
    “force_delay_rel (Let s x y) z”,
    “force_delay_rel (If x y z) w”,
    “force_delay_rel (Delay x) y”,
-   “force_delay_rel (Box x) y”,
    “force_delay_rel (MkTick x) y”,
    “force_delay_rel (Force x) y”]
   |> map (SIMP_CONV (srw_ss()) [Once force_delay_rel_cases])
@@ -134,10 +129,6 @@ Inductive exp_rel:
   (∀x y.
      exp_rel x y ⇒
        exp_rel (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀x y.
-     exp_rel x y ⇒
-       exp_rel (Box x) (Box y)) ∧
 [~Force:]
   (∀x y.
      exp_rel x y ⇒
@@ -167,14 +158,10 @@ Inductive exp_rel:
      EVERY ok_bind (MAP SND g) ∧
      LIST_REL exp_rel (MAP SND f) (MAP SND g) ⇒
      v_rel (Recclosure f n) (Recclosure g n)) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w))) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      exp_rel x y ⇒
-     v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
+     v_rel (Thunk x) (Thunk y)) ∧
 [v_rel_Atom:]
   (∀x.
      v_rel (Atom x) (Atom x)) ∧
@@ -195,7 +182,6 @@ Theorem exp_rel_def =
    “exp_rel (Let s x y) z”,
    “exp_rel (If x y z) w”,
    “exp_rel (Delay x) y”,
-   “exp_rel (Box x) y”,
    “exp_rel (MkTick x) y”,
    “exp_rel (Force x) y”]
   |> map (SIMP_CONV (srw_ss()) [Once exp_rel_cases])
@@ -229,7 +215,7 @@ Proof
         gen_tac >> strip_tac >> last_x_assum irule >>
         first_x_assum $ irule_at $ Pos last >> simp [] >>
         rename1 ‘EL x l’ >>
-        ‘exp_size (EL x l) ≤ exp4_size l’ suffices_by gvs [] >>
+        ‘exp_size (EL x l) ≤ exp3_size l’ suffices_by gvs [] >>
         assume_tac exp_size_lemma >> fs [] >>
         first_x_assum irule >> gs [EL_MEM])
     >- (AP_TERM_TAC >> AP_TERM_TAC >>
@@ -237,7 +223,7 @@ Proof
         gen_tac >> strip_tac >> last_x_assum irule >>
         first_x_assum $ irule_at $ Pos last >> simp [] >>
         rename1 ‘EL x l’ >>
-        ‘exp_size (EL x l) ≤ exp4_size l’ suffices_by gvs [] >>
+        ‘exp_size (EL x l) ≤ exp3_size l’ suffices_by gvs [] >>
         assume_tac exp_size_lemma >> fs [] >>
         first_x_assum irule >> gs [EL_MEM])
     >- (MK_COMB_TAC >- (AP_TERM_TAC >> gs []) >> gs [])
@@ -359,9 +345,6 @@ Proof
   >~ [‘Delay x’] >- (
     rw [subst_def]
     \\ gs [exp_rel_Delay])
-  >~ [‘Box x’] >- (
-    rw [subst_def]
-    \\ gs [exp_rel_Box])
   >~ [‘Force x’] >- (
     rw [subst_def]
     \\ gs [exp_rel_Force])
@@ -553,12 +536,6 @@ Proof
   >~ [‘Delay x’] >- (
     rw [Once exp_rel_cases] \\ gs []
     \\ simp [eval_to_def, v_rel_def])
-  >~ [‘Box x’] >- (
-    rw [exp_rel_def] \\ gs []
-    \\ simp [eval_to_def]
-    \\ rename1 ‘exp_rel x y’
-    \\ first_x_assum $ drule_then assume_tac
-    \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to k x’ \\ gs [v_rel_def])
   >~ [‘MkTick x’] >- (
     rw [exp_rel_def] \\ gs []
     \\ simp [eval_to_def]
@@ -844,7 +821,6 @@ Proof
   >- metis_tac []
   >- metis_tac []
   >- metis_tac []
-  >- metis_tac []
   >- (
     Q.REFINE_EXISTS_TAC ‘Force _’ \\ gs [clean_rel_def]
     \\ metis_tac [])
diff --git a/compiler/backend/passes/proofs/thunk_let_forceProofScript.sml b/compiler/backend/passes/proofs/thunk_let_forceProofScript.sml
index 7ce555fe..536a05ee 100644
--- a/compiler/backend/passes/proofs/thunk_let_forceProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_let_forceProofScript.sml
@@ -18,16 +18,15 @@ open pure_miscTheory thunkLangPropsTheory;
 val _ = new_theory "thunk_let_forceProof";
 
 val _ = set_grammar_ancestry ["finite_map", "pred_set", "rich_list",
-                              "thunkLang", "wellorder", "quotient_sum",
-                              "quotient_pair", "thunkLangProps"];
+                              "thunkLang", "wellorder", "thunkLangProps"];
 
 Overload safe_itree = “pure_semantics$safe_itree”
 
 val _ = numLib.prefer_num ();
 
-Theorem SUM_REL_def[local,simp] = quotient_sumTheory.SUM_REL_def;
+Theorem SUM_REL_THM[local,simp] = sumTheory.SUM_REL_THM;
 
-Theorem PAIR_REL_def[local,simp] = quotient_pairTheory.PAIR_REL;
+Theorem PAIR_REL_def[local,simp] = pairTheory.PAIR_REL;
 
 Datatype:
   lhs = Var string | Val thunkLang$v
@@ -106,10 +105,6 @@ Inductive exp_rel:
   (∀m x y.
      exp_rel m x y ⇒
        exp_rel m (Delay x) (Delay y)) ∧
-[exp_rel_Box:]
-  (∀m x y.
-     exp_rel m x y ⇒
-       exp_rel m (Box x) (Box y)) ∧
 [exp_rel_Force:]
   (∀m x y.
      exp_rel m x y ⇒
@@ -149,14 +144,10 @@ Inductive exp_rel:
      LIST_REL (λ(fn,x) (gn,y). fn = gn ∧ exp_rel NONE x y ∧
                                freevars x ⊆ set (MAP FST f)) f g ⇒
        v_rel (Recclosure f n) (Recclosure g n)) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      exp_rel NONE x y ∧ closed x ⇒
-       v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w)))
+       v_rel (Thunk x) (Thunk y))
 End
 
 Theorem v_rel_cases[local] = CONJUNCT2 exp_rel_cases;
@@ -173,8 +164,8 @@ Theorem v_rel_def[simp] =
     “v_rel z (Monadic mop ys)”,
     “v_rel (Atom x) z”,
     “v_rel z (Atom x)”,
-    “v_rel (Thunk (INL x)) z”,
-    “v_rel z (Thunk (INR x))” ]
+    “v_rel (Thunk x) z”,
+    “v_rel z (Thunk x)” ]
   |> map (SIMP_CONV (srw_ss()) [Once v_rel_cases])
   |> LIST_CONJ;
 
@@ -459,10 +450,6 @@ Proof
    (fs [subst_def]
     \\ irule exp_rel_Delay
     \\ first_x_assum irule \\ fs [])
-  >~ [‘Box’] >-
-   (fs [subst_def]
-    \\ irule exp_rel_Box
-    \\ first_x_assum irule \\ fs [])
   >~ [‘Lam’] >-
    (fs [subst_def]
     \\ irule exp_rel_Lam \\ fs [subst_acc_def]
@@ -623,8 +610,6 @@ Proof
     \\ fs [ALOOKUP_NONE,MAP_REVERSE] \\ gvs []
     \\ irule exp_rel_Value
     \\ drule_all ALOOKUP_REVERSE_REVERSE \\ fs [])
-  >~ [‘v_rel (Thunk (INL v))’] >-
-   (irule v_rel_Thunk_INL \\ fs [])
   \\ simp [Once v_rel_cases] \\ fs [SF ETA_ss]
   \\ last_x_assum mp_tac
   \\ match_mp_tac LIST_REL_mono \\ fs [FORALL_PROD]
@@ -1088,65 +1073,54 @@ Proof
         \\ qpat_assum ‘_ = INL Type_error’ (SUBST1_TAC o SYM)
         \\ irule eval_to_mono \\ gs []))
     \\ simp [subst_funs_def]
-    \\ reverse CASE_TAC \\ gs []
+    \\ rename1 ‘exp_rel _ x1 y1’
+    \\ Cases_on ‘eval_to (k - 1) y1 = INL Diverge’
     >- (
-      rename1 ‘exp_rel _ x1 y1’
-      \\ Cases_on ‘eval_to (k - 1) y1 = INL Diverge’
-      >- (
-        Cases_on ‘eval_to k x = INL Diverge’
-        >- (
-          qexists_tac ‘0’
-          \\ simp [])
-        \\ ‘∀j. eval_to (j + k) x = eval_to k x’
-          by (gen_tac \\ irule eval_to_mono \\ gs [])
-        \\ gvs []
-        \\ ‘∀j. j + k - 1 = j + (k - 1)’ by gs []
-        \\ asm_simp_tac std_ss []
-        \\ qpat_assum `_ = INL Diverge` (SUBST1_TAC o SYM)
-        \\ first_x_assum irule
-        \\ gs [eval_to_wo_def]
-        \\ qx_gen_tac ‘j’
-        \\ strip_tac
-        \\ qpat_x_assum ‘∀k. eval_to _ (Force _) ≠ _’ mp_tac
-        \\ simp [Once eval_to_def]
-        \\ qexists_tac ‘j + k’
-        \\ asm_simp_tac std_ss []
-        \\ simp [dest_anyThunk_def, subst_funs_def]
-        \\ qpat_assum ‘_ = INL Type_error’ (SUBST1_TAC o SYM)
-        \\ irule eval_to_mono \\ gs [])
-      \\ ‘∀j1. eval_to (j1 + j + k) x = eval_to (j + k) x’
-        by (gen_tac \\ irule eval_to_mono \\ gs [])
-      \\ Q.REFINE_EXISTS_TAC ‘j1 + j’ \\ gs []
-      \\ ‘∃j. ($= +++ v_rel) (eval_to (j + (k - 1)) x1)
-                                 (eval_to (k - 1) y1)’
-        suffices_by (
-          disch_then (qx_choose_then ‘j1’ assume_tac)
-          \\ ‘eval_to (j1 + j + k - 1) x1 =
-              eval_to (j1 + k - 1) x1’
-            by (irule eval_to_mono \\ gs []
-                \\ strip_tac \\ gs []
-                \\ Cases_on ‘eval_to (k - 1) y1’ \\ gs [])
-          \\ qexists_tac ‘j1’ \\ gs [])
-      \\ first_x_assum irule
-      \\ gs [eval_to_wo_def]
-      \\ qx_gen_tac ‘j1’
-      \\ strip_tac
-      \\ qpat_x_assum ‘∀k. eval_to _ (Force _) ≠ _’ mp_tac
-      \\ simp [Once eval_to_def]
-      \\ qexists_tac ‘j + (j1 + k)’
-      \\ asm_simp_tac std_ss []
-      \\ simp [dest_anyThunk_def, subst_funs_def]
-      \\ qpat_assum ‘_ = INL Type_error’ (SUBST1_TAC o SYM)
-      \\ irule eval_to_mono \\ gs [])
+     Cases_on ‘eval_to k x = INL Diverge’
+     >- (
+       qexists_tac ‘0’
+       \\ simp [])
+     \\ ‘∀j. eval_to (j + k) x = eval_to k x’
+       by (gen_tac \\ irule eval_to_mono \\ gs [])
+     \\ gvs []
+     \\ ‘∀j. j + k - 1 = j + (k - 1)’ by gs []
+     \\ asm_simp_tac std_ss []
+     \\ qpat_assum `_ = INL Diverge` (SUBST1_TAC o SYM)
+     \\ first_x_assum irule
+     \\ gs [eval_to_wo_def]
+     \\ qx_gen_tac ‘j’
+     \\ strip_tac
+     \\ qpat_x_assum ‘∀k. eval_to _ (Force _) ≠ _’ mp_tac
+     \\ simp [Once eval_to_def]
+     \\ qexists_tac ‘j + k’
+     \\ asm_simp_tac std_ss []
+     \\ simp [dest_anyThunk_def, subst_funs_def]
+     \\ qpat_assum ‘_ = INL Type_error’ (SUBST1_TAC o SYM)
+     \\ irule eval_to_mono \\ gs [])
     \\ ‘∀j1. eval_to (j1 + j + k) x = eval_to (j + k) x’
       by (gen_tac \\ irule eval_to_mono \\ gs [])
-    \\ Q.REFINE_EXISTS_TAC ‘j + j1’ \\ gs []
-    \\ rgs [Once (CONJUNCT2 exp_rel_cases)] \\ rw []
-    \\ rename1 ‘eval_to k1 x1 = INR v1’
-    \\ qexists_tac ‘j1 + k1’
-    \\ ‘eval_to (k + k1 + j + j1 - 1) x1 = eval_to k1 x1’
-      by (irule eval_to_mono \\ gs [])
-    \\ gs [])
+    \\ Q.REFINE_EXISTS_TAC ‘j1 + j’ \\ gs []
+    \\ ‘∃j. ($= +++ v_rel) (eval_to (j + (k - 1)) x1)
+                           (eval_to (k - 1) y1)’
+      suffices_by (
+      disch_then (qx_choose_then ‘j1’ assume_tac)
+      \\ ‘eval_to (j1 + j + k - 1) x1 =
+          eval_to (j1 + k - 1) x1’
+        by (irule eval_to_mono \\ gs []
+            \\ strip_tac \\ gs []
+            \\ Cases_on ‘eval_to (k - 1) y1’ \\ gs [])
+      \\ qexists_tac ‘j1’ \\ gs [])
+    \\ first_x_assum irule
+    \\ gs [eval_to_wo_def]
+    \\ qx_gen_tac ‘j1’
+    \\ strip_tac
+    \\ qpat_x_assum ‘∀k. eval_to _ (Force _) ≠ _’ mp_tac
+    \\ simp [Once eval_to_def]
+    \\ qexists_tac ‘j + (j1 + k)’
+    \\ asm_simp_tac std_ss []
+    \\ simp [dest_anyThunk_def, subst_funs_def]
+    \\ qpat_assum ‘_ = INL Type_error’ (SUBST1_TAC o SYM)
+    \\ irule eval_to_mono \\ gs [])
   >~ [‘Lam s x’] >-
    (ntac 2 strip_tac
     \\ rw [Once exp_rel_cases]
@@ -1155,20 +1129,6 @@ Proof
    (ntac 2 strip_tac
     \\ rw [Once exp_rel_cases]
     \\ simp [eval_to_def])
-  >~ [‘Box x’] >-
-   (ntac 2 strip_tac
-    \\ rw [Once exp_rel_cases]
-    \\ rename1 ‘exp_rel _ x y’
-    \\ simp [eval_to_def]
-    \\ ‘∃j. ($= +++ v_rel) (eval_to (j + k) x) (eval_to k y)’
-      suffices_by (
-        disch_then (qx_choose_then ‘j’ assume_tac)
-        \\ qexists_tac ‘j’
-        \\ Cases_on ‘eval_to (j + k) x’ \\ Cases_on ‘eval_to k y’ \\ gs [])
-    \\ first_x_assum irule \\ simp [eval_to_wo_def, exp_size_def]
-    \\ rpt strip_tac
-    \\ first_x_assum (qspec_then ‘k’ mp_tac)
-    \\ simp [eval_to_def])
   >~ [‘App f x’] >-
    (ntac 2 strip_tac
     \\ rw [Once exp_rel_cases]
@@ -1942,9 +1902,6 @@ Proof
   rw [rel_ok_def]
   >- ((* ∀x. f x ≠ Err from rel_ok prevents this case *)
     simp [force_apply_closure])
-  >- ((* Thunks go to Thunks or DoTicks *)
-    Cases_on ‘s’ \\ gs []
-    \\ gs [Once v_rel_cases])
   >- ((* Equal literals are related *)
     simp [exp_rel_Prim])
   >- ((* Equal 0-arity conses are related *)
@@ -2033,10 +1990,6 @@ Inductive e_rel:
   (∀m x y.
      e_rel m x y ⇒
        e_rel m (Delay x) (Delay y)) ∧
-[e_rel_Box:]
-  (∀m x y.
-     e_rel m x y ⇒
-       e_rel m (Box x) (Box y)) ∧
 [e_rel_Force:]
   (∀m x y.
      e_rel m x y ⇒
@@ -2174,18 +2127,6 @@ Proof
     \\ reverse Induct \\ fs [PULL_EXISTS] \\ rw []
     \\ irule_at Any exp_rel_Delay \\ fs []
     \\ last_x_assum $ drule_then $ irule_at Any \\ fs [])
-  >~ [‘Box’] >-
-   (qexists_tac ‘k’ \\ fs [] \\ rw []
-    \\ last_x_assum $ dxrule_then assume_tac \\ pop_assum mp_tac
-    \\ qid_spec_tac ‘x’ \\ qid_spec_tac ‘y’ \\ qid_spec_tac ‘k1’
-    \\ reverse Induct \\ fs [PULL_EXISTS] \\ rw []
-    >- (last_x_assum $ drule_then $ irule_at Any
-        \\ irule_at Any exp_rel_Box \\ fs [])
-    \\ pop_assum mp_tac
-    \\ qid_spec_tac ‘x’ \\ qid_spec_tac ‘y’ \\ qid_spec_tac ‘m’
-    \\ reverse Induct \\ fs [PULL_EXISTS] \\ rw []
-    \\ irule_at Any exp_rel_Box \\ fs []
-    \\ last_x_assum $ drule_then $ irule_at Any \\ fs [])
   >~ [‘Force’] >-
    (qexists_tac ‘k’ \\ fs [] \\ rw []
     \\ last_x_assum $ dxrule_then assume_tac \\ pop_assum mp_tac
diff --git a/compiler/backend/passes/proofs/thunk_let_force_1ProofScript.sml b/compiler/backend/passes/proofs/thunk_let_force_1ProofScript.sml
index a47121af..e0afebe2 100644
--- a/compiler/backend/passes/proofs/thunk_let_force_1ProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_let_force_1ProofScript.sml
@@ -20,8 +20,8 @@ val _ = new_theory "thunk_let_force_1Proof";
 
 val _ = set_grammar_ancestry ["thunk_let_force", "thunk_let_forceProof","thunk_cexp",
                               "finite_map", "pred_set", "rich_list",
-                              "thunkLang", "wellorder", "quotient_sum",
-                              "quotient_pair", "thunkLangProps", "thunk_exp_of"];
+                              "thunkLang", "wellorder",
+                              "thunkLangProps", "thunk_exp_of"];
 
 Overload safe_itree = “pure_semantics$safe_itree”
 
@@ -85,9 +85,6 @@ Proof
   >~ [‘Delay’] >-
    (fs [let_force_def] \\ rw [] \\ irule e_rel_Delay
     \\ first_x_assum irule \\ fs [])
-  >~ [‘Box’] >-
-   (fs [let_force_def] \\ rw [] \\ irule e_rel_Box
-    \\ first_x_assum irule \\ fs [])
   >~ [‘Force’] >-
    (rw [] \\ fs [let_force_def]
     \\ CASE_TAC \\ gvs []
diff --git a/compiler/backend/passes/proofs/thunk_remove_unuseful_bindingsScript.sml b/compiler/backend/passes/proofs/thunk_remove_unuseful_bindingsScript.sml
index e005dd91..85217747 100644
--- a/compiler/backend/passes/proofs/thunk_remove_unuseful_bindingsScript.sml
+++ b/compiler/backend/passes/proofs/thunk_remove_unuseful_bindingsScript.sml
@@ -87,10 +87,6 @@ Inductive clean_rel:
   (∀x y.
      clean_rel x y ⇒
        clean_rel (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀x y.
-     clean_rel x y ⇒
-       clean_rel (Box x) (Box y)) ∧
 [~Force:]
   (∀x y.
      clean_rel x y ⇒
@@ -127,14 +123,10 @@ Inductive clean_rel:
      LIST_REL clean_rel (MAP SND f) (MAP SND g) ∧
      EVERY (λe. v ∉ freevars e) (MAP SND f) ⇒
      v_rel (Recclosure (SNOC (v,w) f) n) (Recclosure g n)) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w))) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      clean_rel x y ⇒
-     v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
+     v_rel (Thunk x) (Thunk y)) ∧
 [v_rel_Atom:]
   (∀x.
      v_rel (Atom x) (Atom x)) ∧
@@ -155,7 +147,6 @@ Theorem clean_rel_def =
    “clean_rel (Let s x y) z”,
    “clean_rel (If x y z) w”,
    “clean_rel (Delay x) y”,
-   “clean_rel (Box x) y”,
    “clean_rel (MkTick x) y”,
    “clean_rel (Force x) y”]
   |> map (SIMP_CONV (srw_ss()) [Once clean_rel_cases])
@@ -286,7 +277,6 @@ Proof
   >- (first_x_assum irule \\ gvs [] \\ rpt $ first_x_assum $ irule_at Any)
   >- (first_x_assum irule \\ gvs [] \\ rpt $ first_x_assum $ irule_at Any)
   >- (first_x_assum irule \\ gvs [] \\ rpt $ first_x_assum $ irule_at Any)
-  >- (first_x_assum irule \\ gvs [] \\ rpt $ first_x_assum $ irule_at Any)
 QED
 
 Theorem exp1_size_append:
@@ -387,8 +377,6 @@ Proof
       \\ rpt $ first_x_assum $ irule_at Any)
   >- (last_x_assum irule \\ simp []
       \\ rpt $ first_x_assum $ irule_at Any)
-  >- (last_x_assum irule \\ simp []
-      \\ rpt $ first_x_assum $ irule_at Any)
 QED
 
 Theorem clean_rel_subst:
@@ -536,9 +524,6 @@ Proof
   >~ [‘Delay x’] >- (
     rw [subst_def]
     \\ gs [clean_rel_Delay])
-  >~ [‘Box x’] >- (
-    rw [subst_def]
-    \\ gs [clean_rel_Box])
   >~ [‘Force x’] >- (
     rw [subst_def]
     \\ gs [clean_rel_Force])
@@ -1051,13 +1036,6 @@ Proof
   >~ [‘Delay x’] >- (
     rw [Once clean_rel_cases] \\ gs []
     \\ simp [eval_to_def, v_rel_def])
-  >~ [‘Box x’] >- (
-    rw [clean_rel_def] \\ gs []
-    \\ simp [eval_to_def]
-    \\ rename1 ‘clean_rel x y’
-    \\ first_x_assum $ drule_then $ qx_choose_then ‘j’ assume_tac
-    \\ qexists_tac ‘j’
-    \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to (k + j) x’ \\ gs [v_rel_def])
   >~ [‘MkTick x’] >- (
     rw [clean_rel_def] \\ gs [eval_to_def]
     \\ first_x_assum $ dxrule_then $ qx_choose_then ‘j’ assume_tac
diff --git a/compiler/backend/passes/proofs/thunk_split_Delay_LamProofScript.sml b/compiler/backend/passes/proofs/thunk_split_Delay_LamProofScript.sml
index 6fc7db39..efa54461 100644
--- a/compiler/backend/passes/proofs/thunk_split_Delay_LamProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_split_Delay_LamProofScript.sml
@@ -112,14 +112,6 @@ Proof
   Induct \\ gvs [replace_Force_def]
 QED
 
-Theorem FOLDL_replace_Force_Box:
-  ∀map_l map x.
-    FOLDL (λe v. replace_Force (Var (explode (to_fmap map ' v))) (explode v) e) (Box x) map_l
-    = Box (FOLDL (λe v. replace_Force (Var (explode (to_fmap map ' v))) (explode v) e) x map_l)
-Proof
-  Induct \\ gvs [replace_Force_def]
-QED
-
 Theorem FOLDL_replace_Force_If:
   ∀map_l map x y z.
     FOLDL (λe v. replace_Force (Var (explode (to_fmap map ' v))) (explode v) e) (If x y z) map_l
@@ -1493,12 +1485,6 @@ Proof
       \\ pop_assum $ dxrule_then assume_tac \\ gs []
       \\ metis_tac [SUBSET_TRANS])
   >~[‘Delay e’]
-  >- (rpt $ gen_tac \\ strip_tac
-      \\ last_x_assum irule
-      \\ pairarg_tac \\ gs []
-      \\ first_x_assum $ irule_at Any
-      \\ simp [cexp_size_def])
-  >~[‘Box e’]
   >- (rpt $ gen_tac \\ strip_tac
       \\ last_x_assum irule
       \\ pairarg_tac \\ gs []
@@ -3567,16 +3553,6 @@ Proof
       \\ gvs [exp_of_def, FOLDL_replace_Force_Delay, exp_rel1_def, exp_rel2_def,
               freevars_def, boundvars_def, cexp_wf_def, PULL_EXISTS, cns_arities_def]
       \\ metis_tac [])
-  >~[‘Box _’]
-
-  >- (rename1 ‘split_Delayed_Lam e _ _’
-      \\ rpt $ gen_tac \\ pairarg_tac
-      \\ gvs [PULL_FORALL] \\ strip_tac
-      \\ last_x_assum $ qspec_then ‘e’ assume_tac \\ fs [cexp_size_def]
-      \\ pop_assum $ drule_all_then $ qx_choose_then ‘e_mid’ assume_tac
-      \\ gvs [exp_of_def, FOLDL_replace_Force_Box, exp_rel1_def, exp_rel2_def,
-              freevars_def, boundvars_def, cexp_wf_def, PULL_EXISTS, cns_arities_def]
-      \\ metis_tac [])
   >~[‘Force (exp_of e)’]
 
   >- (Cases_on ‘dest_Var e’ \\ gvs []
diff --git a/compiler/backend/passes/proofs/thunk_split_Forcing_LamProofScript.sml b/compiler/backend/passes/proofs/thunk_split_Forcing_LamProofScript.sml
index 241160b2..3add76fa 100644
--- a/compiler/backend/passes/proofs/thunk_split_Forcing_LamProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_split_Forcing_LamProofScript.sml
@@ -1442,12 +1442,6 @@ Proof
               Induct_on ‘l’ >> simp [FORALL_PROD, Disj_def, exp_rel_def]) >>
           simp [exp_rel_def, exp_rel_lets_for]))
   >~[‘Delay (exp_of e)’]
-  >- (strip_tac >> gs [PULL_FORALL] >>
-      last_x_assum $ qspec_then ‘e’ assume_tac >>
-      gen_tac >> pairarg_tac >> gs [boundvars_def, freevars_def, exp_rel_def] >>
-      gen_tac >> strip_tac >> simp [cexp_wf_def] >>
-      last_x_assum $ dxrule_then assume_tac >> gs [])
-  >~[‘Box (exp_of e)’]
   >- (strip_tac >> gs [PULL_FORALL] >>
       last_x_assum $ qspec_then ‘e’ assume_tac >>
       gen_tac >> pairarg_tac >> gs [boundvars_def, freevars_def, exp_rel_def] >>
diff --git a/compiler/backend/passes/proofs/thunk_tickProofScript.sml b/compiler/backend/passes/proofs/thunk_tickProofScript.sml
index 012e060d..1a921b6a 100644
--- a/compiler/backend/passes/proofs/thunk_tickProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_tickProofScript.sml
@@ -11,12 +11,12 @@ open pure_miscTheory thunkLangPropsTheory thunk_semanticsTheory;
 val _ = new_theory "thunk_tickProof";
 
 val _ = set_grammar_ancestry [
-  "finite_map", "pred_set", "rich_list", "thunkLang", "quotient_sum",
-  "quotient_pair", "thunkLangProps", "thunk_semantics" ];
+  "finite_map", "pred_set", "rich_list", "thunkLang",
+  "thunkLangProps", "thunk_semantics" ];
 
-Theorem SUM_REL_def[local,simp] = quotient_sumTheory.SUM_REL_def;
+Theorem SUM_REL_THM[local,simp] = sumTheory.SUM_REL_THM;
 
-Theorem PAIR_REL_THM[local,simp] = quotient_pairTheory.PAIR_REL_THM;
+Theorem PAIR_REL_THM[local,simp] = pairTheory.PAIR_REL_THM;
 
 val _ = numLib.prefer_num ();
 
@@ -73,10 +73,6 @@ Inductive exp_rel:
   (∀x y.
      exp_rel x y ⇒
        exp_rel (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀x y.
-     exp_rel x y ⇒
-       exp_rel (Box x) (Box y)) ∧
 [~Force:]
   (∀x y.
      exp_rel x y ⇒
@@ -104,14 +100,10 @@ Inductive exp_rel:
      EVERY ok_bind (MAP SND g) ∧
      LIST_REL exp_rel (MAP SND f) (MAP SND g) ⇒
        v_rel (Recclosure f n) (Recclosure g n)) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w))) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      exp_rel x y ⇒
-       v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
+       v_rel (Thunk x) (Thunk y)) ∧
 [v_rel_Atom:]
   (∀x.
      v_rel (Atom x) (Atom x)) ∧
@@ -132,7 +124,6 @@ Theorem exp_rel_def =
    “exp_rel (Let s x y) z”,
    “exp_rel (If x y z) w”,
    “exp_rel (Delay x) y”,
-   “exp_rel (Box x) y”,
    “exp_rel (MkTick x) y”,
    “exp_rel (Force x) y”]
   |> map (SIMP_CONV (srw_ss()) [Once exp_rel_cases])
@@ -240,10 +231,6 @@ Proof
     qexists_tac ‘0’
     \\ irule_at Any exp_rel_Delay
     \\ gs [])
-  >~ [‘Box x’] >- (
-    qexists_tac ‘0’
-    \\ irule_at Any exp_rel_Box
-    \\ gs [])
   >~ [‘Force x’] >- (
     qexists_tac ‘0’
     \\ irule_at Any exp_rel_Force
@@ -347,9 +334,6 @@ Proof
   >~ [‘Delay x’] >- (
     rw [subst_def]
     \\ gs [exp_rel_Delay])
-  >~ [‘Box x’] >- (
-    rw [subst_def]
-    \\ gs [exp_rel_Box])
   >~ [‘Force x’] >- (
     rw [subst_def]
     \\ gs [exp_rel_Force])
@@ -704,20 +688,6 @@ Proof
     \\ Q.REFINE_EXISTS_TAC ‘j + n’
     \\ once_rewrite_tac [DECIDE “j + n + k = (j + k) + n”]
     \\ simp [eval_to_Tick, eval_to_def, v_rel_def])
-  >~ [‘Box x’] >- (
-    dxrule_then assume_tac exp_rel_FUNPOW \\ gvs []
-    \\ gvs [Once exp_rel_def]
-    \\ Q.REFINE_EXISTS_TAC ‘j + n’
-    \\ once_rewrite_tac [DECIDE “j + n + k = (j + k) + n”]
-    \\ simp [eval_to_Tick, eval_to_def]
-    \\ rename1 ‘exp_rel x y’
-    \\ ‘∃j. ($= +++ v_rel) (eval_to k x) (eval_to (j + k) y)’
-      suffices_by (
-        disch_then (qx_choose_then ‘j’ assume_tac)
-        \\ qexists_tac ‘j’
-        \\ Cases_on ‘eval_to k x’ \\ Cases_on ‘eval_to (j + k) y’ \\ gs []
-        \\ simp [v_rel_def])
-    \\ first_x_assum (irule_at Any) \\ gs [])
   >~ [‘Force x’] >- (
     dxrule_then assume_tac exp_rel_FUNPOW \\ gvs []
     \\ rgs [Once exp_rel_def]
@@ -752,8 +722,9 @@ Proof
         \\ rw [Once exp_rel_cases] \\ gs []
         \\ Cases_on ‘x0’ \\ gvs [])
       \\ pairarg_tac \\ gvs []
+      \\ rename1 ‘dest_anyThunk v1 = INR (wx, binds)’
       \\ ‘∃wx' binds'. dest_anyThunk w1 = INR (wx', binds') ∧
-                       (v_rel +++ exp_rel) wx wx' ∧
+                       exp_rel wx wx' ∧
                        MAP FST binds = MAP FST binds' ∧
                        EVERY ok_bind (MAP SND binds) ∧
                        EVERY ok_bind (MAP SND binds') ∧
@@ -771,12 +742,6 @@ Proof
             \\ gvs [EVERY_EL, EL_MAP]
             \\ first_x_assum (drule_then assume_tac)
             \\ gvs [ok_bind_def])
-      \\ CASE_TAC \\ gs []
-      >- (
-        qexists_tac ‘j’ \\ simp []
-        \\ CASE_TAC \\ gs []
-        \\ Cases_on ‘v1’ \\ Cases_on ‘w1’ \\ gs [dest_anyThunk_def])
-      \\ Cases_on ‘wx'’ \\ gs []
       \\ rename1 ‘exp_rel x1 x2’
       \\ ‘exp_rel (subst_funs binds x1) (subst_funs binds' x2)’
         by (simp [subst_funs_def]
diff --git a/compiler/backend/passes/proofs/thunk_to_envProofScript.sml b/compiler/backend/passes/proofs/thunk_to_envProofScript.sml
index 653fe0fb..5ce88233 100644
--- a/compiler/backend/passes/proofs/thunk_to_envProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_to_envProofScript.sml
@@ -65,8 +65,6 @@ Proof
    (fs [to_env_def] \\ irule exp_rel_Delay \\ fs [cexp_wf_def])
   >~ [‘Force’] >-
    (fs [to_env_def] \\ irule exp_rel_Force \\ fs [cexp_wf_def])
-  >~ [‘Box’] >-
-   (fs [to_env_def] \\ irule exp_rel_Box \\ fs [cexp_wf_def])
   >~ [‘Letrec’] >-
    (fs [to_env_def] \\ irule exp_rel_Letrec \\ fs [cexp_wf_def]
     \\ fs [GSYM MAP_REVERSE,MAP_MAP_o,combinTheory.o_DEF]
diff --git a/compiler/backend/passes/proofs/thunk_to_env_1ProofScript.sml b/compiler/backend/passes/proofs/thunk_to_env_1ProofScript.sml
index 832e2878..e776548b 100644
--- a/compiler/backend/passes/proofs/thunk_to_env_1ProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_to_env_1ProofScript.sml
@@ -79,10 +79,6 @@ Inductive exp_rel:
   (∀env x y.
      exp_rel env x y ⇒
        exp_rel env (Delay x) (Delay y)) ∧
-[exp_rel_Box:]
-  (∀env x y.
-     exp_rel env x y ⇒
-       exp_rel env (Box x) (Box y)) ∧
 [exp_rel_Force:]
   (∀env x y.
      exp_rel env x y ⇒
@@ -105,14 +101,10 @@ Inductive exp_rel:
                  exp_rel (FILTER (λ(n,x). ¬MEM n (MAP FST f)) env) b c)
               (REVERSE f) g ⇒
        v_rel (Recclosure f n) (Recclosure g env n)) ∧
-[v_rel_Thunk_v:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w))) ∧
-[v_rel_Thunk_exp:]
+[v_rel_Thunk:]
   (∀env x y.
      exp_rel env x y ⇒
-       v_rel (Thunk (INR x)) (Thunk (INR (env, y)))) ∧
+       v_rel (Thunk x) (Thunk (INR (env, y)))) ∧
 [v_rel_Atom:]
   (∀l.
      v_rel (Atom l) (Atom l))
@@ -132,7 +124,6 @@ Theorem exp_rel_def =
     “exp_rel env (If x y z) w”,
     “exp_rel env (Letrec f x) y”,
     “exp_rel env (Delay x) y”,
-    “exp_rel env (Box x) y”,
     “exp_rel env (Force x) y” ]
   |> map (SIMP_CONV (srw_ss ()) [Once exp_rel_cases])
   |> LIST_CONJ;
@@ -148,9 +139,8 @@ Theorem v_rel_def =
     “v_rel z (Monadix env mop ys)”,
     “v_rel (Atom s) z”,
     “v_rel z (Atom s)”,
-    “v_rel (Thunk (INL s)) z”,
     “v_rel z (Thunk (INL s))”,
-    “v_rel (Thunk (INR s)) z”,
+    “v_rel (Thunk s) z”,
     “v_rel z (Thunk (INR (env, s)))” ]
   |> map (SIMP_CONV (srw_ss ()) [Once v_rel_cases])
   |> LIST_CONJ;
@@ -282,17 +272,15 @@ Proof
     \\ gvs [ELIM_UNCURRY, env_rel_def, LIST_REL_EL_EQN])
   >~ [‘Delay x’] >- (
     rw [subst_def, exp_rel_def])
-  >~ [‘Box x’] >- (
-    rw [subst_def, exp_rel_def])
   >~ [‘Force x’] >- (
     rw [subst_def, exp_rel_def])
   >~ [`Monad mop xs`]
   >- (rw[subst_def, exp_rel_def] >> gvs[LIST_REL_EL_EQN, EL_MAP])
 QED
 
-Theorem SUM_REL_def[local,simp] = quotient_sumTheory.SUM_REL_def;
+Theorem SUM_REL_THM[local,simp] = sumTheory.SUM_REL_THM;
 
-Theorem PAIR_REL_def[local,simp] = quotient_pairTheory.PAIR_REL;
+Theorem PAIR_REL_def[local,simp] = pairTheory.PAIR_REL;
 
 Theorem eval_to_exp_rel:
   ∀k x env y.
@@ -388,11 +376,6 @@ Proof
             v_rel_def])
   >~ [‘Delay x’] >- (
     gvs [exp_rel_def, eval_to_def, envLangTheory.eval_to_def, v_rel_def])
-  >~ [‘Box x’] >- (
-    gvs [exp_rel_def, eval_to_def, envLangTheory.eval_to_def, v_rel_def]
-    \\ first_x_assum (drule_all_then assume_tac)
-    \\ rename1 ‘exp_rel _ x y’
-    \\ Cases_on ‘eval_to k x’ \\ Cases_on ‘eval_to k env y’ \\ gs [v_rel_def])
   >~ [‘Force x’] >- (
     gvs [exp_rel_def]
     \\ rename1 ‘exp_rel _ x y’
@@ -424,7 +407,6 @@ Proof
       \\ gs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM]
       \\ gvs [env_rel_def, LIST_REL_EL_EQN, ELIM_UNCURRY, EL_MAP, EL_REVERSE,
               Abbr ‘xs’, v_rel_def])
-    \\ CASE_TAC \\ gvs [v_rel_def]
     \\ first_x_assum irule
     \\ simp [subst_funs_def])
   >~ [‘MkTick x’] >- (
diff --git a/compiler/backend/passes/proofs/thunk_unthunkProofScript.sml b/compiler/backend/passes/proofs/thunk_unthunkProofScript.sml
index 0d0d995f..1de0dd66 100644
--- a/compiler/backend/passes/proofs/thunk_unthunkProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_unthunkProofScript.sml
@@ -13,12 +13,11 @@ open pure_miscTheory thunkLangPropsTheory thunk_semanticsTheory
 val _ = new_theory "thunk_unthunkProof";
 
 val _ = set_grammar_ancestry ["finite_map", "pred_set", "rich_list",
-                              "thunkLang", "quotient_sum", "thunk_semantics",
-                              "thunkLangProps"];
+                              "thunkLang", "thunk_semantics", "thunkLangProps"];
 
 val _ = numLib.prefer_num ();
 
-Theorem SUM_REL_def[local,simp] = quotient_sumTheory.SUM_REL_def;
+Theorem SUM_REL_THM[local,simp] = sumTheory.SUM_REL_THM;
 
 (* --------------------------
    exp_inv:
@@ -107,7 +106,7 @@ Inductive exp_inv:
 [v_inv_Thunk:]
   (∀x.
      exp_inv x ⇒
-       v_inv (Thunk (INR x))) ∧
+       v_inv (Thunk x)) ∧
 [v_inv_DoTick:]
   (∀v.
      v_inv v ⇒
@@ -119,8 +118,6 @@ Theorem exp_inv_def:
      exp_inv (Var v) = T) ∧
   (∀v.
      exp_inv (Value v) = v_inv v) ∧
-  (∀x.
-     exp_inv (Box x) = F) ∧
   (∀f x.
      exp_inv (App f x) =
        (∃y. x = Delay y ∧
@@ -170,8 +167,7 @@ Theorem v_inv_def[simp]:
   (∀s x. v_inv (Closure s x) = exp_inv x) ∧
   (∀f n. v_inv (Recclosure f n) =
            EVERY (λv. ∃x. v = Delay x ∧ exp_inv x) (MAP SND f)) ∧
-  (∀v. v_inv (Thunk (INL v)) = F) ∧
-  (∀x. v_inv (Thunk (INR x)) = exp_inv x) ∧
+  (∀x. v_inv (Thunk x) = exp_inv x) ∧
   (∀v. v_inv (DoTick v) = v_inv v) ∧
   (∀x. v_inv (Atom x) = T)
 Proof
@@ -278,11 +274,11 @@ Inductive exp_rel:
   (∀x y.
      exp_rel x y ∧
      closed x ⇒
-       v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
+       v_rel (Thunk x) (Thunk y)) ∧
 [v_rel_Thunk_Changed:]
   (∀v w.
      v_rel v w ⇒
-       v_rel (Thunk (INR (Force (Value v)))) (DoTick w)) ∧
+       v_rel (Thunk (Force (Value v))) (DoTick w)) ∧
 [v_rel_Atom:]
   (∀x.
      v_rel (Atom x) (Atom x))
@@ -321,11 +317,11 @@ QED
 
 Theorem v_rel_Thunk_def:
   v_rel (Thunk x) z =
-    ((∃y w. z = Thunk (INR y) ∧
-            x = INR w ∧
+    ((∃y w. z = Thunk y ∧
+            x = w ∧
             exp_rel w y ∧
             closed w) ∨
-     (∃v y. x = INR (Force (Value v)) ∧
+     (∃v y. x = Force (Value v) ∧
             z = DoTick y ∧
             v_rel v y))
 Proof
@@ -348,7 +344,7 @@ QED
 Theorem v_rel_rev[simp]:
   (∀w.
      v_rel v (DoTick w) =
-       (∃x. v = Thunk (INR (Force (Value x))) ∧
+       (∃x. v = Thunk (Force (Value x)) ∧
             v_rel x w)) ∧
   (∀s y.
      v_rel v (Closure s y) =
@@ -376,8 +372,8 @@ Theorem v_rel_rev[simp]:
   (∀v s.
      v_rel v (Thunk s) =
       (∃x y.
-         v = Thunk (INR x) ∧
-         s = INR y ∧
+         v = Thunk x ∧
+         s = y ∧
          exp_rel x y ∧
          closed x)) ∧
   (∀v a.
@@ -547,8 +543,6 @@ Proof
           \\ rpt (pop_assum kall_tac)
           \\ qid_spec_tac ‘ws’ \\ Induct_on ‘vs’ \\ Cases_on ‘ws’ \\ simp [])
     \\ gvs [Abbr ‘R’, OPTREL_def, exp_rel_Delay_Force_Var, exp_rel_Value])
-  >- ((* Box *)
-    rw [Once exp_rel_cases])
   >- ((* Force *)
     rw [Once exp_rel_cases]
     \\ simp [subst_def]
@@ -737,8 +731,6 @@ Proof
   >- ((* Delay *)
     rw [Once exp_rel_cases]
     \\ rgs [eval_to_def, exp_inv_def, v_rel_Thunk_Same])
-  >- ((* Box *)
-    rw [Once exp_rel_cases])
   >- ((* Force *)
     rw [Once exp_rel_cases]
     \\ CONV_TAC (PATH_CONV "lr" (SIMP_CONV (srw_ss()) [Once eval_to_def]))
diff --git a/compiler/backend/passes/proofs/thunk_untickProofScript.sml b/compiler/backend/passes/proofs/thunk_untickProofScript.sml
index d071d2f0..5316602e 100644
--- a/compiler/backend/passes/proofs/thunk_untickProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_untickProofScript.sml
@@ -12,12 +12,11 @@ open pure_miscTheory thunkLangPropsTheory thunk_semanticsTheory;
 val _ = new_theory "thunk_untickProof";
 
 val _ = set_grammar_ancestry ["finite_map", "pred_set", "rich_list",
-                              "thunkLang", "quotient_sum", "quotient_pair",
-                              "thunkLangProps"];
+                              "thunkLang", "thunkLangProps"];
 
-Theorem SUM_REL_def[local,simp] = quotient_sumTheory.SUM_REL_def;
+Theorem SUM_REL_THM[local,simp] = sumTheory.SUM_REL_THM;
 
-Theorem PAIR_REL_THM[local,simp] = quotient_pairTheory.PAIR_REL_THM;
+Theorem PAIR_REL_THM[local,simp] = pairTheory.PAIR_REL_THM;
 
 val _ = numLib.prefer_num ();
 
@@ -70,10 +69,6 @@ Inductive exp_rel:
   (∀x y.
      exp_rel x y ⇒
        exp_rel (Delay x) (Delay y)) ∧
-[~Box:]
-  (∀x y.
-     exp_rel x y ⇒
-       exp_rel (Box x) (Box y)) ∧
 [~Force:]
   (∀x y.
      exp_rel x y ⇒
@@ -98,14 +93,10 @@ Inductive exp_rel:
   (∀f g n.
      LIST_REL (λ(f,x) (g,y). f = g ∧ ok_bind x ∧ exp_rel x y) f g ⇒
        v_rel (Recclosure f n) (Recclosure g n)) ∧
-[v_rel_Thunk_INR:]
+[v_rel_Thunk:]
   (∀x y.
      exp_rel x y ⇒
-       v_rel (Thunk (INR x)) (Thunk (INR y))) ∧
-[v_rel_Thunk_INL:]
-  (∀v w.
-     v_rel v w ⇒
-       v_rel (Thunk (INL v)) (Thunk (INL w))) ∧
+       v_rel (Thunk x) (Thunk y)) ∧
 [v_rel_Atom:]
   (∀x.
      v_rel (Atom x) (Atom x)) ∧
@@ -133,13 +124,9 @@ Theorem v_rel_def[simp]:
        ∃g. w = Recclosure g n ∧
            LIST_REL (λ(f,x) (g,y). f = g ∧ ok_bind x ∧ exp_rel x y) f g) ∧
   (∀x.
-     v_rel (Thunk (INR x)) w =
-       ∃y. w = Thunk (INR y) ∧
+     v_rel (Thunk x) w =
+       ∃y. w = Thunk y ∧
            exp_rel x y) ∧
-  (∀v w.
-     v_rel (Thunk (INL v)) w =
-       ∃u. w = Thunk (INL u) ∧
-       v_rel v u) ∧
   (∀x.
      v_rel (Atom x) w =
        (w = Atom x)) ∧
@@ -171,7 +158,6 @@ Theorem exp_rel_def =
    “exp_rel (Let s x y) z”,
    “exp_rel (If x y z) w”,
    “exp_rel (Delay x) y”,
-   “exp_rel (Box x) y”,
    “exp_rel (MkTick x) y”,
    “exp_rel (Force x) y”]
   |> map (SIMP_CONV (srw_ss()) [Once exp_rel_cases])
@@ -293,9 +279,6 @@ Proof
   >- ((* Delay *)
     rw [Once exp_rel_cases]
     \\ simp [subst_def, exp_rel_Delay])
-  >- ((* Box *)
-    rw [Once exp_rel_cases]
-    \\ simp [subst_def, exp_rel_Box])
   >- ((* Force *)
     rw [Once exp_rel_cases] \\ simp [subst_def]
     \\ irule exp_rel_Force \\ fs [])
@@ -355,26 +338,24 @@ Proof
   \\ CASE_TAC \\ gs []
 QED
 
+
 Theorem v_rel_dest_anyThunk:
   v_rel v w ∧
   dest_Tick v = NONE ⇒
-    ($= +++ ((v_rel +++ exp_rel) ###
+    ($= +++ (exp_rel ###
              LIST_REL (λ(f,x) (g,y). f = g ∧ ok_bind x ∧ exp_rel x y)))
       (dest_anyThunk v)
       (dest_anyThunk w)
 Proof
   Cases_on ‘v’ \\ Cases_on ‘w’ \\ rw [] \\ gvs [v_rel_def, dest_anyThunk_def]
-  >- (
-    rename1 ‘LIST_REL _ f g’
-    \\ ‘OPTREL (λx y. ok_bind x ∧ exp_rel x y)
-               (ALOOKUP (REVERSE f) s)
-               (ALOOKUP (REVERSE g) s)’
-      by (irule LIST_REL_OPTREL
-          \\ gs [ELIM_UNCURRY, LIST_REL_CONJ])
-    \\ gs [OPTREL_def]
-    \\ Cases_on ‘x’ \\ Cases_on ‘y’ \\ rgs [Once exp_rel_cases])
-  \\ rename1 ‘_ (Thunk s1) (Thunk s2)’
-  \\ Cases_on ‘s1’ \\ Cases_on ‘s2’ \\ gs []
+  \\ rename1 ‘LIST_REL _ f g’
+  \\ ‘OPTREL (λx y. ok_bind x ∧ exp_rel x y)
+      (ALOOKUP (REVERSE f) s)
+      (ALOOKUP (REVERSE g) s)’
+    by (irule LIST_REL_OPTREL
+        \\ gs [ELIM_UNCURRY, LIST_REL_CONJ])
+  \\ gs [OPTREL_def]
+  \\ Cases_on ‘x’ \\ Cases_on ‘y’ \\ rgs [Once exp_rel_cases]
 QED
 
 Theorem exp_rel_eval_to:
@@ -810,17 +791,6 @@ Proof
   >- ((* Delay *)
     rw [Once exp_rel_cases]
     \\ gs [eval_to_def])
-  >- ((* Box *)
-    rw [Once exp_rel_cases] \\ gs [eval_to_def]
-    \\ rename1 ‘exp_rel x y’
-    \\ ‘∀ck. eval_to ck x ≠ INL Type_error’
-      by (qx_gen_tac ‘ck’
-          \\ strip_tac
-          \\ first_x_assum (qspec_then ‘ck’ assume_tac)
-          \\ gs [])
-    \\ first_x_assum (drule_all_then (qx_choose_then ‘j1’ assume_tac))
-    \\ qexists_tac ‘j1’
-    \\ Cases_on ‘eval_to k y’ \\ Cases_on ‘eval_to (j1 + k) x’ \\ gs [])
   >- ((* Force *)
     rw [Once exp_rel_cases] \\ rename1 ‘exp_rel x y’
     \\ psimp "rar" [Once eval_to_def]
@@ -865,14 +835,8 @@ Proof
       \\ pairarg_tac \\ gvs []
       \\ rename1 ‘_ yy (wx,binds)’
       \\ PairCases_on ‘yy’ \\ gvs []
-      \\ Cases_on ‘wx’ \\ gs []
-      >- (
-        qexists_tac ‘j1’
-        \\ simp [Once eval_to_def]
-        \\ Cases_on ‘yy0’ \\ gs [])
-      \\ Cases_on ‘yy0’ \\ gs []
-      \\ rename1 ‘dest_anyThunk u1 = INR (INR y2, x2)’
-      \\ rename1 ‘dest_anyThunk u = INR (INR y1, x1)’
+      \\ rename1 ‘dest_anyThunk u1 = INR (y2, x2)’
+      \\ rename1 ‘dest_anyThunk u = INR (y1, x1)’
       \\ ‘exp_rel (subst_funs x1 y1) (subst_funs x2 y2) ∧
           ∀ck. eval_to ck (subst_funs x1 y1) ≠ INL Type_error’
         by (simp [subst_funs_def]
@@ -951,19 +915,8 @@ Proof
     \\ pairarg_tac \\ gvs []
     \\ rename1 ‘_ yy (wx,binds)’
     \\ PairCases_on ‘yy’ \\ gvs []
-    \\ Cases_on ‘wx’ \\ gs []
-    >- (
-      qmatch_asmsub_abbrev_tac ‘eval_to _ bod’
-      \\ ‘eval_to (j2 + k) bod ≠ INL Diverge’
-        by (strip_tac \\ gs [])
-      \\ drule_then (qspec_then ‘j1 + j2 + k’ assume_tac) eval_to_mono
-      \\ ‘eval_to (j1 + j2 + k + 1) x = eval_to (j1 + k) x’
-        by (irule eval_to_mono \\ gs [])
-      \\ qexists_tac ‘j1 + j2 + 1’
-      \\ simp [Once eval_to_def] \\ gs [])
-    \\ Cases_on ‘yy0’ \\ gs []
-    \\ rename1 ‘dest_anyThunk u1 = INR (INR y2, x2)’
-    \\ rename1 ‘dest_anyThunk u = INR (INR y1, x1)’
+    \\ rename1 ‘dest_anyThunk u1 = INR (y2, x2)’
+    \\ rename1 ‘dest_anyThunk u = INR (y1, x1)’
     \\ simp [Once eval_to_def]
     \\ Cases_on ‘eval_to (k - 1) (subst_funs x2 y2) = INL Diverge’ \\ gs []
     >- (
@@ -1459,8 +1412,6 @@ Proof
   rw [rel_ok_def]
   >- ((* ∀x. f x ≠ Err from rel_ok prevents this case *)
     simp [untick_apply_closure])
-  >- ((* Thunks go to Thunks or DoTicks *)
-    Cases_on ‘s’ \\ gs [])
   >- ((* Equal literals are related *)
     simp [exp_rel_Prim])
   >- ((* Equal 0-arity conses are related *)
diff --git a/compiler/backend/passes/thunk_let_forceScript.sml b/compiler/backend/passes/thunk_let_forceScript.sml
index 4b16a5e6..75800fbb 100644
--- a/compiler/backend/passes/thunk_let_forceScript.sml
+++ b/compiler/backend/passes/thunk_let_forceScript.sml
@@ -49,7 +49,6 @@ Definition let_force_def:
      | SOME v => case ALOOKUP m v of
                  | NONE => Force (let_force m x)
                  | SOME t => Var t) ∧
-  let_force m (Box x) = Box (let_force m x) ∧
   let_force m (Letrec fs x) =
     (let m1 = FILTER (can_keep_list (MAP FST fs)) m in
        Letrec (MAP (λ(n,x). (n,let_force m1 x)) fs) (let_force m1 x)) ∧
diff --git a/compiler/backend/passes/thunk_split_Delay_LamScript.sml b/compiler/backend/passes/thunk_split_Delay_LamScript.sml
index cd6ae907..c7166276 100644
--- a/compiler/backend/passes/thunk_split_Delay_LamScript.sml
+++ b/compiler/backend/passes/thunk_split_Delay_LamScript.sml
@@ -113,9 +113,6 @@ Definition split_Delayed_Lam_def:
     (split_Delayed_Lam (Delay e) var_creator maps =
         let (e', vc) = split_Delayed_Lam e var_creator maps in
         (Delay e', vc)) /\
-    (split_Delayed_Lam (Box e) var_creator maps =
-        let (e', vc) = split_Delayed_Lam e var_creator maps in
-        (Box e', vc)) /\
     (split_Delayed_Lam (Force e) var_creator maps =
         case dest_Var e of
             | SOME v =>
diff --git a/compiler/backend/passes/thunk_split_Forcing_LamScript.sml b/compiler/backend/passes/thunk_split_Forcing_LamScript.sml
index b4a7e718..90f17d03 100644
--- a/compiler/backend/passes/thunk_split_Forcing_LamScript.sml
+++ b/compiler/backend/passes/thunk_split_Forcing_LamScript.sml
@@ -45,7 +45,6 @@ Definition extract_names_def:
        | NONE => empty_vars
        | SOME (a,e) => (extract_names e) in
        insert_var (extract_names_rows s ys) n) ∧
-  extract_names (Box x) = extract_names x ∧
   extract_names (Delay x) = extract_names x ∧
   extract_names (Force x) = extract_names x ∧
   extract_names_list s [] = s ∧
@@ -139,9 +138,6 @@ Definition my_function_def:
   (my_function s (Delay e) =
      let (s, e) = my_function s e in
        (s, Delay e)) ∧
-  (my_function s (Box e) =
-     let (s, e) = my_function s e in
-       (s, Box e)) ∧
   (my_function_list s [] = (s, [])) ∧
   (my_function_list s (hd::tl) =
      let (s, hd) = my_function s hd in
diff --git a/compiler/backend/passes/thunk_to_envScript.sml b/compiler/backend/passes/thunk_to_envScript.sml
index cbd05c3c..dc3212aa 100644
--- a/compiler/backend/passes/thunk_to_envScript.sml
+++ b/compiler/backend/passes/thunk_to_envScript.sml
@@ -42,7 +42,6 @@ Definition to_env_def:
   to_env (App x xs) = Apps (to_env x) (MAP to_env xs) ∧
   to_env (Delay x) = Delay (to_env x) ∧
   to_env (Force x) = Force (to_env x) ∧
-  to_env (Box x) = Box (to_env x) ∧
   to_env (Letrec fs x) = Letrec (REVERSE (MAP (λ(n,x). (n,to_env x)) fs)) (to_env x) ∧
   to_env (Case v rows d) = Case v (MAP (λ(n,p,x). (n,p,to_env x)) rows)
                             (case d of NONE => NONE | SOME (a,e) => SOME (a,to_env e)) ∧
diff --git a/meta-theory/exp_eqSimps.sml b/meta-theory/exp_eqSimps.sml
index 3cc8f274..25459169 100644
--- a/meta-theory/exp_eqSimps.sml
+++ b/meta-theory/exp_eqSimps.sml
@@ -19,19 +19,19 @@ val impi = REWRITE_RULE [GSYM AND_IMP_INTRO]
 
 val PAIR_REL_REFL' = Q.prove(
   ‘(∀x. R1 x x) ∧ (∀y. R2 y y) ⇒ ∀p. (R1 ### R2) p p’,
-  rpt strip_tac >> Cases_on ‘p’ >> simp[quotient_pairTheory.PAIR_REL]);
+  rpt strip_tac >> Cases_on ‘p’ >> simp[pairTheory.PAIR_REL]);
 
 val PAIR_REL_TRANS' = Q.prove(
   ‘(∀x y z. R1 x y ∧ R1 y z ⇒ R1 x z) ∧ (∀a b c. R2 a b ∧ R2 b c ⇒ R2 a c) ⇒
    ∀p1 p2 p3. (R1 ### R2) p1 p2 ∧ (R1 ### R2) p2 p3 ⇒ (R1 ### R2) p1 p3’,
   rpt strip_tac >> map_every Cases_on [‘p1’, ‘p2’, ‘p3’] >>
-  gs[quotient_pairTheory.PAIR_REL] >> metis_tac[]);
+  gs[pairTheory.PAIR_REL] >> metis_tac[]);
 
 val PAIR_REL_SYM' = Q.prove(
   ‘(∀x y. R1 x y ⇒ R1 y x) ∧ (∀a b. R2 a b ⇒ R2 b a) ⇒
    ∀p1 p2. (R1 ### R2) p1 p2 ⇒ (R1 ### R2) p2 p1’,
   rpt strip_tac >> map_every Cases_on [‘p1’, ‘p2’] >>
-  gs[quotient_pairTheory.PAIR_REL]);
+  gs[pairTheory.PAIR_REL]);
 
 
 val EXPEQ_ss = let
@@ -74,7 +74,7 @@ val lrintro_cong = Q.prove(
 val lr_cons_cong = Q.prove(
   ‘k1 = k2 ⇒ x ≅ y ⇒ lrt xs ys ⇒ lrt ((k1,x)::xs) ((k2,y)::ys)’,
   rpt strip_tac >>
-  simp[listTheory.LIST_REL_CONS1, quotient_pairTheory.PAIR_REL]);
+  simp[listTheory.LIST_REL_CONS1, pairTheory.PAIR_REL]);
 
 val LREXPEQ_ss = let
   val rsd = {refl = lreq_refl, trans = lreq_trans,
diff --git a/typing/pure_typingPropsScript.sml b/typing/pure_typingPropsScript.sml
index 6f06e324..75801522 100644
--- a/typing/pure_typingPropsScript.sml
+++ b/typing/pure_typingPropsScript.sml
@@ -1635,7 +1635,7 @@ Inductive insert_seq:
   (insert_seq ce1 ce2 ∧
    LIST_REL (λ(cn1,pvs1,ce1) (cn2,pvs2,ce2).
     cn1 = cn2 ∧ pvs1 = pvs2 ∧ insert_seq ce1 ce2) css1 css2 ∧
-   OPTION_REL (λ(cn_ars1,ce1) (cn_ars2,ce2).
+   OPTREL (λ(cn_ars1,ce1) (cn_ars2,ce2).
     cn_ars1 = cn_ars2 ∧ insert_seq ce1 ce2) usopt1 usopt2
     ⇒ insert_seq (pure_cexp$Case d ce1 x css1 usopt1) (Case d' ce2 x css2 usopt2))
 End