diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
index 1d481b6cbb..81a9cbb518 100644
--- a/examples/lambda/barendregt/boehmScript.sml
+++ b/examples/lambda/barendregt/boehmScript.sml
@@ -2897,6 +2897,57 @@ Proof
       Q.EXISTS_TAC ‘q’ >> art [] ]
 QED
 
+Theorem subterm_width_inclusive :
+    !M p q. q <<= p /\ subterm_width M p <= d ==> subterm_width M q <= d
+Proof
+    rpt STRIP_TAC
+ >> Cases_on ‘p = []’ >- fs []
+ >> Cases_on ‘q = []’ >- rw []
+ >> Cases_on ‘p’ >> fs [subterm_width_def]
+ >> Cases_on ‘q’ >> fs [subterm_width_def]
+ >> T_TAC
+ >> Q.PAT_X_ASSUM ‘h' = h’ K_TAC
+ >> rename1 ‘t0 <<= t’
+ >> Q_TAC (TRANS_TAC LESS_EQ_TRANS)
+      ‘MAX_SET
+          (IMAGE (hnf_children_size o principle_hnf)
+             {subterm' (FV M) M q 0 |
+              q |
+              q <<= FRONT (h::t) /\ solvable (subterm' (FV M) M q 0)})’
+ >> POP_ASSUM (REWRITE_TAC o wrap)
+ >> MATCH_MP_TAC SUBSET_MAX_SET
+ >> CONJ_TAC
+ >- (MATCH_MP_TAC IMAGE_FINITE \\
+     MATCH_MP_TAC FINITE_SUBSET \\
+     Q.EXISTS_TAC ‘{subterm' (FV M) M q 0 | q | q <<= FRONT (h::t0)}’ \\
+     reverse CONJ_TAC
+     >- (rw [SUBSET_DEF] \\
+         Q.EXISTS_TAC ‘q’ >> art []) \\
+     Know ‘{subterm' (FV M) M q 0 | q <<= FRONT (h::t0)} =
+           IMAGE (\q. subterm' (FV M) M q 0) {q | q <<= FRONT (h::t0)}’
+     >- (rw [Once EXTENSION] >> EQ_TAC >> rw []) >> Rewr' \\
+     MATCH_MP_TAC IMAGE_FINITE \\
+     rw [FINITE_prefix])
+ >> CONJ_TAC
+ >- (MATCH_MP_TAC IMAGE_FINITE \\
+     MATCH_MP_TAC FINITE_SUBSET \\
+     Q.EXISTS_TAC ‘{subterm' (FV M) M q 0 | q | q <<= FRONT (h::t)}’ \\
+     reverse CONJ_TAC
+     >- (rw [SUBSET_DEF] \\
+         Q.EXISTS_TAC ‘q’ >> art []) \\
+     Know ‘{subterm' (FV M) M q 0 | q <<= FRONT (h::t)} =
+           IMAGE (\q. subterm' (FV M) M q 0) {q | q <<= FRONT (h::t)}’
+     >- (rw [Once EXTENSION] >> EQ_TAC >> rw []) >> Rewr' \\
+     MATCH_MP_TAC IMAGE_FINITE \\
+     rw [FINITE_prefix])
+ >> rw [SUBSET_DEF]
+ >> Q.EXISTS_TAC ‘subterm' (FV M) M q 0’ >> art []
+ >> Q.EXISTS_TAC ‘q’ >> art []
+ >> Q_TAC (TRANS_TAC isPREFIX_TRANS) ‘FRONT (h::t0)’ >> art []
+ >> MATCH_MP_TAC IS_PREFIX_FRONT_MONO
+ >> simp []
+QED
+
 (* NOTE: ‘p <> []’ is necessary for ‘FRONT p’ to be meaningful, and then
    subterm_valid_path_lemma makes sure that all involved ‘subterm X M q r’
    are meaningful (IS_SOME).
@@ -6919,9 +6970,10 @@ Proof
      >- (Q.X_GEN_TAC ‘i’ >> DISCH_TAC \\
          Q.PAT_X_ASSUM ‘!i q. i < k /\ q <<= p ==> subterm X (M i) q r <> NONE’
            (MP_TAC o Q.SPECL [‘i’, ‘q’]) >> simp [] \\
-         Cases_on ‘q’ >> fs [] \\
+         Q.PAT_X_ASSUM ‘!i. i < k ==> subterm_width (M i) p <= d’ drule \\
          Cases_on ‘p’ >> fs [] \\
-         Q.PAT_X_ASSUM ‘h = h'’ (fs o wrap o SYM) \\
+         Cases_on ‘q’ >> fs [] \\
+         Q.PAT_X_ASSUM ‘h' = h’ (fs o wrap) >> T_TAC \\
          simp [subterm_of_solvables] \\
          Know ‘principle_hnf (H i) = H i’
          >- (MATCH_MP_TAC principle_hnf_reduce \\
@@ -6931,7 +6983,8 @@ Proof
          >- (rw [Abbr ‘H’, LAMl_size_appstar, GSYM appstar_APPEND]) \\
          DISCH_TAC \\
          simp [] \\
-         NTAC 2 (POP_ASSUM K_TAC) >> T_TAC \\
+         NTAC 2 (POP_ASSUM K_TAC) \\
+         DISCH_TAC \\
          RNEWS_TAC (“ys' :string list”, “r :num”, “(n :num -> num) i”)
                     “X :string set” \\
          qabbrev_tac ‘vs' = TAKE (n i) vs’ \\
@@ -7084,7 +7137,7 @@ Proof
          DISCH_TAC \\
       (* applying subterm_fresh_tpm_cong *)
          DISCH_TAC (* subterm X (tpm pm N) t (SUC r) <> NONE *) \\
-         MP_TAC (Q.SPECL [‘pm’, ‘X’, ‘N’, ‘t’, ‘SUC r’] subterm_fresh_tpm_cong) \\
+         MP_TAC (Q.SPECL [‘pm’, ‘X’, ‘N’, ‘t'’, ‘SUC r’] subterm_fresh_tpm_cong) \\
          impl_tac >- simp [Abbr ‘pm’, MAP_ZIP] \\
          simp [] >> STRIP_TAC \\
          POP_ASSUM K_TAC (* already used *) \\
@@ -7106,12 +7159,13 @@ Proof
              simp [Abbr ‘ss’, Abbr ‘sub’] \\
              simp [MAP_REVERSE, MAP_GENLIST, o_DEF]) \\
       (* subterm_width N t <= d_max *)
-         Know ‘subterm_width (M i) (h::t) <= d’
-         >- cheat \\
+         Know ‘subterm_width (M i) (h::t') <= d’
+         >- (MATCH_MP_TAC subterm_width_inclusive \\
+             Q.EXISTS_TAC ‘h::t’ >> simp []) \\
          qabbrev_tac ‘Ms' = args i ++ DROP (n i) (MAP VAR vs)’ \\
       (* applying subterm_width_induction_lemma (the general one) *)
-         Suff ‘subterm_width (M i) (h::t) <= d <=>
-               m i <= d /\ subterm_width (EL h Ms') t <= d’
+         Suff ‘subterm_width (M i) (h::t') <= d <=>
+               m i <= d /\ subterm_width (EL h Ms') t' <= d’
          >- (Rewr' \\
              Know ‘EL h Ms' = N’
              >- (simp [Abbr ‘Ms'’, Abbr ‘N’] \\
@@ -7128,7 +7182,7 @@ Proof
              Q.EXISTS_TAC ‘M i’ >> art [] \\
              rw [Abbr ‘M’, EL_MEM]) \\
          MATCH_MP_TAC ltree_paths_inclusive \\
-         Q.EXISTS_TAC ‘h::t'’ >> simp []) >> DISCH_TAC \\
+         Q.EXISTS_TAC ‘h::t’ >> simp []) >> DISCH_TAC \\
   (* NOTE: ‘solvable (subterm' X (M i) q r)’ only holds when ‘q <<= FRONT p’.
      The case that ‘unsolvable (subterm' X (M j1/j2) q r)’ (p = q) must be
      treated specially. In this case, ltree_el (BT' X (M i) r q = SOME bot.
@@ -7234,10 +7288,22 @@ Proof
          Know ‘y i IN Z’ >- rw [] \\
          Suff ‘Z SUBSET X UNION RANK r’ >- METIS_TAC [SUBSET_DEF] \\
          FIRST_X_ASSUM ACCEPT_TAC) >> DISCH_TAC \\
-     Know ‘FV (tpm (REVERSE pm) N) SUBSET X UNION RANK r1 /\
+  (* some properties needed by the next "solvable" subgoal *)
+     Know ‘set vs SUBSET X UNION RANK r1’
+     >- (Suff ‘set vs SUBSET RANK r1’ >- SET_TAC [] \\
+         qunabbrev_tac ‘vs’ \\
+         MATCH_MP_TAC RNEWS_SUBSET_RANK >> simp [Abbr ‘r1’]) >> DISCH_TAC \\
+     Know ‘set ys SUBSET X UNION RANK r1’
+     >- (Suff ‘set ys SUBSET RANK r1’ >- SET_TAC [] \\
+         qunabbrev_tac ‘ys’ \\
+         MATCH_MP_TAC RNEWS_SUBSET_RANK >> simp [Abbr ‘r1’] \\
+         rw [LENGTH_NON_NIL]) >> DISCH_TAC \\
+     Know ‘FV (tpm (REVERSE pm) N)  SUBSET X UNION RANK r1 /\
            FV (tpm (REVERSE pm) N') SUBSET X UNION RANK r1’
-     >- (
-         cheat) >> STRIP_TAC \\
+     >- (CONJ_TAC \\
+         MATCH_MP_TAC FV_tpm_lemma \\
+         Q.EXISTS_TAC ‘r1’ >> simp [Abbr ‘pm’, MAP_REVERSE, MAP_ZIP]) \\
+     STRIP_TAC \\
      Know ‘hnf_children_size N0 <= d_max /\ hnf_children_size N0' <= d_max’
      >- (
          cheat) >> STRIP_TAC \\