diff --git a/compiler/backend/passes/proofs/pure_to_thunkProofScript.sml b/compiler/backend/passes/proofs/pure_to_thunkProofScript.sml
index 761b1802..be1c749d 100644
--- a/compiler/backend/passes/proofs/pure_to_thunkProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_to_thunkProofScript.sml
@@ -99,21 +99,47 @@ Proof
   Induct \\ fs [PULL_EXISTS,MAP_EQ_CONS]
 QED
 
+Theorem mk_delay_rel_conj:
+  mk_delay_rel (λx y. P x y ∧ Q x y) x y
+  ⇒ mk_delay_rel P x y ∧ mk_delay_rel Q x y
+Proof
+  Induct_on `mk_delay_rel` >> rw[] >> simp[Once mk_delay_rel_cases]
+QED
+
 Theorem IMP_mk_delay_eq_Delay:
-  exp_rel x1 y1 ∧ (∀c v. x1 = Var c v ⇒ mk_delay flag y1 ≠ Var v) ⇒
-  ∃x2. exp_rel x1 x2 ∧ mk_delay flag y1 = Delay x2
+  exp_rel x1 y1 ⇒ mk_delay_rel exp_rel x1 (mk_delay flag y1)
 Proof
-  Cases_on ‘∃c m. x1 = Var c m’ \\ gvs []
+  Induct_on `exp_rel` >> reverse $ rw[]
+  >- simp[Once mk_delay_rel_cases] >>
+  simp[Once mk_delay_rel_cases, mk_delay_def] >>
+  simp[Once exp_rel_cases] >> gvs[AllCaseEqs()]
   >- (
-    simp [Once exp_rel_cases] \\ rw [] \\ fs [mk_delay_def, AllCaseEqs()] >>
-    simp[Once exp_rel_cases]
+    rpt conj_tac
+    >- (
+      qpat_x_assum `LIST_REL _ _ _` mp_tac >>
+      match_mp_tac LIST_REL_mono >> rw[] >> rpt (pairarg_tac >> gvs[])
+      )
+    >- (
+      qpat_x_assum `mk_delay_rel _ _ _` mp_tac >>
+      rpt $ pop_assum kall_tac >>
+      Induct_on `mk_delay_rel` >> rw[] >> simp[Once mk_delay_rel_cases]
+      )
+    >- (
+      Cases_on `eopt` >> Cases_on `yopt` >> gvs[] >>
+      rpt (pairarg_tac >> gvs[])
+      )
+    )
+  >>~- (
+    [`LIST_REL`],
+    qpat_x_assum `LIST_REL _ _ _` mp_tac >> match_mp_tac LIST_REL_mono >>
+    rw[] >> rpt (pairarg_tac >> gvs[]) >>
+    qpat_x_assum `mk_delay_rel _ _ _` mp_tac >>
+    rpt $ pop_assum kall_tac >>
+    Induct_on `mk_delay_rel` >> rw[] >> simp[Once mk_delay_rel_cases]
     ) >>
-  Cases_on ‘x1’ \\ gvs []
-  \\ strip_tac
-  \\ first_assum $ irule_at $ Pos hd
-  \\ pop_assum mp_tac
-  \\ rw[Once exp_rel_cases]
-  \\ gvs [mk_delay_def]
+  qpat_x_assum `mk_delay_rel (λa b. _)  _ _` mp_tac >>
+  rpt $ pop_assum kall_tac >>
+  Induct_on `mk_delay_rel` >> rw[] >> simp[Once mk_delay_rel_cases]
 QED
 
 Theorem cns_arities_mk_delay:
@@ -162,14 +188,6 @@ Proof
   \\ Cases_on ‘c’ \\ gvs []
 QED
 
-Theorem to_thunk_eq_Force_Var:
-  to_thunk b s h = (Force (Var n),s') ∧ NestedCase_free h ⇒ ∃a. h = Var a n
-Proof
-  Cases_on ‘h’ \\ gvs [to_thunk_def]
-  \\ rpt (pairarg_tac \\ gvs [AllCaseEqs()] \\ rw [])
-  \\ gvs [monad_to_thunk_def |> DefnBase.one_line_ify NONE, AllCaseEqs()]
-QED
-
 Theorem exp_rel_to_thunk:
   (∀flag s (x:'a pure_cexp$cexp) x1 s1.
     to_thunk flag s x = (x1,s1) ∧ NestedCase_free x ∧ vars_ok s ∧
@@ -304,7 +322,7 @@ Proof
     >-
      (conj_tac
       >- (irule exp_rel_Case \\ fs []
-          \\ conj_tac >- (strip_tac \\ irule IMP_mk_delay_eq_Delay \\ fs [])
+          \\ reverse conj_tac >- (irule IMP_mk_delay_eq_Delay \\ fs [])
           \\ qpat_x_assum ‘LIST_REL exp_rel _ _’ mp_tac
           \\ rpt $ qpat_x_assum ‘EVERY _ _’ mp_tac
           \\ qid_spec_tac ‘ys’
@@ -409,8 +427,8 @@ Proof
     \\ strip_tac \\ fs []
     \\ conj_tac
     >- (irule exp_rel_Case \\ fs []
-        \\ once_rewrite_tac [CONJ_COMM] \\ rewrite_tac [GSYM CONJ_ASSOC]
-        \\ conj_tac >- (strip_tac \\ irule IMP_mk_delay_eq_Delay \\ fs [])
+        \\ rewrite_tac [CONJ_ASSOC]
+        \\ reverse conj_tac >- (irule IMP_mk_delay_eq_Delay \\ fs [])
         \\ qpat_x_assum ‘LIST_REL exp_rel _ _’ mp_tac
         \\ rpt $ qpat_x_assum ‘EVERY _ _’ mp_tac
         \\ qid_spec_tac ‘ys’
@@ -581,13 +599,7 @@ Proof
       \\ simp [delay_arg_def,EVAL “LUPDATE x 1 [y1;y2]”,EVAL “LUPDATE x 2 [y1;y2;y3]”,
                any_el_def, boundvars_exp_of_mk_delay]
       \\ simp [IMP_mk_delay_eq_Delay,cexp_wf_mk_delay,cns_arities_mk_delay]
-      \\ simp [PULL_EXISTS,SF DNF_ss]
-      \\ gvs [to_thunk_def]
-      \\ rpt (pairarg_tac \\ gvs [])
-      \\ rename [‘mk_delay flag y3’]
-      \\ Cases_on ‘mk_delay flag y3 = Delay y3’
-      \\ gvs [mk_delay_not_Delay]
-      \\ imp_res_tac to_thunk_eq_Force_Var \\ gvs [mk_delay_def])
+      \\ simp [PULL_EXISTS,SF DNF_ss])
     >~ [‘AtomOp a’] >-
      (gvs [] \\ irule_at Any exp_rel_Prim \\ gvs []
       \\ qpat_x_assum ‘_ ⇒ _’ mp_tac \\ impl_tac
@@ -632,6 +644,10 @@ Proof
     \\ simp [thunk_cexpTheory.cns_arities_def]
     \\ rw []
     \\ metis_tac [])
+  >~ [`Annot`]
+  >- (
+    simp[Once exp_rel_cases]
+    )
   \\ qpat_x_assum ‘_ ⇒ _’ mp_tac \\ impl_tac
   >- fs [EVERY_MEM,SUBSET_DEF,PULL_EXISTS,MEM_MAP,PULL_FORALL,SF SFY_ss]
   \\ strip_tac \\ fs [] \\ fs [SUBSET_DEF]
diff --git a/compiler/backend/passes/proofs/pure_to_thunk_2ProofScript.sml b/compiler/backend/passes/proofs/pure_to_thunk_2ProofScript.sml
index ec874708..2c24e98a 100644
--- a/compiler/backend/passes/proofs/pure_to_thunk_2ProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_to_thunk_2ProofScript.sml
@@ -25,6 +25,22 @@ val _ = set_grammar_ancestry
 Overload mk_delay_rel = ``λf x y. (∃c v. x = Var c v ∧ y = Var v) ∨
                                   (∃z. f x z ∧ y = Delay z)``
 
+Inductive mk_delay_rel:
+  mk_delay_rel f (Var c v) (Var v) ∧
+
+  (f x z ∧ y = Delay z ⇒ mk_delay_rel f x y) ∧
+
+  (mk_delay_rel f x y ⇒ mk_delay_rel f (Annot c annot x) y)
+End
+
+Theorem mk_delay_rel_mono[mono]:
+  (∀x y. f x y ⇒ g x y) ⇒
+  mk_delay_rel f x y ⇒ mk_delay_rel g x y
+Proof
+  Induct_on `mk_delay_rel` >> rw[] >>
+  simp[Once mk_delay_rel_cases]
+QED
+
 Inductive exp_rel:
 [~Var:]
   (∀(n:mlstring).
@@ -36,8 +52,7 @@ Inductive exp_rel:
        exp_rel (pure_cexp$Lam i s x) (Lam s y))
 [~Let:]
   (∀s x y z1 y1.
-     (~(∃c v. x = Var c v ∧ z1 = Var v) ⇒
-      (∃x1. exp_rel x x1 ∧ z1 = Delay x1)) ∧
+     mk_delay_rel exp_rel x z1 ∧
      exp_rel y y1 ⇒
        exp_rel (Let i s x y) (Let (SOME s) z1 y1))
 [~Letrec:]
@@ -48,20 +63,17 @@ Inductive exp_rel:
 [~App:]
   (∀f g xs ys.
      exp_rel f g ∧
-     LIST_REL (λx z1. ~(∃c v. x = Var c v ∧ z1 = Var v) ⇒
-                      (∃x1. exp_rel x x1 ∧ z1 = Delay x1)) xs ys ⇒
+     LIST_REL (mk_delay_rel exp_rel) xs ys ⇒
        exp_rel (App i f xs) (App g ys))
 [~Cons:]
   (∀xs ys n.
-     LIST_REL (λx z1. ~(∃c v. x = Var c v ∧ z1 = Var v) ⇒
-                      (∃x1. exp_rel x x1 ∧ z1 = Delay x1)) xs ys ∧
+     LIST_REL (mk_delay_rel exp_rel) xs ys ∧
      explode n ∉ monad_cns ⇒
        exp_rel (Prim i (Cons n) xs) (Prim (Cons n) ys))
 [~Ret_Raise:]
   (∀mop xs ys n.
      (if n = «Ret» then mop = Ret else n = «Raise» ∧ mop = Raise) ∧
-     LIST_REL (λx z1. ~(∃c v. x = Var c v ∧ z1 = Var v) ⇒
-                      (∃x1. exp_rel x x1 ∧ z1 = Delay x1)) xs ys ⇒
+     LIST_REL (mk_delay_rel exp_rel) xs ys ⇒
        exp_rel (Prim i (Cons n) xs) (Monad mop ys))
 [~Bind_Handle:]
   (∀mop xs ys n.
@@ -110,14 +122,15 @@ Inductive exp_rel:
        x1 = y1 ∧ x2 = y2 ∧ ~MEM fresh x2 ∧
        exp_rel x3 y3 ∧ explode fresh ∉ freevars (exp_of' x3)) xs ys ∧
      (∀a x. eopt = SOME (a,x) ⇒ explode fresh ∉ freevars (exp_of' x)) ∧
-     (~(∃c z. x = Var c z ∧ a_exp = Var z) ⇒
-      (∃x1. exp_rel x x1 ∧ a_exp = Delay x1)) ∧
+     mk_delay_rel exp_rel x a_exp ∧
      fresh ≠ v ∧
      OPTREL (λ(a,x) (b,y). a = b ∧ exp_rel x y) eopt yopt ⇒
        exp_rel (Case i x v xs eopt)
                (Let (SOME v) a_exp $
                 Let (SOME fresh) (Force (Var v)) $
                   Case fresh ys yopt))
+[~Annot:]
+  (exp_rel ce ce' ⇒ exp_rel (Annot d annot ce) ce')
 End
 
 Overload to_thunk = “pure_to_thunk_1Proof$compile_rel”
@@ -311,13 +324,14 @@ Proof
           lift_rel q1 q2 ∧
           force_rel NONE q2 q3 ∧
           proj_rel q3 q4 ∧
-          delay_force (Delay q4) (exp_of a_exp)’ by
-      (qpat_x_assum ‘(∀c z. x = Var c z ⇒ a_exp ≠ Var z) ⇒ _’ mp_tac
-       \\ disch_then (assume_tac o ONCE_REWRITE_RULE [IMP_DISJ_THM])
-       \\ reverse $ gvs []
-       >- metis_tac [delay_force_Delay]
-       \\ fs [exp_of'_def]
-       \\irule_at Any pure_to_thunk_1ProofTheory.compile_rel_Var
+          delay_force (Delay q4) (exp_of a_exp)’ by (
+        qpat_x_assum ‘mk_delay_rel _ _ _’ mp_tac >>
+        qpat_x_assum `cexp_wf _` mp_tac >>
+        rpt $ pop_assum kall_tac >>
+        Induct_on `mk_delay_rel` >> reverse $ rw[] >> gvs[exp_of'_def, cexp_wf_def]
+        >- metis_tac[]
+        >- metis_tac [delay_force_Delay]
+       \\ irule_at Any pure_to_thunk_1ProofTheory.compile_rel_Var
        \\ irule_at Any thunk_case_liftProofTheory.compile_rel_Force
        \\ irule_at Any thunk_let_forceProofTheory.exp_rel_Force
        \\ irule_at Any thunk_case_projProofTheory.compile_rel_Force
@@ -329,7 +343,7 @@ Proof
     \\ qpat_x_assum ‘lift_rel _ _’ $ irule_at Any
     \\ qpat_x_assum ‘force_rel NONE _ _’ $ irule_at Any
     \\ qpat_x_assum ‘proj_rel _ _’ $ irule_at Any \\ fs []
-    \\ qpat_x_assum ‘(∀c z. x = Var c z ⇒ a_exp ≠ Var z) ⇒ _’ kall_tac
+    \\ qpat_x_assum ‘mk_delay_rel _ _ _’ kall_tac
     \\ Cases_on ‘xs’ \\ fs []
     \\ PairCases_on ‘h’ \\ fs []
     \\ rename [‘_ = yy :: _’]
@@ -464,18 +478,19 @@ Proof
     \\ irule_at Any thunk_case_liftProofTheory.compile_rel_Delay
     \\ irule_at Any thunk_let_forceProofTheory.exp_rel_Delay
     \\ irule_at Any thunk_case_projProofTheory.compile_rel_Delay
-    \\ gvs [IMP_DISJ_THM,exp_of'_def]
-    >-
-     (irule_at Any pure_to_thunk_1ProofTheory.compile_rel_Var
-      \\ irule_at Any thunk_case_liftProofTheory.compile_rel_Force
-      \\ irule_at Any thunk_let_forceProofTheory.exp_rel_Force
-      \\ irule_at Any thunk_case_projProofTheory.compile_rel_Force
-      \\ irule_at Any thunk_case_liftProofTheory.compile_rel_Var
-      \\ irule_at Any thunk_let_forceProofTheory.exp_rel_Var
-      \\ irule_at Any thunk_case_projProofTheory.compile_rel_Var
-      \\ irule_at Any thunk_unthunkProofTheory.delay_force_Delat_Force_Var
-      \\ metis_tac [])
-    \\ irule_at Any thunk_unthunkProofTheory.delay_force_Delay
+    \\ qpat_x_assum `mk_delay_rel _ _ _` mp_tac
+    \\ qpat_x_assum `cexp_wf x` mp_tac
+    \\ Induct_on `mk_delay_rel` >> reverse $ rw[] >> gvs[cexp_wf_def, exp_of'_def]
+    >- metis_tac[]
+    >- metis_tac [delay_force_Delay]
+    \\ irule_at Any pure_to_thunk_1ProofTheory.compile_rel_Var
+    \\ irule_at Any thunk_case_liftProofTheory.compile_rel_Force
+    \\ irule_at Any thunk_let_forceProofTheory.exp_rel_Force
+    \\ irule_at Any thunk_case_projProofTheory.compile_rel_Force
+    \\ irule_at Any thunk_case_liftProofTheory.compile_rel_Var
+    \\ irule_at Any thunk_let_forceProofTheory.exp_rel_Var
+    \\ irule_at Any thunk_case_projProofTheory.compile_rel_Var
+    \\ irule_at Any thunk_unthunkProofTheory.delay_force_Delat_Force_Var
     \\ metis_tac [])
   >~ [‘Cons _ _’] >-
    (irule_at Any pure_to_thunk_1ProofTheory.compile_rel_Cons
@@ -497,9 +512,11 @@ Proof
     \\ last_x_assum drule \\ strip_tac
     \\ rpt $ first_assum $ irule_at Any
     \\ rpt $ qpat_x_assum ‘LIST_REL _ _ _’ kall_tac
-    \\ qpat_x_assum ‘(∀c z. h = Var c z ⇒ h5 ≠ Var z) ⇒ _’ mp_tac
-    \\ disch_then (assume_tac o ONCE_REWRITE_RULE [IMP_DISJ_THM])
-    \\ reverse $ gvs []
+    \\ qpat_x_assum `mk_delay_rel _ _ _` mp_tac
+    \\ qpat_x_assum `cexp_wf _` mp_tac
+    \\ rpt $ pop_assum kall_tac
+    \\ Induct_on `mk_delay_rel` \\ reverse $ rw[] \\ gvs[cexp_wf_def, exp_of'_def]
+    >- metis_tac[]
     >-
      (qpat_x_assum ‘to_thunk (exp_of' _) _’ $ irule_at Any
       \\ irule_at Any thunk_case_liftProofTheory.compile_rel_Delay
@@ -542,7 +559,8 @@ Proof
     \\ qpat_x_assum ‘exp_rel x x5’ assume_tac
     \\ drule exp_rel_App
     \\ disch_then $ qspecl_then [‘ARB’,‘[h]’,‘[h5]’] mp_tac
-    \\ impl_tac >- (fs [] \\ strip_tac \\ gvs [SF SFY_ss])
+    \\ impl_tac
+    >- (gvs[] >> irule mk_delay_rel_mono >> goal_assum $ drule_at Any >> simp[])
     \\ strip_tac
     \\ first_x_assum $ drule
     \\ fs [GSYM PULL_EXISTS]
@@ -557,9 +575,10 @@ Proof
     \\ irule_at Any thunk_case_projProofTheory.compile_rel_App
     \\ irule_at Any thunk_unthunkProofTheory.delay_force_App
     \\ qpat_x_assum ‘LIST_REL _ _ _’ kall_tac
-    \\ qpat_x_assum ‘(∀c z. h = Var c z ⇒ h5 ≠ Var z) ⇒ _’ mp_tac
-    \\ disch_then (assume_tac o ONCE_REWRITE_RULE [IMP_DISJ_THM])
-    \\ reverse $ gvs []
+    \\ qpat_x_assum `mk_delay_rel _ _ _` mp_tac
+    \\ qpat_x_assum `cexp_wf h` mp_tac
+    \\ Induct_on `mk_delay_rel` \\ reverse $ rw[] \\ gvs[cexp_wf_def, exp_of'_def]
+    >- metis_tac[]
     >-
      (qpat_x_assum ‘to_thunk (exp_of' _) _’ $ irule_at Any
       \\ qpat_x_assum ‘lift_rel y1 _’ $ irule_at Any
@@ -651,24 +670,32 @@ Proof
   >~ [`Ret`]
   >- (
     simp[lift_cases, force_cases, proj_cases, delay_force_cases, PULL_EXISTS] >>
-    last_x_assum $ mp_tac o ONCE_REWRITE_RULE [IMP_DISJ_THM] >> rw[] >> gvs[]
+    rpt $ pop_assum mp_tac >> Induct_on `mk_delay_rel` >> reverse $ rw[] >>
+    gvs[cexp_wf_def, exp_of'_def]
+    >- metis_tac[]
+    >- (
+      simp[lift_cases, force_cases, proj_cases, delay_force_cases, PULL_EXISTS] >>
+      rpt $ goal_assum drule
+      )
     >- (
       simp[exp_of'_def, to_thunk_cases, PULL_EXISTS] >>
       ntac 3 $ simp[lift_cases, force_cases, proj_cases, delay_force_cases, PULL_EXISTS]
-      ) >>
-    simp[lift_cases, force_cases, proj_cases, delay_force_cases, PULL_EXISTS] >>
-    rpt $ goal_assum drule
+      )
     )
   >~ [`Raise`]
   >- (
     simp[lift_cases, force_cases, proj_cases, delay_force_cases, PULL_EXISTS] >>
-    last_x_assum $ mp_tac o ONCE_REWRITE_RULE [IMP_DISJ_THM] >> rw[] >> gvs[]
+    rpt $ pop_assum mp_tac >> Induct_on `mk_delay_rel` >> reverse $ rw[] >>
+    gvs[cexp_wf_def, exp_of'_def]
+    >- metis_tac[]
+    >- (
+      simp[lift_cases, force_cases, proj_cases, delay_force_cases, PULL_EXISTS] >>
+      rpt $ goal_assum drule
+      )
     >- (
       simp[exp_of'_def, to_thunk_cases, PULL_EXISTS] >>
       ntac 3 $ simp[lift_cases, force_cases, proj_cases, delay_force_cases, PULL_EXISTS]
-      ) >>
-    simp[lift_cases, force_cases, proj_cases, delay_force_cases, PULL_EXISTS] >>
-    rpt $ goal_assum drule
+      )
     )
   >~ [`Bind`]
   >- (
@@ -702,29 +729,38 @@ Proof
     ntac 4 $ simp[proj_cases, PULL_EXISTS] >>
     ntac 5 $ simp[delay_force_cases]
     )
-  >~ [`Alloc`] (* Delay (Force (Var _)) case *)
-  >- (
-    simp[lift_cases, force_cases, proj_cases, delay_force_cases, PULL_EXISTS] >>
-    goal_assum drule >> simp[exp_of'_def, to_thunk_cases, PULL_EXISTS] >>
-    simp[LUPDATE_DEF] >> simp[lift_cases, PULL_EXISTS] >> goal_assum drule >>
-    ntac 7 $ simp[lift_cases, PULL_EXISTS] >> simp[force_cases, PULL_EXISTS] >>
-    goal_assum drule >> ntac 7 $ simp[force_cases, PULL_EXISTS] >>
-    simp[proj_cases, PULL_EXISTS] >> goal_assum drule >>
-    ntac 7 $ simp[proj_cases, PULL_EXISTS] >> ntac 6 $ simp[delay_force_cases]
-    )
   >~ [`Alloc`]
   >- (
-    simp[LUPDATE_DEF] >>
-    ntac 2 $ simp[lift_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
-    simp[lift_cases, PULL_EXISTS] >> goal_assum drule >>
-    ntac 7 $ simp[lift_cases, PULL_EXISTS] >>
-    ntac 2 $ simp[force_cases, PULL_EXISTS] >> goal_assum drule >>
-    simp[force_cases, PULL_EXISTS] >> goal_assum drule >>
-    ntac 7 $ simp[force_cases, PULL_EXISTS] >>
-    ntac 2 $ simp[proj_cases, PULL_EXISTS] >> goal_assum drule >>
-    simp[proj_cases, PULL_EXISTS] >> goal_assum drule >>
-    ntac 7 $ simp[proj_cases, PULL_EXISTS] >>
-    ntac 7 $ simp[delay_force_cases, PULL_EXISTS]
+    simp[lift_cases, force_cases, proj_cases, delay_force_cases, PULL_EXISTS] >>
+    goal_assum dxrule >>
+    rpt $ pop_assum mp_tac >>
+    Induct_on `mk_delay_rel` >> reverse $ rw[] >> gvs[exp_of'_def, cexp_wf_def]
+    >- metis_tac[]
+    >- (
+      goal_assum drule >>
+      simp[to_thunk_cases, PULL_EXISTS] >>
+      simp[LUPDATE_DEF] >> simp[lift_cases, PULL_EXISTS] >> goal_assum drule >>
+      simp[lift_cases, PULL_EXISTS] >> goal_assum drule >>
+      ntac 5 $ simp[lift_cases, PULL_EXISTS] >>
+      simp[force_cases, PULL_EXISTS] >> goal_assum drule >>
+      simp[force_cases, PULL_EXISTS] >> goal_assum drule >>
+      ntac 4 $ simp[force_cases, PULL_EXISTS] >>
+      simp[proj_cases, PULL_EXISTS] >> goal_assum drule >>
+      simp[proj_cases, PULL_EXISTS] >> goal_assum drule >>
+      ntac 4 $ simp[proj_cases, PULL_EXISTS] >>
+      ntac 6 $ simp[delay_force_cases]
+      )
+    >- (
+      simp[LUPDATE_DEF] >>
+      simp[to_thunk_cases, PULL_EXISTS] >>
+      simp[lift_cases, PULL_EXISTS] >> goal_assum drule >>
+      ntac 7 $ simp[lift_cases, PULL_EXISTS] >>
+      simp[force_cases, PULL_EXISTS] >> goal_assum drule >>
+      ntac 7 $ simp[force_cases, PULL_EXISTS] >>
+      simp[proj_cases, PULL_EXISTS] >> goal_assum drule >>
+      ntac 7 $ simp[proj_cases, PULL_EXISTS] >>
+      ntac 7 $ simp[delay_force_cases, PULL_EXISTS]
+      )
     )
   >~ [`Deref`]
   >- (
@@ -737,31 +773,36 @@ Proof
     ntac 2 $ simp[delay_force_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
     ntac 4 $ simp[delay_force_cases, PULL_EXISTS]
     )
-  >~ [`Update`] (* Delay (Force (Var _)) case *)
-  >- (
-    simp[LUPDATE_DEF, exp_of'_def] >> rpt $ goal_assum drule >>
-    simp[to_thunk_cases, PULL_EXISTS] >>
-    ntac 3 $ simp[lift_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
-    ntac 11 $ simp[lift_cases, PULL_EXISTS] >>
-    ntac 3 $ simp[force_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
-    ntac 11 $ simp[force_cases, PULL_EXISTS] >>
-    ntac 3 $ simp[proj_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
-    ntac 11 $ simp[proj_cases, PULL_EXISTS] >>
-    ntac 12 $ simp[Once delay_force_cases]
-    )
   >~ [`Update`]
   >- (
-    simp[LUPDATE_DEF, exp_of'_def] >> rpt $ goal_assum drule >>
-    ntac 3 $ simp[lift_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
-    simp[lift_cases, PULL_EXISTS] >> goal_assum drule >>
-    ntac 11 $ simp[lift_cases, PULL_EXISTS] >>
-    ntac 3 $ simp[force_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
-    simp[force_cases, PULL_EXISTS] >> goal_assum drule >>
-    ntac 11 $ simp[force_cases, PULL_EXISTS] >>
-    ntac 3 $ simp[proj_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
-    simp[proj_cases, PULL_EXISTS] >> goal_assum drule >>
-    ntac 11 $ simp[proj_cases, PULL_EXISTS] >>
-    ntac 12 $ simp[Once delay_force_cases]
+    simp[lift_cases, force_cases, proj_cases, delay_force_cases, PULL_EXISTS] >>
+    rpt $ goal_assum dxrule >>
+    rpt $ pop_assum mp_tac >>
+    Induct_on `mk_delay_rel` >> reverse $ rw[] >> gvs[exp_of'_def, cexp_wf_def]
+    >- metis_tac[]
+    >- (
+      simp[LUPDATE_DEF] >> rpt $ goal_assum drule >>
+      ntac 2 $ simp[lift_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
+      simp[lift_cases, PULL_EXISTS] >> goal_assum drule >>
+      ntac 8 $ simp[lift_cases, PULL_EXISTS] >>
+      ntac 2 $ simp[force_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
+      simp[force_cases, PULL_EXISTS] >> goal_assum drule >>
+      ntac 8 $ simp[force_cases, PULL_EXISTS] >>
+      ntac 2 $ simp[proj_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
+      simp[proj_cases, PULL_EXISTS] >> goal_assum drule >>
+      ntac 8 $ simp[proj_cases, PULL_EXISTS] >>
+      ntac 12 $ simp[Once delay_force_cases]
+      )
+    >- (
+      simp[LUPDATE_DEF] >> simp[to_thunk_cases] >>
+      ntac 2 $ simp[lift_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
+      ntac 11 $ simp[lift_cases, PULL_EXISTS] >>
+      ntac 2 $ simp[force_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
+      ntac 11 $ simp[force_cases, PULL_EXISTS] >>
+      ntac 2 $ simp[proj_cases, PULL_EXISTS] >> rpt $ goal_assum drule >>
+      ntac 11 $ simp[proj_cases, PULL_EXISTS] >>
+      ntac 12 $ simp[Once delay_force_cases]
+      )
     )
 QED