diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
new file mode 100644
index 0000000000..669ac44d33
--- /dev/null
+++ b/examples/lambda/barendregt/boehmScript.sml
@@ -0,0 +1,834 @@
+(*---------------------------------------------------------------------------*
+ * boehmScript.sml: (Effective) Boehm Trees (Chapter 10 of [1])              *
+ *---------------------------------------------------------------------------*)
+
+open HolKernel boolLib Parse bossLib;
+
+(* core theories *)
+open optionTheory arithmeticTheory pred_setTheory listTheory rich_listTheory
+     llistTheory relationTheory ltreeTheory pathTheory posetTheory hurdUtils;
+
+open binderLib nomsetTheory termTheory appFOLDLTheory chap2Theory chap3Theory
+     head_reductionTheory standardisationTheory solvableTheory reductionEval;
+
+val _ = new_theory "boehm";
+
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"];
+
+val o_DEF = combinTheory.o_DEF;
+
+(*---------------------------------------------------------------------------*
+ *  Equivalent terms
+ *---------------------------------------------------------------------------*)
+
+(* Definition 10.2.19 [1, p. 238]
+
+   M = LAMl v1 (y  @* Ms) @@ (MAP VAR v1) == y  @* Ms'
+   N = LAMl v2 (y' @* Ns) @@ (MAP VAR v2) == y' @* Ns'
+
+   LENGTH Ms  = n /\ LENGTH Ns  = n'
+   LENGTH Ms' = m /\ LENGTH Ns' = m'
+
+   y = y'
+   n - m = n' - m' (possibly negative) <=> n + m' = n' + m (non-negative)
+ *)
+Definition equivalent_def :
+    equivalent (M :term) (N :term) =
+        if solvable M /\ solvable N then
+           let M0 = principle_hnf M;
+               N0 = principle_hnf N;
+               n  = LAMl_size M0;
+               n' = LAMl_size N0;
+               vs = FRESH_list (MAX n n') (FV M0 UNION FV N0);
+              vsM = TAKE n  vs;
+              vsN = TAKE n' vs;
+               M1 = principle_hnf (M0 @* (MAP VAR vsM));
+               N1 = principle_hnf (N0 @* (MAP VAR vsN));
+               y  = hnf_head M1;
+               y' = hnf_head N1;
+               m  = LENGTH (hnf_children M1);
+               m' = LENGTH (hnf_children N1);
+           in
+               y = y' /\ n + m' = n' + m
+        else
+           ~solvable M /\ ~solvable N
+End
+
+Theorem equivalent_comm :
+    !M N. equivalent M N <=> equivalent N M
+Proof
+    RW_TAC std_ss [equivalent_def, Once MAX_COMM, Once UNION_COMM]
+ >- (rename1 ‘y2 = y3 /\ n1 + m3 = n3 + m2 <=> y = y1 /\ n + m1 = n1 + m’ \\
+    ‘n3 = n’ by rw [Abbr ‘n3’, Abbr ‘n’] >> gs [] \\
+     EQ_TAC >> rw [])
+ >>  METIS_TAC []
+QED
+
+Theorem equivalent_of_solvables :
+    !M N. solvable M /\ solvable N ==>
+         (equivalent M N <=>
+          let M0 = principle_hnf M;
+              N0 = principle_hnf N;
+              n  = LAMl_size M0;
+              n' = LAMl_size N0;
+              vs = FRESH_list (MAX n n') (FV M0 UNION FV N0);
+             vsM = TAKE n  vs;
+             vsN = TAKE n' vs;
+              M1 = principle_hnf (M0 @* (MAP VAR vsM));
+              N1 = principle_hnf (N0 @* (MAP VAR vsN));
+              y  = hnf_head M1;
+              y' = hnf_head N1;
+              m  = LENGTH (hnf_children M1);
+              m' = LENGTH (hnf_children N1);
+           in
+              y = y' /\ n + m' = n' + m)
+Proof
+    RW_TAC std_ss [equivalent_def]
+QED
+
+(* NOTE: this combined tactic is useful after:
+
+   RW_TAC std_ss [equivalent_def]
+ *)
+val equivalent_tac =
+   ‘hnf M0 /\ hnf N0’ by PROVE_TAC [hnf_principle_hnf, solvable_iff_has_hnf] \\
+   ‘ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M0 UNION FV N0) /\
+    LENGTH vs = MAX n n'’ by rw [Abbr ‘vs’, FRESH_list_def] \\
+    Know ‘?y2 args2. N0 = LAMl vsN (VAR y2 @* args2)’
+    >- (qunabbrevl_tac [‘vsN’, ‘n'’] \\
+        irule (iffLR hnf_cases_shared) >> rw [] \\
+        MATCH_MP_TAC DISJOINT_SUBSET \\
+        Q.EXISTS_TAC ‘FV M0 UNION FV N0’ >> rw [SUBSET_UNION]) \\
+    Know ‘?y1 args1. M0 = LAMl vsM (VAR y1 @* args1)’
+    >- (qunabbrevl_tac [‘vsM’, ‘n’] \\
+        irule (iffLR hnf_cases_shared) >> rw [] \\
+        MATCH_MP_TAC DISJOINT_SUBSET \\
+        Q.EXISTS_TAC ‘FV M0 UNION FV N0’ >> rw [SUBSET_UNION]) \\
+    NTAC 2 STRIP_TAC \\
+    Know ‘M1 = VAR y1 @* args1’
+    >- (qunabbrev_tac ‘M1’ \\
+        Q.PAT_ASSUM ‘M0 = _’ (ONCE_REWRITE_TAC o wrap) \\
+        MATCH_MP_TAC principle_hnf_reduce >> rw [hnf_appstar]) \\
+    DISCH_TAC \\
+    Know ‘N1 = VAR y2 @* args2’
+    >- (qunabbrev_tac ‘N1’ \\
+        Q.PAT_ASSUM ‘N0 = _’ (ONCE_REWRITE_TAC o wrap) \\
+        MATCH_MP_TAC principle_hnf_reduce >> rw [hnf_appstar]) \\
+    DISCH_TAC \\
+   ‘VAR y1 = y’ by rw [Abbr ‘y’, hnf_head_absfree] \\
+   ‘VAR y2 = y'’ by rw [Abbr ‘y'’, hnf_head_absfree];
+
+(* From [1, p.238]. This concerte example shows that dB encoding is not easy in
+   defining this "concept": the literal encoding of inner head variables are not
+   the same for equivalent terms.
+ *)
+Theorem not_equivalent_example :
+    !x y. x <> y ==> ~equivalent (LAM x (VAR y @@ M)) (LAM y (VAR y @@ M))
+Proof
+ (* NOTE: ‘y’ must avoid here for the shared equivalent_tac *)
+    qx_genl_tac [‘x’, ‘v’] >> DISCH_TAC
+ >> ‘hnf (LAM x (VAR v @@ M)) /\ hnf (LAM v (VAR v @@ M))’ by rw []
+ >> ‘solvable (LAM x (VAR v @@ M)) /\ solvable (LAM v (VAR v @@ M))’
+       by rw [solvable_iff_has_hnf, hnf_has_hnf]
+ >> RW_TAC std_ss [equivalent_of_solvables, principle_hnf_eq_self]
+ (* applying shared tactics *)
+ >> equivalent_tac
+ >> qunabbrevl_tac [‘n’, ‘n'’]
+ >> Know ‘LAMl_size M0 = 1 /\ LAMl_size N0 = 1’
+ >- (rw [Abbr ‘M0’, Abbr ‘N0’, LAMl_size_def])
+ >> DISCH_THEN (rfs o wrap)
+ >> qabbrev_tac ‘z = HD vs’
+ >> ‘vs = [z]’ by METIS_TAC [SING_HD]
+ >> Q.PAT_X_ASSUM ‘vsN = vsM’ (rfs o wrap o SYM)
+ >> rfs [Abbr ‘vsN’]
+ >> POP_ASSUM (rfs o wrap)
+ >> qunabbrevl_tac [‘M0’, ‘N0’]
+ >> DISJ1_TAC
+ >> qunabbrevl_tac [‘y’, ‘y'’]
+ (* applying principle_hnf_beta *)
+ >> qabbrev_tac ‘t = VAR v @@ M’
+ >> ‘hnf t’ by rw [Abbr ‘t’]
+ >> Know ‘M1 = [VAR z/x] t’
+ >- (qunabbrev_tac ‘M1’ \\
+     Cases_on ‘z = x’ >- POP_ASSUM (rfs o wrap) \\
+     MATCH_MP_TAC principle_hnf_beta >> simp [Abbr ‘t’] \\
+     rfs [FV_thm])
+ >> Rewr'
+ >> Know ‘N1 = [VAR z/v] t’
+ >- (qunabbrev_tac ‘N1’ \\
+     Cases_on ‘z = v’ >- POP_ASSUM (rfs o wrap) \\
+     MATCH_MP_TAC principle_hnf_beta >> simp [Abbr ‘t’] \\
+     rfs [FV_thm])
+ >> Rewr'
+ >> simp [Abbr ‘t’]
+ (* final goal: y <> z *)
+ >> Q.PAT_X_ASSUM ‘z # LAM x (VAR v @@ M)’ MP_TAC
+ >> rw [FV_thm]
+ >> METIS_TAC []
+QED
+
+Theorem equivalent_unsolvables :
+    !M N. unsolvable M /\ unsolvable N ==> equivalent M N
+Proof
+    rw [equivalent_def]
+QED
+
+(*---------------------------------------------------------------------------*
+ *  Boehm transformations
+ *---------------------------------------------------------------------------*)
+
+(* Definition 10.3.3 (i) *)
+Type transform[pp] = “:(term -> term) list”
+
+(* Definition 10.3.3 (ii) *)
+Definition solving_transform_def :
+    solving_transform (f :term -> term) <=>
+      (?x. f = \p. p @@ VAR x) \/ (?x N. f = [N/x])
+End
+
+Theorem solving_transform_subst[simp] :
+    solving_transform [N/x]
+Proof
+    rw [solving_transform_def]
+ >> DISJ2_TAC >> qexistsl_tac [‘x’, ‘N’] >> rw []
+QED
+
+Theorem solving_transform_rightctxt[simp] :
+    solving_transform (rightctxt (VAR x))
+Proof
+    rw [solving_transform_def, FUN_EQ_THM]
+ >> DISJ1_TAC
+ >> Q.EXISTS_TAC ‘x’ >> rw [rightctxt_thm]
+QED
+
+Theorem solving_transform_lameq :
+    !f M N. solving_transform f /\ M == N ==> f M == f N
+Proof
+    rw [solving_transform_def, FUN_EQ_THM]
+ >- rw [lameq_rules]
+ >> rw [lameq_sub_cong]
+QED
+
+(* Definition 10.3.3 (iii)
+
+   NOTE: "Boehm transform is a finite composition of solving transforms
+        (including the identity as a composition of zero transforms).
+
+   Here we just define "Boehm transform" as a list of solving transforms,
+   thus always finite. The "composition" part depends on how this list is used.
+ *)
+Definition Boehm_transform_def :
+    Boehm_transform pi = EVERY solving_transform pi
+End
+
+Theorem Boehm_transform_CONS[simp] :
+    Boehm_transform (h::pi) <=> solving_transform h /\ Boehm_transform pi
+Proof
+    rw [Boehm_transform_def]
+QED
+
+Theorem Boehm_transform_SNOC[simp] :
+    Boehm_transform (SNOC h pi) <=> Boehm_transform pi /\ solving_transform h
+Proof
+    rw [Boehm_transform_def, EVERY_SNOC]
+QED
+
+(* ‘apply pi M’ (applying a Boehm transformation) means "M^{pi}" or "pi(M)"
+
+   NOTE: ‘apply [f3;f2;f1] M = (f3 o f2 o f1) M = f3 (f2 (f1 M))’ *)
+Definition apply_def :
+    apply pi = FOLDR $o I pi
+End
+
+(* NOTE: either FOLDL or FOLDR is correct (due to combinTheory.o_ASSOC),
+         but FOLDR seems more natural requiring natural list induction in
+         the next proof(s), while FOLDL would require SNOC_INDUCT.
+ *)
+Theorem apply_alt :
+    !pi. apply pi = FOLDL $o I pi
+Proof
+    REWRITE_TAC [apply_def]
+ >> Induct_on ‘pi’ >> rw [FOLDL, FOLDR]
+ >> KILL_TAC (* only FOLDL is left *)
+ >> Induct_on ‘pi’ using SNOC_INDUCT
+ >> rw [FOLDL_SNOC, FOLDL]
+ >> POP_ASSUM (rw o wrap o SYM)
+QED
+
+Theorem apply_rwts[simp] :
+    (apply [] = I) /\
+    (!f pi M. apply (f::pi) M = f (apply pi M)) /\
+    (!f pi M. apply (SNOC f pi) M = apply pi (f M))
+Proof
+    NTAC 2 (CONJ_TAC >- rw [apply_def, o_DEF])
+ >> rw [apply_alt, o_DEF, FOLDL_SNOC]
+QED
+
+(* Lemma 10.3.4 (i) [1, p.246] *)
+Theorem Boehm_transform_lameq_ctxt :
+    !pi. Boehm_transform pi ==> ?c. ctxt c /\ !M. apply pi M == c M
+Proof
+    Induct_on ‘pi’
+ >> rw [Boehm_transform_def, apply_def]
+ >- (Q.EXISTS_TAC ‘\x. x’ >> rw [ctxt_rules, FOLDR])
+ >> fs [GSYM Boehm_transform_def, apply_def]
+ >> fs [solving_transform_def]
+ >- (Q.EXISTS_TAC ‘\y. c y @@ (\y. VAR x) y’ \\
+     rw [ctxt_rules, FOLDR] \\
+     MATCH_MP_TAC lameq_APPL >> art [])
+ (* stage work *)
+ >> Q.EXISTS_TAC ‘\y. (\z. LAM x (c z)) y @@ (\y. N) y’
+ >> rw [ctxt_rules, constant_contexts_exist, FOLDR]
+ >> MATCH_MP_TAC lameq_TRANS
+ >> Q.EXISTS_TAC ‘[N/x] (c M)’
+ >> reverse CONJ_TAC >- rw [lameq_rules]
+ >> irule lameq_sub_cong >> rw []
+QED
+
+Theorem asmlam_apply_cong :
+    !pi M N. Boehm_transform pi /\ asmlam eqns M N ==>
+             asmlam eqns (apply pi M) (apply pi N)
+Proof
+    Induct_on ‘pi’ using SNOC_INDUCT >> rw []
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
+ >> fs [solving_transform_def]
+ >- rw [asmlam_rules]
+ >> MATCH_MP_TAC asmlam_subst >> art []
+QED
+
+(* Used by: separability_lemma2 *)
+Theorem lameq_apply_cong :
+    !pi M N. Boehm_transform pi /\ M == N ==> apply pi M == apply pi N
+Proof
+    Induct_on ‘pi’ using SNOC_INDUCT >> rw []
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
+ >> MATCH_MP_TAC solving_transform_lameq >> art []
+QED
+
+Theorem Boehm_transform_APPEND :
+    !p1 p2. Boehm_transform p1 /\ Boehm_transform p2 ==> Boehm_transform (p1 ++ p2)
+Proof
+    rw [Boehm_transform_def]
+QED
+
+Theorem Boehm_apply_APPEND :
+    !p1 p2 M. apply (p1 ++ p2) M = apply p1 (apply p2 M)
+Proof
+    Q.X_GEN_TAC ‘p1’
+ >> Induct_on ‘p2’ using SNOC_INDUCT
+ >> rw [APPEND_SNOC]
+QED
+
+(* Used by separability_lemma2 *)
+Theorem Boehm_apply_MAP_rightctxt :
+    !Ns t. apply (MAP rightctxt Ns) t = t @* (REVERSE Ns)
+Proof
+    Induct_on ‘Ns’ >> rw [rightctxt_thm]
+ >> rw [GSYM SNOC_APPEND]
+QED
+
+(* Used by separability_lemma0 *)
+Theorem Boehm_apply_MAP_rightctxt' :
+    !Ns t. apply (MAP rightctxt (REVERSE Ns)) t = t @* Ns
+Proof
+    rpt GEN_TAC
+ >> qabbrev_tac ‘Ns' = REVERSE Ns’
+ >> ‘Ns = REVERSE Ns'’ by rw [Abbr ‘Ns'’, REVERSE_REVERSE]
+ >> rw [Boehm_apply_MAP_rightctxt]
+QED
+
+(* Used by separability_lemma2 *)
+Theorem Boehm_apply_unsolvable :
+    !pi M. Boehm_transform pi /\ unsolvable M ==> unsolvable (apply pi M)
+Proof
+    Induct_on ‘pi’ using SNOC_INDUCT >> rw []
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
+ >> fs [solving_transform_def, solvable_iff_has_hnf] (* 2 subgaols *)
+ >| [ (* goal 1 (of 2) *)
+      CCONTR_TAC >> fs [] \\
+      METIS_TAC [has_hnf_APP_E],
+      (* goal 2 (of 2) *)
+      CCONTR_TAC >> fs [] \\
+      METIS_TAC [has_hnf_SUB_E] ]
+QED
+
+(*---------------------------------------------------------------------------*
+ *  Separability of terms
+ *---------------------------------------------------------------------------*)
+
+Theorem separability_lemma0_case2[local] :
+    !y args1 args2 k. 0 < k /\ LENGTH args1 = LENGTH args2 + k ==>
+       !P Q. ?pi. Boehm_transform pi /\
+                  apply pi (VAR y @* args1) == P /\
+                  apply pi (VAR y @* args2) == Q
+Proof
+    rpt STRIP_TAC
+ >> qabbrev_tac ‘M1 = VAR y @* args1’
+ >> qabbrev_tac ‘N1 = VAR y @* args2’
+ >> qabbrev_tac ‘p  = LENGTH args1’
+ >> qabbrev_tac ‘p' = LENGTH args2’
+ >> qabbrev_tac ‘vs = FRESH_list (k + 1) (y INSERT FV P UNION FV Q)’
+ >> ‘ALL_DISTINCT vs /\ DISJOINT (set vs) (y INSERT FV P UNION FV Q)’
+      by rw [Abbr ‘vs’, FRESH_list_def]
+ >> qabbrev_tac ‘a = HD vs’
+ >> qabbrev_tac ‘bs = DROP 1 vs’
+ >> Know ‘LENGTH bs + 1 = LENGTH vs /\ 1 < LENGTH vs’
+ >- (‘LENGTH vs = k + 1’ by rw [Abbr ‘vs’, FRESH_list_def] \\
+     rw [Abbr ‘bs’])
+ >> STRIP_TAC
+ >> ‘vs <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
+ (* p1 = ()a b_1 b_2 ... b_k *)
+ >> qabbrev_tac ‘p1 = MAP rightctxt (REVERSE (MAP VAR vs))’
+ >> ‘Boehm_transform p1’ by rw [Boehm_transform_def, Abbr ‘p1’, EVERY_MAP]
+ >> ‘apply p1 M1 = VAR y @* (args1 ++ MAP VAR vs)’
+      by (rw [Abbr ‘M1’, Abbr ‘p1’, Boehm_apply_MAP_rightctxt', appstar_APPEND])
+ >> ‘apply p1 N1 = VAR y @* (args2 ++ MAP VAR vs)’
+      by (rw [Abbr ‘N1’, Abbr ‘p1’, Boehm_apply_MAP_rightctxt', appstar_APPEND])
+ (* p2 *)
+ >> qabbrev_tac ‘Z = FRESH_list (p + 1) {}’
+ >> ‘ALL_DISTINCT Z /\ LENGTH Z = p + 1’ by rw [Abbr ‘Z’, FRESH_list_def]
+ >> ‘Z <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
+ >> qabbrev_tac ‘z = LAST Z’
+ >> qabbrev_tac ‘p2 = [[LAMl Z (VAR z)/y]]’
+ >> ‘Boehm_transform p2’ by rw [Boehm_transform_def, Abbr ‘p2’]
+ >> Know ‘apply p2 (VAR y @* (args1 ++ MAP VAR vs)) == VAR a @* MAP VAR bs’
+ >- (simp [Abbr ‘p2’, appstar_SUB] \\
+     Know ‘MAP [LAMl Z (VAR z)/y] (MAP VAR vs) = MAP VAR vs’
+     >- (rw [LIST_EQ_REWRITE, EL_MAP] \\
+         MATCH_MP_TAC lemma14b \\
+         Q.PAT_X_ASSUM ‘DISJOINT (set vs) _’ (MP_TAC o (ONCE_REWRITE_RULE [DISJOINT_SYM])) \\
+         rw [DISJOINT_ALT, MEM_EL] >> METIS_TAC []) >> Rewr' \\
+     qabbrev_tac ‘args1' = MAP [LAMl Z (VAR z)/y] args1’ \\
+     Know ‘LAMl Z (VAR z) = LAMl (FRONT Z) (LAM z (VAR z))’
+     >- (REWRITE_TAC [GSYM LAMl_SNOC] \\
+         Suff ‘SNOC z (FRONT Z) = Z’ >- Rewr \\
+         qunabbrev_tac ‘z’ >> MATCH_MP_TAC SNOC_LAST_FRONT >> art []) >> Rewr' \\
+     REWRITE_TAC [appstar_APPEND] \\
+     qabbrev_tac ‘t :term = LAM z (VAR z)’ \\
+     MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘t @* MAP VAR vs’ \\
+     CONJ_TAC >- (MATCH_MP_TAC lameq_appstar_cong \\
+                  MATCH_MP_TAC lameq_LAMl_appstar_reduce \\
+                  rw [Abbr ‘t’, Abbr ‘args1'’, LENGTH_FRONT]) \\
+     qunabbrev_tac ‘t’ \\
+     Know ‘MAP VAR vs = (VAR a::MAP VAR bs) :term list’
+     >- (rw [Abbr ‘a’, Abbr ‘bs’, LIST_EQ_REWRITE, MAP_DROP] \\
+         Cases_on ‘x’ >- rw [EL_MAP] \\
+         rw [EL_MAP, EL_DROP, ADD1]) >> Rewr' \\
+     rw [GSYM I_alt] \\
+     MATCH_MP_TAC lameq_appstar_cong >> rw [lameq_I])
+ >> DISCH_TAC
+ >> qabbrev_tac ‘b0 = LAST bs’
+ >> Know ‘apply p2 (VAR y @* (args2 ++ MAP VAR vs)) == VAR b0’
+ >- (simp [Abbr ‘p2’, appstar_SUB] \\
+     Know ‘MAP [LAMl Z (VAR z)/y] (MAP VAR vs) = MAP VAR vs’
+     >- (rw [LIST_EQ_REWRITE, EL_MAP] \\
+         MATCH_MP_TAC lemma14b \\
+         Q.PAT_X_ASSUM ‘DISJOINT (set vs) _’ (MP_TAC o (ONCE_REWRITE_RULE [DISJOINT_SYM])) \\
+         rw [DISJOINT_ALT, MEM_EL] >> METIS_TAC []) >> Rewr' \\
+     qabbrev_tac ‘args2' = MAP [LAMl Z (VAR z)/y] args2’ \\
+     Know ‘LAMl Z (VAR z) = LAMl (FRONT Z) (LAM z (VAR z))’
+     >- (REWRITE_TAC [GSYM LAMl_SNOC] \\
+         Suff ‘SNOC z (FRONT Z) = Z’ >- Rewr \\
+         qunabbrev_tac ‘z’ >> MATCH_MP_TAC SNOC_LAST_FRONT >> art []) >> Rewr' \\
+     Know ‘args2' ++ MAP VAR vs = SNOC (VAR b0) (args2' ++ MAP VAR (FRONT vs))’
+     >- (qunabbrev_tac ‘b0’ \\
+         Know ‘VAR (LAST bs) :term = LAST (MAP VAR vs)’
+         >- (rw [Abbr ‘bs’, listTheory.last_drop, LAST_MAP]) >> Rewr' \\
+         Know ‘args2' ++ MAP VAR (FRONT vs) = FRONT (args2' ++ MAP VAR vs)’
+         >- (rw [MAP_FRONT] \\
+             MATCH_MP_TAC (GSYM FRONT_APPEND_NOT_NIL) >> rw []) >> Rewr' \\
+         Suff ‘LAST (MAP VAR vs) = LAST (args2' ++ MAP VAR vs)’
+         >- (Rewr' >> qabbrev_tac ‘l = args2' ++ MAP VAR vs’ \\
+             MATCH_MP_TAC (GSYM SNOC_LAST_FRONT) >> rw [Abbr ‘l’]) \\
+         MATCH_MP_TAC (GSYM LAST_APPEND_NOT_NIL) >> rw []) >> Rewr' \\
+     REWRITE_TAC [appstar_SNOC] \\
+     qabbrev_tac ‘t :term = LAM z (VAR z)’ \\
+     MATCH_MP_TAC lameq_TRANS \\
+     Q.EXISTS_TAC ‘t @@ VAR b0’ \\
+     CONJ_TAC >- (MATCH_MP_TAC lameq_APPL \\
+                  MATCH_MP_TAC lameq_LAMl_appstar_reduce \\
+                  rw [Abbr ‘t’, Abbr ‘args2'’, LENGTH_FRONT] \\
+                 ‘LENGTH vs = k + 1’ by rw [Abbr ‘vs’, FRESH_list_def] >> rw []) \\
+     rw [Abbr ‘t’, GSYM I_alt, lameq_I])
+ >> DISCH_TAC
+ (* p3 *)
+ >> qabbrev_tac ‘f1 = [LAMl bs P/a]’
+ >> qabbrev_tac ‘f2 = [Q/b0]’
+ >> qabbrev_tac ‘p3 = [f2; f1]’
+ >> Know ‘Boehm_transform p3’
+ >- (rw [Abbr ‘p3’, Abbr ‘f1’, Abbr ‘f2’, Boehm_transform_def, EVERY_DEF])
+ >> DISCH_TAC
+ >> Know ‘f1 (VAR a @* MAP VAR bs) == P’
+ >- (rw [Abbr ‘f1’, appstar_SUB] \\
+     Know ‘MAP [LAMl bs P/a] (MAP VAR bs) = MAP VAR bs’
+     >- (rw [LIST_EQ_REWRITE, EL_MAP] \\
+         MATCH_MP_TAC lemma14b >> simp [FV_thm] \\
+         Q.PAT_X_ASSUM ‘ALL_DISTINCT vs’ MP_TAC \\
+         Cases_on ‘vs’ >- FULL_SIMP_TAC std_ss [] \\
+         fs [Abbr ‘a’, Abbr ‘bs’, LENGTH_DROP] \\
+         METIS_TAC [MEM_EL]) >> Rewr' \\
+     MATCH_MP_TAC lameq_LAMl_appstar_reduce >> simp [] \\
+     Q.PAT_X_ASSUM ‘DISJOINT (set vs) _’ MP_TAC \\
+     rw [DISJOINT_ALT, Abbr ‘bs’, MEM_DROP, MEM_EL] \\
+     METIS_TAC [])
+ >> DISCH_TAC
+ >> Know ‘f2 P = P’
+ >- (rw [Abbr ‘f2’] >> MATCH_MP_TAC lemma14b \\
+     Q.PAT_X_ASSUM ‘DISJOINT (set vs) _’ MP_TAC \\
+     rw [DISJOINT_ALT, Abbr ‘bs’, Abbr ‘b0’, MEM_DROP, MEM_EL, LAST_EL, EL_DROP] \\
+     Suff ‘PRE (LENGTH vs - 1) + 1 < LENGTH vs’ >- METIS_TAC [] \\
+     rw [])
+ >> DISCH_TAC
+ >> Know ‘f1 (VAR b0) = VAR b0’
+ >- (rw [Abbr ‘f1’] >> MATCH_MP_TAC lemma14b \\
+     Q.PAT_X_ASSUM ‘ALL_DISTINCT vs’ MP_TAC \\
+     Cases_on ‘vs’ >- FULL_SIMP_TAC std_ss [] \\
+     fs [Abbr ‘a’, Abbr ‘bs’, Abbr ‘b0’, LENGTH_DROP] \\
+     ‘t <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0] \\
+     rw [MEM_EL, LAST_EL] \\
+     Suff ‘PRE (LENGTH t) < LENGTH t’ >- METIS_TAC [] \\
+     rw [])
+ >> DISCH_TAC
+ >> ‘f2 (VAR b0) = Q’ by rw [Abbr ‘f2’]
+ (* final stage *)
+ >> Q.EXISTS_TAC ‘p3 ++ p2 ++ p1’
+ >> CONJ_ASM1_TAC
+ >- (MATCH_MP_TAC Boehm_transform_APPEND >> art [] \\
+     MATCH_MP_TAC Boehm_transform_APPEND >> art [])
+ >> CONJ_TAC
+ >| [ (* goal 1 (of 2) *)
+      rw [Boehm_apply_APPEND] \\
+      MATCH_MP_TAC lameq_TRANS \\
+      Q.EXISTS_TAC ‘apply p3 (VAR a @* MAP VAR bs)’ \\
+      CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> art []) \\
+      rw [Abbr ‘p3’] \\
+      MATCH_MP_TAC lameq_TRANS \\
+      Q.EXISTS_TAC ‘f2 P’ \\
+      reverse CONJ_TAC >- rw [] \\
+      MATCH_MP_TAC solving_transform_lameq >> rw [Abbr ‘f2’],
+      (* goal 2 (of 2) *)
+      REWRITE_TAC [Boehm_apply_APPEND] \\
+      Q.PAT_X_ASSUM ‘apply P1 N1 = _’ (ONCE_REWRITE_TAC o wrap) \\
+      MATCH_MP_TAC lameq_TRANS \\
+      Q.EXISTS_TAC ‘apply p3 (VAR b0)’ \\
+      reverse CONJ_TAC >- rw [Abbr ‘p3’] \\
+      MATCH_MP_TAC lameq_apply_cong >> art [] ]
+QED
+
+Theorem separability_lemma0[local] :
+    !M N. solvable (M :term) /\ solvable N /\
+          LAMl_size (principle_hnf M) <= LAMl_size (principle_hnf N) ==>
+          equivalent M N \/
+          !P Q. ?pi. Boehm_transform pi /\ apply pi M == P /\ apply pi N == Q
+Proof
+    RW_TAC std_ss [equivalent_def]
+ (* applying the shared equivalent_tac *)
+ >> equivalent_tac
+ (* cleanup MAX and vsN *)
+ >> ‘MAX n n' = n'’ by rw [MAX_DEF]
+ >> POP_ASSUM (REV_FULL_SIMP_TAC std_ss o wrap)
+ >> ‘vsN = vs’ by rw [Abbr ‘vsN’, TAKE_LENGTH_ID_rwt]
+ >> qunabbrev_tac ‘vsN’
+ >> POP_ASSUM (REV_FULL_SIMP_TAC std_ss o wrap)
+ (* Case 1 *)
+ >> Cases_on ‘y <> y'’
+ >- (simp [] >> rpt GEN_TAC \\
+    ‘y1 <> y2’ by (CCONTR_TAC >> fs []) \\
+     qabbrev_tac ‘k = n' - n’ \\
+    ‘n + k = n'’ by rw [Abbr ‘k’] \\
+     qabbrev_tac ‘p0 = MAP rightctxt (REVERSE (MAP VAR vs))’ \\
+  (* properties of p0 *)
+    ‘Boehm_transform p0’ by rw [Boehm_transform_def, Abbr ‘p0’, EVERY_MAP] \\
+     Know ‘apply p0 N0 == N1’
+     >- (rw [Abbr ‘p0’, Boehm_apply_MAP_rightctxt']) >> DISCH_TAC \\
+     Know ‘apply p0 M0 == M1 @* DROP n (MAP VAR vs)’
+     >- (qabbrev_tac ‘l :term list = MAP VAR vs’ \\
+         qunabbrev_tac ‘p0’ \\
+         Know ‘REVERSE l = REVERSE (TAKE n l ++ DROP n l)’
+         >- REWRITE_TAC [TAKE_DROP] >> Rewr' \\
+         REWRITE_TAC [REVERSE_APPEND, MAP_APPEND, Boehm_apply_APPEND] \\
+         REWRITE_TAC [Boehm_apply_MAP_rightctxt'] \\
+         MATCH_MP_TAC lameq_appstar_cong \\
+         rw [Abbr ‘l’, Abbr ‘vsM’, GSYM MAP_TAKE]) >> DISCH_TAC \\
+  (* now use P and Q
+
+     NOTE: This Z = [z1;z2] contains two fresh variables fixing the textbook proof,
+           where [1, p.254] the iterated substition "[LAMl as P/y1] [LAMl as' Q/y2]"
+           must be fixed to act as a simultaneous substitition:
+
+       [LAMl as [VAR z2/y2]P/y1] [LAMl as' [VAR z1/y1]Q/y2] [VAR y1/z1] [VAR y2/z2]
+   *)
+     qabbrev_tac ‘Z = FRESH_list 2 (FV P UNION FV Q)’ \\
+    ‘ALL_DISTINCT Z /\ DISJOINT (set Z) (FV P UNION FV Q) /\ LENGTH Z = 2’
+       by rw [FRESH_list_def, Abbr ‘Z’] \\
+     qabbrev_tac ‘z1 = EL 0 Z’ \\
+     qabbrev_tac ‘z2 = EL 1 Z’ \\
+    ‘MEM z1 Z /\ MEM z2 Z’
+       by (rw [MEM_EL, Abbr ‘z1’, Abbr ‘z2’] >| (* 2 subgoals *)
+           [ Q.EXISTS_TAC ‘0’ >> rw [],
+             Q.EXISTS_TAC ‘1’ >> rw [] ]) \\
+    ‘z1 <> z2’ by (rw [Abbr ‘z1’, Abbr ‘z2’, ALL_DISTINCT_EL_IMP]) \\
+     qabbrev_tac ‘as = FRESH_list (m + k) (FV P UNION set Z)’ \\
+    ‘LENGTH as = m + k /\ DISJOINT (set as) (FV P UNION set Z)’
+       by rw [Abbr ‘as’, FRESH_list_def] \\
+     qabbrev_tac ‘as' = FRESH_list m' (FV Q UNION set Z)’ \\
+    ‘LENGTH as' = m' /\ DISJOINT (set as') (FV Q UNION set Z)’
+       by rw [Abbr ‘as'’, FRESH_list_def] \\
+     qabbrev_tac ‘f1 = [LAMl as  ([VAR z2/y2] P)/y1]’ \\
+     qabbrev_tac ‘f2 = [LAMl as' ([VAR z1/y1] Q)/y2]’ \\
+     qabbrev_tac ‘f3 :term -> term = [VAR y1/z1]’ \\
+     qabbrev_tac ‘f4 :term -> term = [VAR y2/z2]’ \\
+     qabbrev_tac ‘p1 = [f4; f3; f2; f1]’ \\
+  (* properties of p1 *)
+    ‘Boehm_transform p1’ by rw [Boehm_transform_def, Abbr ‘p1’,
+                                Abbr ‘f1’, Abbr ‘f2’, Abbr ‘f3’, Abbr ‘f4’] \\
+     Know ‘DISJOINT (set as) (FV ([VAR z2/y2] P))’
+     >- (MATCH_MP_TAC DISJOINT_SUBSET \\
+         Q.EXISTS_TAC ‘FV P UNION set Z’ >> art [] \\
+         simp [FV_SUB] \\
+         Cases_on ‘y2 IN FV P’ >> rw [SUBSET_DEF, Abbr ‘z2’] >> art []) \\
+     DISCH_TAC \\
+     Know ‘DISJOINT (set as') (FV ([VAR z1/y1] Q))’
+     >- (MATCH_MP_TAC DISJOINT_SUBSET \\
+         Q.EXISTS_TAC ‘FV Q UNION set Z’ >> art [] \\
+         simp [FV_SUB] \\
+         Cases_on ‘y1 IN FV Q’ >> rw [SUBSET_DEF, Abbr ‘z2’] >> art []) \\
+     DISCH_TAC \\
+  (* stage work *)
+     Q.EXISTS_TAC ‘p1 ++ p0’ \\
+     CONJ_ASM1_TAC >- rw [Boehm_transform_APPEND] \\
+     reverse CONJ_TAC >| (* 2 subgoals, Q part seems easier *)
+     [ (* goal 1 (of 2) *)
+       MATCH_MP_TAC lameq_TRANS \\
+       Q.EXISTS_TAC ‘apply (p1 ++ p0) N0’ \\
+       CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
+                    qunabbrev_tac ‘N0’ >> MATCH_MP_TAC lameq_SYM \\
+                    MATCH_MP_TAC lameq_principle_hnf >> art [GSYM solvable_iff_has_hnf]) \\
+    (* eliminating p0 *)
+       REWRITE_TAC [Boehm_apply_APPEND] \\
+       MATCH_MP_TAC lameq_TRANS \\
+       Q.EXISTS_TAC ‘apply p1 N1’ \\
+       CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> art []) \\
+       SIMP_TAC (srw_ss()) [Abbr ‘p1’] (* f4 (f3 (f2 (f1 N1))) == Q *) \\
+    (* eliminating f1 *)
+      ‘f1 N1 = VAR y2 @* (MAP f1 args2)’
+          by (rw [appstar_SUB, Abbr ‘f1’]) >> POP_ORW \\
+    (* eliminating f2 *)
+       qunabbrev_tac ‘f2’ \\
+       MATCH_MP_TAC lameq_TRANS \\
+       Q.EXISTS_TAC ‘f4 (f3 ([VAR z1/y1] Q))’ \\
+       CONJ_TAC >- (MATCH_MP_TAC solving_transform_lameq \\
+                    CONJ_TAC >- rw [Abbr ‘f4’] \\
+                    MATCH_MP_TAC solving_transform_lameq \\
+                    CONJ_TAC >- rw [Abbr ‘f3’] \\
+                    MATCH_MP_TAC lameq_hnf_fresh_subst >> art [] \\
+                    rw [Abbr ‘m'’, hnf_children_hnf]) \\
+    (* eliminating f3 *)
+       qunabbrev_tac ‘f3’ \\
+       Know ‘[VAR y1/z1] ([VAR z1/y1] Q) = Q’
+       >- (MATCH_MP_TAC lemma15b \\
+           Q.PAT_X_ASSUM ‘DISJOINT (set Z) (FV P UNION FV Q)’ MP_TAC \\
+           rw [DISJOINT_ALT] >> METIS_TAC []) >> Rewr' \\
+    (* eliminating f4 *)
+       qunabbrev_tac ‘f4’ \\
+       Suff ‘[VAR y2/z2] Q = Q’ >- rw [] \\
+       MATCH_MP_TAC lemma14b \\
+       Q.PAT_X_ASSUM ‘DISJOINT (set Z) (FV P UNION FV Q)’ MP_TAC \\
+       rw [DISJOINT_ALT] >> METIS_TAC [],
+       (* goal 2 (of 2) *)
+       MATCH_MP_TAC lameq_TRANS \\
+       Q.EXISTS_TAC ‘apply (p1 ++ p0) M0’ \\
+       CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
+                    qunabbrev_tac ‘M0’ \\
+                    MATCH_MP_TAC lameq_SYM \\
+                    MATCH_MP_TAC lameq_principle_hnf >> art [GSYM solvable_iff_has_hnf]) \\
+    (* eliminating p0 *)
+       REWRITE_TAC [Boehm_apply_APPEND] \\
+       MATCH_MP_TAC lameq_TRANS \\
+       Q.EXISTS_TAC ‘apply p1 (M1 @* DROP n (MAP VAR vs))’ \\
+       CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> art []) \\
+       SIMP_TAC (srw_ss()) [Abbr ‘p1’] (* f4 (f3 (f2 (f1 M1))) == P *) \\
+    (* eliminating f1 *)
+       MATCH_MP_TAC lameq_TRANS \\
+       Q.EXISTS_TAC ‘f4 (f3 (f2 ([VAR z2/y2] P)))’ \\
+       CONJ_TAC >- (MATCH_MP_TAC solving_transform_lameq \\
+                    CONJ_TAC >- rw [Abbr ‘f4’] \\
+                    MATCH_MP_TAC solving_transform_lameq \\
+                    CONJ_TAC >- rw [Abbr ‘f3’] \\
+                    MATCH_MP_TAC solving_transform_lameq \\
+                    CONJ_TAC >- rw [Abbr ‘f2’] \\
+                    rw [appstar_SUB, GSYM appstar_APPEND, Abbr ‘f1’] \\
+                    MATCH_MP_TAC lameq_LAMl_appstar_reduce >> art [] \\
+                    rw [Abbr ‘m’, hnf_children_hnf]) \\
+    (* eliminating f2 *)
+       Know ‘f2 ([VAR z2/y2] P) = [VAR z2/y2] P’
+       >- (qunabbrev_tac ‘f2’ \\
+           MATCH_MP_TAC lemma14b >> rw [FV_SUB] \\
+           CCONTR_TAC >> ‘MEM y2 Z’ by METIS_TAC [] \\
+           Q.PAT_X_ASSUM ‘DISJOINT (set Z) (FV P UNION FV Q)’
+               (MP_TAC o ONCE_REWRITE_RULE [DISJOINT_SYM]) \\
+           rw [DISJOINT_ALT] >> METIS_TAC []) >> Rewr' \\
+    (* eliminating f3 *)
+       Know ‘f3 ([VAR z2/y2] P) = [VAR z2/y2] P’
+       >- (qunabbrev_tac ‘f3’ \\
+           MATCH_MP_TAC lemma14b \\
+           Suff ‘z1 # P’ >- rw [FV_SUB] \\
+           Q.PAT_X_ASSUM ‘DISJOINT (set Z) (FV P UNION FV Q)’ MP_TAC \\
+           rw [DISJOINT_ALT] >> METIS_TAC []) >> Rewr' \\
+    (* eliminating f4 *)
+       qunabbrev_tac ‘f4’ \\
+       Suff ‘[VAR y2/z2] ([VAR z2/y2] P) = P’ >- rw [] \\
+       MATCH_MP_TAC lemma15b \\
+       Q.PAT_X_ASSUM ‘DISJOINT (set Z) (FV P UNION FV Q)’ MP_TAC \\
+       rw [DISJOINT_ALT] >> METIS_TAC [] ])
+ (* Case 2 *)
+ >> REWRITE_TAC [DECIDE “P \/ Q <=> ~P ==> Q”]
+ >> rfs [] >> DISCH_TAC (* m' + n <> m + n' *)
+ >> rpt GEN_TAC
+ (* p0 is the same as in case 1 *)
+ >> qabbrev_tac ‘p0 = MAP rightctxt (REVERSE (MAP VAR vs))’
+ (* properties of p0 *)
+ >> ‘Boehm_transform p0’ by rw [Boehm_transform_def, Abbr ‘p0’, EVERY_MAP]
+ >> Know ‘apply p0 N0 == N1’
+ >- rw [Abbr ‘p0’, Boehm_apply_MAP_rightctxt']
+ >> ‘LENGTH args2 = m'’ by rw [Abbr ‘m'’, hnf_children_hnf]
+ >> Q.PAT_X_ASSUM ‘N1 = _’ (ONCE_REWRITE_TAC o wrap)
+ >> DISCH_TAC
+ >> Know ‘apply p0 M0 == M1 @* DROP n (MAP VAR vs)’
+ >- (qabbrev_tac ‘l :term list = MAP VAR vs’ \\
+     qunabbrev_tac ‘p0’ \\
+     Know ‘REVERSE l = REVERSE (TAKE n l ++ DROP n l)’
+     >- REWRITE_TAC [TAKE_DROP] >> Rewr' \\
+     REWRITE_TAC [REVERSE_APPEND, MAP_APPEND, Boehm_apply_APPEND] \\
+     REWRITE_TAC [Boehm_apply_MAP_rightctxt'] \\
+     MATCH_MP_TAC lameq_appstar_cong \\
+     rw [Abbr ‘l’, Abbr ‘vsM’, GSYM MAP_TAKE])
+ >> ‘LENGTH args1 = m’ by rw [Abbr ‘m’, hnf_children_hnf]
+ >> Q.PAT_X_ASSUM ‘M1 = _’ (ONCE_REWRITE_TAC o wrap)
+ >> ‘VAR y1 = VAR y2 :term’ by PROVE_TAC [] >> POP_ORW
+ >> REWRITE_TAC [GSYM appstar_APPEND]
+ >> qabbrev_tac ‘args1' = args1 ++ DROP n (MAP VAR vs)’
+ >> DISCH_TAC
+ >> qabbrev_tac ‘l = LENGTH args1'’
+ >> ‘l <> m'’ by rw [Abbr ‘l’, Abbr ‘args1'’]
+ (* stage work *)
+ >> ‘m' < l \/ l < m'’ by rw [] (* 2 subgoals, same ending tactics *)
+ >| [ (* goal 1 (of 2) *)
+      MP_TAC (Q.SPECL [‘y2’, ‘args1'’, ‘args2’, ‘l - m'’] separability_lemma0_case2) \\
+      simp [] \\
+      DISCH_THEN (STRIP_ASSUME_TAC o (Q.SPECL [‘P’, ‘Q’])),
+      (* goal 2 (of 2) *)
+      MP_TAC (Q.SPECL [‘y2’, ‘args2’, ‘args1'’, ‘m' - l’] separability_lemma0_case2) \\
+      simp [] \\
+      DISCH_THEN (STRIP_ASSUME_TAC o (Q.SPECL [‘Q’, ‘P’])) ]
+ (* shared tactics *)
+ >> (Q.EXISTS_TAC ‘pi ++ p0’ \\
+     CONJ_ASM1_TAC >- rw [Boehm_transform_APPEND] \\
+     CONJ_TAC >| (* 2 subgoals *)
+     [ (* goal 1.1 (of 2) *)
+       MATCH_MP_TAC lameq_TRANS \\
+       Q.EXISTS_TAC ‘apply (pi ++ p0) M0’ \\
+       CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
+                    qunabbrev_tac ‘M0’ >> MATCH_MP_TAC lameq_SYM \\
+                    MATCH_MP_TAC lameq_principle_hnf \\
+                    ASM_REWRITE_TAC [GSYM solvable_iff_has_hnf]) \\
+       REWRITE_TAC [Boehm_apply_APPEND] \\
+       MATCH_MP_TAC lameq_TRANS \\
+       Q.EXISTS_TAC ‘apply pi (y' @* args1')’ \\
+       reverse CONJ_TAC >- art [] \\
+       MATCH_MP_TAC lameq_apply_cong \\
+       Q.PAT_X_ASSUM ‘VAR y2 = y'’ (ONCE_REWRITE_TAC o wrap o SYM) >> art [],
+       (* goal 1.2 (of 2) *)
+       MATCH_MP_TAC lameq_TRANS \\
+       Q.EXISTS_TAC ‘apply (pi ++ p0) N0’ \\
+       CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
+                    qunabbrev_tac ‘N0’ >> MATCH_MP_TAC lameq_SYM \\
+                    MATCH_MP_TAC lameq_principle_hnf \\
+                    ASM_REWRITE_TAC [GSYM solvable_iff_has_hnf]) \\
+       REWRITE_TAC [Boehm_apply_APPEND] \\
+       MATCH_MP_TAC lameq_TRANS \\
+       Q.EXISTS_TAC ‘apply pi (y @* args2)’ \\
+       reverse CONJ_TAC >- art [] \\
+       MATCH_MP_TAC lameq_apply_cong \\
+       Q.PAT_X_ASSUM ‘y = y'’ (ONCE_REWRITE_TAC o wrap) \\
+       Q.PAT_X_ASSUM ‘VAR y2 = y'’ (ONCE_REWRITE_TAC o wrap o SYM) >> art [] ])
+QED
+
+(* Lemma 10.4.1 (i) [1, p.254] *)
+Theorem separability_lemma1 :
+    !M N. solvable (M :term) /\ solvable N /\ ~equivalent M N ==>
+          !P Q. ?pi. Boehm_transform pi /\ apply pi M == P /\ apply pi N == Q
+Proof
+    rpt STRIP_TAC
+ >> qabbrev_tac ‘M0 = principle_hnf M’
+ >> qabbrev_tac ‘N0 = principle_hnf N’
+ >> qabbrev_tac ‘n = LAMl_size M0’
+ >> qabbrev_tac ‘n' = LAMl_size N0’
+ (* applying separability_lemma0 *)
+ >> ‘n <= n' \/ n' <= n’ by rw []
+ >- METIS_TAC [separability_lemma0]
+ >> MP_TAC (Q.SPECL [‘N’, ‘M’] separability_lemma0)
+ >> RW_TAC std_ss [Once equivalent_comm]
+ >> POP_ASSUM (MP_TAC o Q.SPECL [‘Q’, ‘P’])
+ >> RW_TAC std_ss []
+ >> Q.EXISTS_TAC ‘pi’ >> art []
+QED
+
+(* Lemma 10.4.1 (ii) [1, p.254] *)
+Theorem separability_lemma2 :
+    !M N. solvable M /\ ~equivalent M N ==>
+          !P. ?pi. Boehm_transform pi /\ apply pi M == P /\ ~solvable (apply pi N)
+Proof
+    rpt STRIP_TAC
+ (* applying separability_lemma1, ‘~equivalent M N’ is only used here *)
+ >> Cases_on ‘solvable N’
+ >- (‘!P Q. ?pi. Boehm_transform pi /\ apply pi M == P /\ apply pi N == Q’
+         by METIS_TAC [separability_lemma1] \\
+     POP_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL [‘P’, ‘Omega’])) \\
+     Q.EXISTS_TAC ‘pi’ >> art [] \\
+     METIS_TAC [lameq_solvable_cong, unsolvable_Omega])
+ (* stage work *)
+ >> ‘?M0. M == M0 /\ hnf M0’ by METIS_TAC [has_hnf_def, solvable_iff_has_hnf]
+ >> ‘?vs args y. ALL_DISTINCT vs /\ M0 = LAMl vs (VAR y @* args)’
+       by METIS_TAC [hnf_cases]
+ >> qabbrev_tac ‘as = FRESH_list (LENGTH args) (FV P)’
+ >> qabbrev_tac ‘pi = [LAMl as P/y]::MAP rightctxt (MAP VAR (REVERSE vs))’
+ >> Q.EXISTS_TAC ‘pi’
+ >> STRONG_CONJ_TAC
+ >- rw [Abbr ‘pi’, Boehm_transform_def, EVERY_SNOC, EVERY_MAP]
+ >> DISCH_TAC
+ (* applying Boehm_apply_unsolvable *)
+ >> reverse CONJ_TAC
+ >- (MATCH_MP_TAC Boehm_apply_unsolvable >> art [])
+ (* stage work *)
+ >> MATCH_MP_TAC lameq_TRANS
+ >> Q.EXISTS_TAC ‘apply pi M0’
+ >> CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> art [])
+ >> POP_ASSUM K_TAC (* ‘Boehm_transform pi’ is not needed here *)
+ >> rw [Abbr ‘pi’]
+ >> qabbrev_tac ‘pi :transform = MAP rightctxt (MAP VAR (REVERSE (vs)))’
+ >> qabbrev_tac ‘t = VAR y @* args’
+ (* applying Boehm_apply_MAP_rightctxt *)
+ >> Know ‘apply pi (LAMl vs t) = LAMl vs t @* MAP VAR vs’
+ >- (rw [Abbr ‘pi’, Boehm_apply_MAP_rightctxt] \\
+     rw [MAP_REVERSE, REVERSE_REVERSE])
+ >> Rewr'
+ (* applying lameq_LAMl_appstar_VAR *)
+ >> MATCH_MP_TAC lameq_TRANS
+ >> Q.EXISTS_TAC ‘[LAMl as P/y] t’
+ >> CONJ_TAC
+ >- (irule lameq_sub_cong >> rw [lameq_LAMl_appstar_VAR])
+ >> rw [Abbr ‘t’, appstar_SUB]
+ >> ‘DISJOINT (set as) (FV P) /\ LENGTH as = LENGTH args’
+       by rw [FRESH_list_def, Abbr ‘as’]
+ >> MATCH_MP_TAC lameq_LAMl_appstar_reduce >> rw []
+QED
+
+val _ = export_theory ();
+val _ = html_theory "boehm";
+
+(* References:
+
+   [1] Barendregt, H.P.: The lambda calculus, its syntax and semantics.
+       College Publications, London (1984).
+ *)
diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml
index 0c3704926c..ed908db42a 100644
--- a/examples/lambda/barendregt/chap2Script.sml
+++ b/examples/lambda/barendregt/chap2Script.sml
@@ -218,6 +218,12 @@ val lemma2_13 = store_thm( (* p.20 *)
   POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `c` THEN
   HO_MATCH_MP_TAC ctxt_indn THEN PROVE_TAC [lameq_rules]);
 
+Theorem lameq_LAMl_cong :
+    !vs M N. M == N ==> LAMl vs M == LAMl vs N
+Proof
+    Induct_on ‘vs’ >> rw [lameq_ABS]
+QED
+
 val (lamext_rules, lamext_indn, lamext_cases) = (* p. 21 *)
   Hol_reln`(!x M N. lamext ((LAM x M) @@ N) ([N/x]M)) /\
            (!M. lamext M M) /\
@@ -230,15 +236,24 @@ val (lamext_rules, lamext_indn, lamext_cases) = (* p. 21 *)
                     lamext (M @@ VAR x) (N @@ VAR x) ==>
                     lamext M N)`
 
-val (lameta_rules, lameta_ind, lameta_cases) = (* p. 21 *)
-  Hol_reln`(!x M N. lameta ((LAM x M) @@ N) ([N/x]M)) /\
-           (!M. lameta M M) /\
-           (!M N. lameta M N ==> lameta N M) /\
-           (!M N L. lameta M N /\ lameta N L ==> lameta M L) /\
-           (!M N Z. lameta M N ==> lameta (M @@ Z) (N @@ Z)) /\
-           (!M N Z. lameta M N ==> lameta (Z @@ M) (Z @@ N)) /\
-           (!M N x. lameta M N ==> lameta (LAM x M) (LAM x N)) /\
-           (!M x. ~(x IN FV M) ==> lameta (LAM x (M @@ VAR x)) M)`;
+Inductive lameta : (* p. 21 *)
+[~BETA:]
+  !x M N. lameta ((LAM x M) @@ N) ([N/x]M)
+[~REFL:]
+  !M. lameta M M
+[~SYM:]
+  !M N. lameta M N ==> lameta N M
+[~TRANS:]
+  !M N L. lameta M N /\ lameta N L ==> lameta M L
+[~APPL:]
+  !M N Z. lameta M N ==> lameta (M @@ Z) (N @@ Z)
+[~APPR:]
+  !M N Z. lameta M N ==> lameta (Z @@ M) (Z @@ N)
+[~ABS:]
+  !M N x. lameta M N ==> lameta (LAM x M) (LAM x N)
+[~ETA:]
+  !M x. ~(x IN FV M) ==> lameta (LAM x (M @@ VAR x)) M
+End
 
 val lemma2_14 = store_thm(
   "lemma2_14",
@@ -269,6 +284,20 @@ Definition consistent_def :
     consistent (thy:term -> term -> bool) = ?M N. ~thy M N
 End
 
+Overload inconsistent = “\thy. ~consistent thy”
+
+Theorem inconsistent_def :
+    !thy. inconsistent thy <=> !M N. thy M N
+Proof
+    rw [consistent_def]
+QED
+
+Theorem inconsistent_mono :
+    !t1 t2. t1 RSUBSET t2 /\ inconsistent t1 ==> inconsistent t2
+Proof
+    rw [relationTheory.RSUBSET, inconsistent_def]
+QED
+
 (* This is lambda theories (only having beta equivalence, no eta equivalence)
    extended with extra equations as formulas.
 
@@ -295,6 +324,18 @@ Inductive asmlam :
   !x M M'. asmlam eqns M M' ==> asmlam eqns (LAM x M) (LAM x M')
 End
 
+Theorem asmlam_subst :
+    !M N P x. asmlam eqns M N ==> asmlam eqns ([P/x] M) ([P/x] N)
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC asmlam_trans
+ >> Q.EXISTS_TAC ‘LAM x N @@ P’
+ >> simp [asmlam_rules]
+ >> MATCH_MP_TAC asmlam_trans
+ >> Q.EXISTS_TAC ‘LAM x M @@ P’
+ >> simp [asmlam_rules]
+QED
+
 (* Definition 2.1.32 [1, p.33]
 
    cf. also Definition 2.1.30 (iii): If t is a set of equations, then lambda + t
@@ -621,6 +662,19 @@ Proof
  >> qexistsl_tac [‘v’, ‘t0’] >> REWRITE_TAC []
 QED
 
+Theorem is_abs_cases_genX :
+    !v t. is_abs t /\ v # t <=> ?t0. t = LAM v t0
+Proof
+    rpt GEN_TAC
+ >> reverse EQ_TAC >- (STRIP_TAC >> rw [is_abs_thm])
+ >> rw [is_abs_cases]
+ >> fs [FV_thm]
+ >> Cases_on ‘v = v'’
+ >- (Q.EXISTS_TAC ‘t0’ >> rw [])
+ >> Q.EXISTS_TAC ‘[VAR v/v'] t0’
+ >> MATCH_MP_TAC SIMPLE_ALPHA >> rw []
+QED
+
 Theorem is_abs_appstar[simp]:
   is_abs (M @* Ns) ⇔ is_abs M ∧ (Ns = [])
 Proof
@@ -909,8 +963,8 @@ End
 Definition has_bnf_def: has_bnf t = ?t'. t == t' /\ bnf t'
 End
 
-(* wrong? shouldn't this be ==_eta rather than == ? *)
-val has_benf_def = Define`has_benf t = ?t'. t == t' /\ benf t'`;
+Definition has_benf_def: has_benf t = ?t'. lameta t t' /\ benf t'
+End
 
 Theorem fresh_ssub:
   ∀N. y ∉ FV N ∧ (∀k:string. k ∈ FDOM fm ⇒ y # fm ' k) ⇒ y # fm ' N
@@ -947,6 +1001,42 @@ Proof
   Induct_on ‘Ns’ using SNOC_INDUCT >> rw [appstar_SNOC, lameq_APPL]
 QED
 
+Theorem lameq_LAMl_appstar_VAR[simp] :
+    !xs. LAMl xs t @* (MAP VAR xs) == t
+Proof
+    Induct_on ‘xs’ >> rw []
+ >> qabbrev_tac ‘M = LAMl xs t’
+ >> qabbrev_tac ‘args :term list = MAP VAR xs’
+ >> MATCH_MP_TAC lameq_TRANS
+ >> Q.EXISTS_TAC ‘M @* args’ >> art []
+ >> MATCH_MP_TAC lameq_appstar_cong
+ >> rw [Once lameq_cases]
+ >> DISJ1_TAC >> qexistsl_tac [‘h’, ‘M’] >> rw []
+QED
+
+Theorem lameq_LAMl_appstar_reduce :
+    !xs t args. DISJOINT (set xs) (FV t) /\ LENGTH xs = LENGTH args ==>
+                LAMl xs t @* args == t
+Proof
+    Induct_on ‘xs’ >> rw []
+ >> Cases_on ‘args’ >- fs []
+ >> rw [GSYM appstar_CONS]
+ >> qabbrev_tac ‘M = LAMl xs t’
+ >> MATCH_MP_TAC lameq_TRANS
+ >> Q.EXISTS_TAC ‘M @* t'’
+ >> reverse CONJ_TAC
+ >- (qunabbrev_tac ‘M’ \\
+     FIRST_X_ASSUM MATCH_MP_TAC >> fs [])
+ >> MATCH_MP_TAC lameq_appstar_cong
+ >> rw [Once lameq_cases] >> DISJ1_TAC
+ >> qexistsl_tac [‘h’, ‘M’] >> art []
+ >> MATCH_MP_TAC (GSYM lemma14b)
+ >> rw [Abbr ‘M’, FV_LAMl]
+QED
+
+(* NOTE: The antecedents ‘EVERY closed Ns’ is just one way to make sure that
+   the order of ‘vs’ makes no difference in the substitution results.
+ *)
 Theorem lameq_LAMl_appstar :
     !vs M Ns. ALL_DISTINCT vs /\ (LENGTH vs = LENGTH Ns) /\ EVERY closed Ns ==>
               LAMl vs M @* Ns == (FEMPTY |++ ZIP (vs,Ns)) ' M
diff --git a/examples/lambda/barendregt/chap3Script.sml b/examples/lambda/barendregt/chap3Script.sml
index 591eaada22..cf0c0f1d50 100644
--- a/examples/lambda/barendregt/chap3Script.sml
+++ b/examples/lambda/barendregt/chap3Script.sml
@@ -309,13 +309,19 @@ val bvc_cases = store_thm(
   Q_TAC (NEW_TAC "z") `v INSERT X UNION FV t0` THEN
   METIS_TAC []);
 
-val (grandbeta_rules, grandbeta_ind, grandbeta_cases) =
-    Hol_reln`(!M. grandbeta M M) /\
-             (!M M' x. grandbeta M M' ==> grandbeta (LAM x M) (LAM x M')) /\
-             (!M N M' N'. grandbeta M M' /\ grandbeta N N' ==>
-                          grandbeta (M @@ N) (M' @@ N')) /\
-             (!M N M' N' x. grandbeta M M' /\ grandbeta N N' ==>
-                            grandbeta ((LAM x M) @@ N) ([N'/x] M'))`;
+(* Definition 3.2.3 [1, p60] (one-step parallel beta-reduction) *)
+Inductive grandbeta :
+[~REFL:]
+  !M. grandbeta M M
+[~ABS:]
+  !M M' x. grandbeta M M' ==> grandbeta (LAM x M) (LAM x M')
+[~APP:]
+  !M N M' N'. grandbeta M M' /\ grandbeta N N' ==> grandbeta (M @@ N) (M' @@ N')
+[~BETA:]
+  !M N M' N' x. grandbeta M M' /\ grandbeta N N' ==>
+                grandbeta ((LAM x M) @@ N) ([N'/x] M')
+End
+
 val _ = set_fixity "=b=>" (Infix(NONASSOC,450))
 val _ = overload_on ("=b=>", ``grandbeta``)
 val _ = set_fixity "=b=>*" (Infix(NONASSOC,450))
diff --git a/examples/lambda/barendregt/head_reductionScript.sml b/examples/lambda/barendregt/head_reductionScript.sml
index 17e3c4ee28..0124e26574 100644
--- a/examples/lambda/barendregt/head_reductionScript.sml
+++ b/examples/lambda/barendregt/head_reductionScript.sml
@@ -1,7 +1,8 @@
 open HolKernel Parse boolLib bossLib BasicProvers;
 
 open boolSimps relationTheory pred_setTheory listTheory finite_mapTheory
-     arithmeticTheory llistTheory pathTheory optionTheory hurdUtils;
+     arithmeticTheory llistTheory pathTheory optionTheory rich_listTheory
+     hurdUtils;
 
 open termTheory appFOLDLTheory chap2Theory chap3Theory nomsetTheory binderLib
      horeductionTheory term_posnsTheory finite_developmentsTheory;
@@ -1161,6 +1162,211 @@ Proof
  >> simp []
 QED
 
+(* cf. Omega_starloops *)
+Theorem Omega_hreduce1_loops :
+    Omega -h-> N <=> (N = Omega)
+Proof
+    rw [hreduce1_rwts, Omega_def]
+QED
+
+(*---------------------------------------------------------------------------*
+ *  Accessors of hnf components
+ *---------------------------------------------------------------------------*)
+
+Definition hnf_head_def :
+    hnf_head t = if is_comb t then hnf_head (rator t) else t
+Termination
+    WF_REL_TAC ‘measure size’
+ >> rw [is_comb_APP_EXISTS] >> rw []
+End
+
+Theorem hnf_head_appstar :
+    !t. ~is_comb t ==> (hnf_head (t @* args) = t)
+Proof
+    Induct_on ‘args’ using SNOC_INDUCT
+ >> rw [appstar_SNOC, Once hnf_head_def, FOLDL]
+QED
+
+Theorem hnf_head_hnf[simp] :
+    (hnf_head (VAR y @@ t) = VAR y) /\
+    (hnf_head (VAR y @* args) = VAR y)
+Proof
+    CONJ_TAC
+ >- NTAC 2 (rw [Once hnf_head_def])
+ >> MATCH_MP_TAC hnf_head_appstar
+ >> rw []
+QED
+
+Overload hnf_headvar = “\t. THE_VAR (hnf_head t)”
+
+(* hnf_children retrives the ‘args’ part of an abs-free hnf (VAR y @* args) *)
+Definition hnf_children_def :
+    hnf_children t = if is_comb t then
+                        SNOC (rand t) (hnf_children (rator t))
+                     else []
+Termination
+    WF_REL_TAC ‘measure size’ >> rw [is_comb_APP_EXISTS] >> rw []
+End
+
+Theorem hnf_children_thm :
+   (!y.     hnf_children ((VAR :string -> term) y) = []) /\
+   (!v t.   hnf_children (LAM v t) = []) /\
+   (!t1 t2. hnf_children (t1 @@ t2) = SNOC t2 (hnf_children t1))
+Proof
+   rpt (rw [Once hnf_children_def])
+QED
+
+Theorem hnf_children_appstar :
+    !t. ~is_comb t ==> (hnf_children (t @* args) = args)
+Proof
+    Induct_on ‘args’ using SNOC_INDUCT
+ >- rw [Once hnf_children_def, FOLDL]
+ >> RW_TAC std_ss [appstar_SNOC]
+ >> rw [Once hnf_children_def]
+QED
+
+Theorem hnf_children_hnf :
+    !y args. hnf_children (VAR y @* args) = args
+Proof
+    rpt GEN_TAC
+ >> MATCH_MP_TAC hnf_children_appstar >> rw []
+QED
+
+Theorem absfree_hnf_cases :
+    !M. hnf M /\ ~is_abs M <=> ?y args. M = VAR y @* args
+Proof
+    Q.X_GEN_TAC ‘M’
+ >> EQ_TAC
+ >- (STRIP_TAC \\
+    ‘?vs args y. ALL_DISTINCT vs /\ (M = LAMl vs (VAR y @* args))’
+        by METIS_TAC [hnf_cases] \\
+     reverse (Cases_on ‘vs = []’) >- fs [] \\
+     qexistsl_tac [‘y’, ‘args’] >> rw [LAMl_thm])
+ >> rpt STRIP_TAC
+ >- rw [hnf_appstar]
+ >> rfs [is_abs_cases]
+QED
+
+Theorem absfree_hnf_thm :
+    !M. hnf M /\ ~is_abs M ==> (M = hnf_head M @* hnf_children M)
+Proof
+    rw [absfree_hnf_cases]
+ >> rw [hnf_children_appstar, hnf_head_appstar]
+QED
+
+Theorem hnf_head_absfree :
+    !y args. hnf_head (VAR y @* args) = VAR y
+Proof
+    rpt GEN_TAC
+ >> MATCH_MP_TAC hnf_head_appstar >> rw []
+QED
+
+Theorem lameq_hnf_fresh_subst :
+    !as args P. (LENGTH args = LENGTH as) /\ DISJOINT (set as) (FV P) ==>
+                ([LAMl as P/y] (VAR y @* args) == P)
+Proof
+    Induct_on ‘as’ using SNOC_INDUCT >> rw []
+ >> Cases_on ‘args = []’ >- fs []
+ >> ‘args = SNOC (LAST args) (FRONT args)’ by PROVE_TAC [SNOC_LAST_FRONT]
+ >> POP_ORW
+ >> REWRITE_TAC [appstar_SNOC, SUB_THM]
+ >> MATCH_MP_TAC lameq_TRANS
+ >> qabbrev_tac ‘M = [LAMl as (LAM x P)/y] (LAST args)’
+ >> Q.EXISTS_TAC ‘LAM x P @@ M’
+ >> CONJ_TAC
+ >- (MATCH_MP_TAC lameq_APPL \\
+     FIRST_X_ASSUM MATCH_MP_TAC >> rw [FV_thm, LENGTH_FRONT] \\
+     Q.PAT_X_ASSUM ‘DISJOINT _ _’ MP_TAC \\
+     rw [DISJOINT_ALT])
+ >> rw [Once lameq_cases] >> DISJ1_TAC
+ >> qexistsl_tac [‘x’, ‘P’] >> art []
+ >> MATCH_MP_TAC (GSYM lemma14b)
+ >> Q.PAT_X_ASSUM ‘DISJOINT _ _’ MP_TAC
+ >> rw [DISJOINT_ALT]
+QED
+
+(*---------------------------------------------------------------------------*
+ *  LAMl_size (of hnf)
+ *---------------------------------------------------------------------------*)
+
+val (LAMl_size_thm, _) = define_recursive_term_function
+   ‘(LAMl_size ((VAR :string -> term) s) = 0) /\
+    (LAMl_size (t1 @@ t2) = 0) /\
+    (LAMl_size (LAM v t) = 1 + LAMl_size t)’;
+
+val _ = export_rewrites ["LAMl_size_thm"];
+
+Theorem LAMl_size_0_cases :
+    !t. is_var t \/ is_comb t ==> (LAMl_size t = 0)
+Proof
+    rw [is_var_cases, is_comb_APP_EXISTS]
+ >> rw []
+QED
+
+Theorem LAMl_size_0_cases' :
+    !t. ~is_abs t ==> (LAMl_size t = 0)
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC LAMl_size_0_cases
+ >> METIS_TAC [term_cases]
+QED
+
+Theorem LAMl_size_LAMl :
+    !vs t. ~is_abs t ==> (LAMl_size (LAMl vs t) = LENGTH vs)
+Proof
+    rpt STRIP_TAC
+ >> Induct_on ‘vs’
+ >- rw [LAMl_size_0_cases']
+ >> rw []
+QED
+
+Theorem LAMl_size_hnf :
+    !vs y args. LAMl_size (LAMl vs (VAR y @* args)) = LENGTH vs
+Proof
+    rpt GEN_TAC
+ >> MATCH_MP_TAC LAMl_size_LAMl
+ >> Cases_on ‘args = []’ >- rw []
+ >> ‘?x l. args = SNOC x l’ by METIS_TAC [SNOC_CASES]
+ >> rw [appstar_SNOC]
+QED
+
+(* Another variant of ‘hnf_cases’ with a given (shared) list of fresh variables
+
+   NOTE: "irule (iffLR hnf_cases_shared)" is a useful tactic for this theorem.
+ *)
+Theorem hnf_cases_shared :
+    !vs M. ALL_DISTINCT vs /\ LAMl_size M <= LENGTH vs /\
+           DISJOINT (set vs) (FV M) ==>
+          (hnf M <=> ?y args. (M = LAMl (TAKE (LAMl_size M) vs) (VAR y @* args)))
+Proof
+    rpt STRIP_TAC
+ >> reverse EQ_TAC
+ >- (STRIP_TAC >> POP_ORW \\
+     rw [hnf_appstar, hnf_LAMl])
+ >> rpt (POP_ASSUM MP_TAC)
+ >> Q.ID_SPEC_TAC ‘M’
+ >> Induct_on ‘vs’
+ >- (rw [] \\
+    ‘?vs args y. M = LAMl vs (VAR y @* args)’ by METIS_TAC [hnf_cases] \\
+     fs [LAMl_size_hnf])
+ (* stage work *)
+ >> rw [LIST_TO_SET_SNOC, ALL_DISTINCT_SNOC]
+ >> fs []
+ >> Cases_on ‘LAMl_size M = 0’
+ >- (fs [] \\
+     Q.PAT_X_ASSUM ‘!M. P’ (MP_TAC o (Q.SPEC ‘M’)) >> rw [])
+ >> ‘is_abs M’ by METIS_TAC [LAMl_size_0_cases']
+ (* applying is_abs_cases_genX *)
+ >> ‘?t0. M = LAM h t0’ by METIS_TAC [is_abs_cases_genX]
+ >> FIRST_X_ASSUM (MP_TAC o (Q.SPEC ‘t0’))
+ >> ‘hnf t0’ by METIS_TAC [hnf_thm]
+ >> fs [LAMl_size_hnf]
+ >> Suff ‘DISJOINT (set vs) (FV t0)’ >- rw []
+ >> Q.PAT_X_ASSUM ‘DISJOINT _ _’ MP_TAC
+ >> rw [DISJOINT_ALT]
+ >> METIS_TAC []
+QED
+
 val _ = export_theory()
 val _ = html_theory "head_reduction";
 
diff --git a/examples/lambda/barendregt/horeductionScript.sml b/examples/lambda/barendregt/horeductionScript.sml
index 5c526f7b00..7fa02060ae 100644
--- a/examples/lambda/barendregt/horeductionScript.sml
+++ b/examples/lambda/barendregt/horeductionScript.sml
@@ -179,6 +179,9 @@ Proof
   ]
 QED
 
+(* |- !R x y z. conversion R x y /\ conversion R y z ==> conversion R x z *)
+Theorem conversion_TRANS = cj 3 conversion_rules
+
 Theorem compat_closure_compatible:
   !R. compatible (compat_closure R)
 Proof
@@ -234,6 +237,33 @@ val conversion_compatible = store_thm(
   HO_MATCH_MP_TAC equiv_closure_ind THEN SRW_TAC [][] THEN
   PROVE_TAC [compatible_def, equiv_closure_rules, compat_closure_compatible]);
 
+Theorem conversion_monotone :
+    !r1 r2. r1 RSUBSET r2 ==> (conversion r1) RSUBSET (conversion r2)
+Proof
+    rpt STRIP_TAC
+ >> simp [relationTheory.RSUBSET]
+ >> HO_MATCH_MP_TAC relationTheory.EQC_INDUCTION
+ >> reverse (rw [conversion_rules])
+ >- (MATCH_MP_TAC EQC_TRANS \\
+     rename1 ‘conversion r2 z y’ \\
+     Q.EXISTS_TAC ‘z’ >> ASM_REWRITE_TAC [])
+ >> POP_ASSUM MP_TAC
+ >> Q.ID_SPEC_TAC ‘y’
+ >> Q.ID_SPEC_TAC ‘x’
+ >> HO_MATCH_MP_TAC compat_closure_ind
+ >> RW_TAC std_ss []
+ >| [ (* goal 1 (of 4) *)
+      Q_TAC SUFF_TAC ‘r2 x y’ >- rw [conversion_rules] \\
+      Q.PAT_X_ASSUM ‘r1 RSUBSET r2’ MP_TAC \\
+      rw [relationTheory.RSUBSET],
+      (* goal 2 (of 4) *)
+      PROVE_TAC [conversion_compatible, compatible_def, leftctxt],
+      (* goal 3 (of 4) *)
+      PROVE_TAC [conversion_compatible, compatible_def, rightctxt, rightctxt_thm],
+      (* goal 7 (of 7) *)
+      PROVE_TAC [conversion_compatible, compatible_def, absctxt] ]
+QED
+
 (* "Follows from an induction on the structure of M, and the
     compatibility of reduction R" *)
 val lemma3_8 = store_thm(
diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml
index b940323a6d..fc32688d90 100644
--- a/examples/lambda/barendregt/solvableScript.sml
+++ b/examples/lambda/barendregt/solvableScript.sml
@@ -94,7 +94,7 @@ Theorem solvable_alt_closed'[local] =
     REWRITE_RULE [closed_def] solvable_alt_closed
 
 (* 8.3.1 (iii) [1, p.171] *)
-Overload unsolvable = “\M. ~(solvable M)”
+Overload unsolvable = “\M. ~solvable M”
 
 (* 8.3.2 Examples of solvable terms [1, p.171] *)
 Theorem solvable_K :
@@ -606,6 +606,12 @@ Proof
         Q.EXISTS_TAC ‘fm’ >> simp [] ] ]
 QED
 
+Theorem solvable_iff_LAMl[simp] :
+    !vs M. solvable (LAMl vs M) <=> solvable M
+Proof
+    Induct_on ‘vs’ >> rw [solvable_iff_LAM]
+QED
+
 (* Theorem 8.3.14 (Wadsworth) [1, p.175] *)
 Theorem solvable_iff_has_hnf :
     !M. solvable M <=> has_hnf M
@@ -616,9 +622,9 @@ Proof
  >> ‘closed M0’
        by (rw [closed_def, Abbr ‘M0’, Abbr ‘vs’, FV_LAMl, SET_TO_LIST_INV])
  >> Suff ‘solvable M0 <=> has_hnf M0’
- >- (Q.UNABBREV_TAC ‘M0’ \\
-     KILL_TAC >> Induct_on ‘vs’ >- rw [] \\
-     rw [solvable_iff_LAM, has_hnf_LAM_E])
+ >- (‘solvable M <=> solvable M0’ by rw [Abbr ‘M0’, solvable_iff_LAMl] \\
+     POP_ORW >> Rewr' \\
+     rw [Abbr ‘M0’, has_hnf_LAMl_E])
  >> POP_ASSUM MP_TAC >> KILL_TAC
  >> Q.SPEC_TAC (‘M0’, ‘M’)
  (* stage work, now M is closed *)
@@ -721,7 +727,7 @@ QED
 Theorem hnf_principle_hnf' =
    REWRITE_RULE [GSYM solvable_iff_has_hnf] hnf_principle_hnf
 
-Theorem principle_hnf_eq_self :
+Theorem principle_hnf_eq_self[simp] :
     !M. hnf M ==> principle_hnf M = M
 Proof
     rw [principle_hnf_def]
@@ -868,8 +874,8 @@ QED
 
    NOTE: to satisfy ‘DISJOINT (set xs) (set ys)’, one first get ‘LENGTH xs’
          without knowing ‘xs’ (e.g. by ‘LAMl_size’), then generate ‘ys’ by
-        ‘FRESH_list’, and then call ‘hnf_cases’ (more general version) using ‘ys’
-         as the excluded list.
+        ‘FRESH_list’, and then call ‘hnf_cases_genX’ using ‘ys’ as the excluded
+         list.
  *)
 Theorem principle_hnf_LAMl_appstar :
     !t xs ys. hnf t /\
@@ -895,6 +901,37 @@ Proof
  >> MATCH_MP_TAC principle_hnf_LAMl_appstar_lemma >> rw []
 QED
 
+Theorem principle_hnf_reduce1 :
+    !v t. hnf t ==> principle_hnf (LAM v t @@ VAR v) = t
+Proof
+    rpt STRIP_TAC
+ >> Know ‘principle_hnf (LAM v t @@ VAR v) =
+          principle_hnf ([VAR v/v] t)’
+ >- (MATCH_MP_TAC principle_hnf_hreduce1 \\
+     rw [Once hreduce1_cases] \\
+     qexistsl_tac [‘v’, ‘t’] >> rw [])
+ >> Rewr'
+ >> rw [principle_hnf_eq_self]
+QED
+
+Theorem principle_hnf_reduce :
+    !xs t. hnf t ==> principle_hnf (LAMl xs t @* (MAP VAR xs)) = t
+Proof
+    Induct_on ‘xs’
+ >- rw [principle_hnf_eq_self]
+ >> rw []
+ >> qabbrev_tac ‘M = LAMl xs t’
+ >> qabbrev_tac ‘args :term list = MAP VAR xs’
+ >> Know ‘principle_hnf (LAM h M @@ VAR h @* args) =
+          principle_hnf ([VAR h/h] M @* args)’
+ >- (MATCH_MP_TAC principle_hnf_hreduce1 \\
+     MATCH_MP_TAC hreduce1_rules_appstar >> simp [] \\
+     rw [Once hreduce1_cases] \\
+     qexistsl_tac [‘h’, ‘M’] >> rw [])
+ >> Rewr'
+ >> simp [Abbr ‘M’]
+QED
+
 (* Example 8.3.2 [1, p.171] *)
 Theorem unsolvable_Omega :
     unsolvable Omega
@@ -911,6 +948,82 @@ Proof
  >> rw [Omega_def, I_def]
 QED
 
+(* Another proof based on solvable_iff_has_hnf, told by Michael Norrish *)
+Theorem unsolvable_Omega' :
+    unsolvable Omega
+Proof
+    rw [solvable_iff_has_hnf, corollary11_4_8]
+ >> ‘?r. r is_head_redex Omega /\ labelled_redn beta Omega r Omega’
+       by (rw [GSYM head_reduce1_def, Omega_hreduce1_loops])
+ >> qabbrev_tac ‘p = pgenerate (\n. Omega) (\n. r)’
+ >> ‘infinite p’ by rw [Abbr ‘p’, pgenerate_infinite]
+ >> ‘tail p = p’ by rw [Abbr ‘p’, Once pgenerate_def, tail_def, combinTheory.o_DEF]
+ >> Suff ‘head_reduction_path Omega = p’ >- (Rewr' >> art [])
+ >> MATCH_MP_TAC head_reduction_path_unique
+ >> simp []
+ >> CONJ_TAC >- rw [Abbr ‘p’, Once pgenerate_def]
+ (* is_head_reduction p *)
+ >> irule is_head_reduction_coind
+ >> Q.EXISTS_TAC ‘\p. first p = Omega /\ first_label p = r /\ tail p = p’
+ >> simp []
+ >> CONJ_TAC >- (STRIP_TAC >> rw [Abbr ‘p’, Once pgenerate_def])
+ >> RW_TAC std_ss [] (* 4 subgoals *)
+ >| [ POP_ORW >> simp [first_thm],
+      POP_ORW >> simp [first_thm],
+      POP_ORW >> simp [first_label_def],
+      METIS_TAC [tail_def] ]
+QED
+
+Theorem lameq_solvable_cong_lemma[local] :
+    !M N. closed M /\ closed N /\ M == N ==> (solvable M <=> solvable N)
+Proof
+    Suff ‘!M N. closed M /\ closed N /\ M == N /\ solvable M ==> solvable N’
+ >- METIS_TAC [lameq_SYM]
+ >> rw [solvable_alt_closed]
+ >> gs [solvable_alt_closed]
+ >> Q.EXISTS_TAC ‘Ns’
+ >> MATCH_MP_TAC lameq_TRANS
+ >> Q.EXISTS_TAC ‘M @* Ns’ >> art []
+ >> MATCH_MP_TAC lameq_appstar_cong
+ >> rw [lameq_SYM]
+QED
+
+Theorem lameq_solvable_cong :
+    !M N. M == N ==> (solvable M <=> solvable N)
+Proof
+    rpt STRIP_TAC
+ >> qabbrev_tac ‘vs = SET_TO_LIST (FV M UNION FV N)’
+ >> qabbrev_tac ‘M0 = LAMl vs M’
+ >> qabbrev_tac ‘N0 = LAMl vs N’
+ >> Know ‘closed M0 /\ closed N0’
+ >- (rw [closed_def, Abbr ‘M0’, Abbr ‘N0’, Abbr ‘vs’, FV_LAMl] \\
+    ‘FINITE (FV M UNION FV N)’ by rw [] \\
+     simp [SET_TO_LIST_INV] >> SET_TAC [])
+ >> STRIP_TAC
+ >> ‘solvable M <=> solvable M0’ by (rw [Abbr ‘M0’]) >> POP_ORW
+ >> ‘solvable N <=> solvable N0’ by (rw [Abbr ‘N0’]) >> POP_ORW
+ >> ‘M0 == N0’ by (rw [Abbr ‘M0’, Abbr ‘N0’, lameq_LAMl_cong])
+ >> MATCH_MP_TAC lameq_solvable_cong_lemma >> art []
+QED
+
+Theorem lameq_principle_hnf :
+    !M. has_hnf M ==> principle_hnf M == M
+Proof
+    rpt STRIP_TAC
+ >> qabbrev_tac ‘N = principle_hnf M’
+ >> Know ‘M head_reduces N’
+ >- (rw [head_reduces_def] \\
+     Q.EXISTS_TAC ‘head_reduction_path M’ \\
+     fs [corollary11_4_8, head_reduction_path_def] \\
+     rw [Abbr ‘N’, principle_hnf_def])
+ >> rw [head_reduces_RTC_hreduce1]
+ >> MATCH_MP_TAC lameq_SYM
+ >> MATCH_MP_TAC hreduces_lameq >> art []
+QED
+
+Theorem lameq_principle_hnf' =
+        REWRITE_RULE [GSYM solvable_iff_has_hnf] lameq_principle_hnf
+
 val _ = export_theory ();
 val _ = html_theory "solvable";
 
diff --git a/examples/lambda/barendregt/standardisationScript.sml b/examples/lambda/barendregt/standardisationScript.sml
index 39aac02e5a..3e5d97cd79 100644
--- a/examples/lambda/barendregt/standardisationScript.sml
+++ b/examples/lambda/barendregt/standardisationScript.sml
@@ -995,18 +995,6 @@ val i_reduce_to_LAM_underneath = prove(
     PROVE_TAC [labelled_redn_rules]
   ]);
 
-val FRESH_lists = store_thm(
-  "FRESH_lists",
-  ``!n s : string set.
-       FINITE s ==> ?l'. ALL_DISTINCT l' /\ DISJOINT (LIST_TO_SET l') s /\
-                         (LENGTH l' = n)``,
-  Induct THEN SRW_TAC [][] THENL [
-    RES_TAC THEN
-    Q_TAC (NEW_TAC "z") `LIST_TO_SET l' UNION s` THEN
-    Q.EXISTS_TAC `z::l'` THEN
-    FULL_SIMP_TAC (srw_ss()) []
-  ]);
-
 val _ = augment_srw_ss [rewrites [RENAMING_REVERSE, RENAMING_ZIP_MAP_VAR]]
 
 val head_reduction_standard = store_thm(
@@ -1829,6 +1817,12 @@ Proof
  >> MATCH_MP_TAC betastar_lameq >> art []
 QED
 
+Theorem has_hnf_LAMl_E[simp] :
+    !vs M. has_hnf (LAMl vs M) <=> has_hnf M
+Proof
+    Induct_on ‘vs’ >> rw []
+QED
+
 (* Proposition 8.3.13 (ii) [1, p.174] *)
 Theorem has_hnf_SUB_E :
     !M N z. has_hnf ([N/z] M) ==> has_hnf M
diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml
index 1b359129a8..75cf17543a 100644
--- a/examples/lambda/basics/appFOLDLScript.sml
+++ b/examples/lambda/basics/appFOLDLScript.sml
@@ -1,6 +1,6 @@
 open HolKernel Parse boolLib bossLib;
 
-open arithmeticTheory listTheory pred_setTheory hurdUtils;
+open arithmeticTheory listTheory rich_listTheory pred_setTheory hurdUtils;
 
 open termTheory binderLib;
 
@@ -11,6 +11,20 @@ val _ = Unicode.unicode_version { u = "··", tmnm = "@*"}
 
 Overload "@*" = “\f (args:term list). FOLDL APP f args”
 
+Theorem appstar_empty[simp] :
+    M @* [] = M
+Proof
+    rw [FOLDL]
+QED
+
+(* NOTE: no more [simp] for this theorem *)
+Theorem appstar_thm :
+    (M @* [] = M) /\
+    (M @* (h::t) = M @@ h @* t)
+Proof
+    rw [FOLDL]
+QED
+
 Theorem var_eq_appstar[simp]:
   VAR s = f ·· args ⇔ args = [] ∧ f = VAR s
 Proof
@@ -163,6 +177,13 @@ Proof
     Induct_on ‘Ns’ using SNOC_INDUCT >> simp[appstar_SNOC, MAP_SNOC]
 QED
 
+Theorem appstar_SUB :
+    !args. [N/v] (t @* args) = [N/v] t @* MAP [N/v] args
+Proof
+    Induct_on ‘args’ using SNOC_INDUCT
+ >> rw [appstar_SNOC, MAP_SNOC]
+QED
+
 Theorem FV_appstar :
     !M Ns. FV (M @* Ns) = FV M UNION (BIGUNION (IMAGE FV (set Ns)))
 Proof
@@ -305,6 +326,12 @@ Proof
   ]
 QED
 
+Theorem LAMl_SNOC[simp] :
+    LAMl (SNOC v vs) t = LAMl vs (LAM v t)
+Proof
+    rw [FOLDR_SNOC]
+QED
+
 (*---------------------------------------------------------------------------*
  *  funpow for lambda terms (using arithmeticTheory.FUNPOW)
  *---------------------------------------------------------------------------*)
diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml
index b9443c1ea5..79aa8c4b04 100644
--- a/examples/lambda/basics/termScript.sml
+++ b/examples/lambda/basics/termScript.sml
@@ -313,6 +313,30 @@ Theorem FRESH_LAM[simp]:
   u NOTIN FV (LAM v M) <=> (u <> v ==> u NOTIN FV M)
 Proof SRW_TAC [][] THEN METIS_TAC []
 QED
+
+(* NOTE: this theorem doesn't really belong here but moving it to basic_swapTheory
+         seems unnecessary (and NEW_TAC is not available).
+ *)
+Theorem FRESH_lists :
+    !n s : string set.
+       FINITE s ==> ?l'. ALL_DISTINCT l' /\ DISJOINT (LIST_TO_SET l') s /\
+                         (LENGTH l' = n)
+Proof
+  Induct THEN SRW_TAC [][] THENL [
+    RES_TAC THEN
+    Q_TAC (NEW_TAC "z") `LIST_TO_SET l' UNION s` THEN
+    Q.EXISTS_TAC `z::l'` THEN
+    FULL_SIMP_TAC (srw_ss()) []
+  ]
+QED
+
+(* ‘FRESH_list’ is a function for generating fresh list of new variables *)
+local
+    val th = SIMP_RULE std_ss [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] FRESH_lists
+in
+    val FRESH_list_def = new_specification ("FRESH_list_def", ["FRESH_list"], th)
+end
+
 val FV_EMPTY = store_thm(
   "FV_EMPTY",
   ``(FV t = {}) <=> !v. v NOTIN FV t``,
diff --git a/examples/lambda/completeness/boehm_treeScript.sml b/examples/lambda/completeness/boehm_treeScript.sml
index 3df6b3789d..c3af83eb44 100644
--- a/examples/lambda/completeness/boehm_treeScript.sml
+++ b/examples/lambda/completeness/boehm_treeScript.sml
@@ -5,18 +5,21 @@
 open HolKernel boolLib Parse bossLib;
 
 (* core theories *)
-open optionTheory arithmeticTheory pred_setTheory listTheory llistTheory
-     ltreeTheory pathTheory posetTheory hurdUtils rich_listTheory;
+open optionTheory arithmeticTheory pred_setTheory listTheory rich_listTheory
+     llistTheory relationTheory ltreeTheory pathTheory posetTheory hurdUtils;
 
-open binderLib termTheory appFOLDLTheory chap2Theory chap3Theory
-     head_reductionTheory standardisationTheory solvableTheory pure_dBTheory;
+open basic_swapTheory binderLib termTheory appFOLDLTheory chap2Theory
+     chap3Theory head_reductionTheory standardisationTheory solvableTheory;
+
+open pure_dBTheory;
 
 val _ = new_theory "boehm_tree";
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"];
 val o_DEF = combinTheory.o_DEF; (* cannot directly open combinTheory *)
 
 (* A dB-term M is hnf if its corresponding Lambda term is hnf *)
-Overload dhnf = “hnf o toTerm”
+Overload dhnf = “\M. hnf (toTerm M)”
 
 Theorem dhnf_fromTerm[simp] :
     !M. dhnf (fromTerm M) <=> hnf M
@@ -24,158 +27,6 @@ Proof
     rw [o_DEF]
 QED
 
-(* Translations from dLAMl to dABSi.
-
-   Some samples for guessing out the statements of this theorem:
-
-> SIMP_CONV arith_ss [dLAM_def, lift_def, sub_def, lift_sub]
-                     “dLAM v1 (dLAM v0 t)”;
-# val it =
-   |- dLAM v1 (dLAM v0 t) =
-      dABS (dABS ([dV 1/v1 + 2] ([dV 0/v0 + 2] (lift (lift t 0) 1)))): thm
-
-> SIMP_CONV arith_ss [dLAM_def, lift_def, sub_def, lift_sub]
-                     “dLAM v2 (dLAM v1 (dLAM v0 t))”;
-# val it =
-   |- dLAM v2 (dLAM v1 (dLAM v0 t)) =
-      dABS
-        (dABS
-           (dABS ([dV 2/v2 + 3]
-                    ([dV 1/v1 + 3]
-                       ([dV 0/v0 + 3]
-                          (lift (lift (lift t 0) 1) 2)))))): thm
- *)
-Theorem dLAMl_to_dABSi :
-    !vs. ALL_DISTINCT (vs :num list) ==>
-         let n = LENGTH vs;
-             body = FOLDL lift t (GENLIST I n);
-             phi = ZIP (GENLIST dV n, MAP (\i. i + n) (REVERSE vs))
-         in dLAMl vs t = dABSi n (body ISUB phi)
-Proof
-    Induct_on ‘vs’ >- rw [isub_def]
- >> rw [isub_def, GSYM SNOC_APPEND, MAP_SNOC, FUNPOW_SUC, GENLIST, FOLDL_SNOC,
-        dLAM_def]
- >> fs []
- >> qabbrev_tac ‘n = LENGTH vs’
- >> rw [lift_dABSi]
- >> Q.PAT_X_ASSUM ‘dLAMl vs t = _’ K_TAC
- >> qabbrev_tac ‘N = FOLDL lift t (GENLIST I n)’
- >> qabbrev_tac ‘Ms = GENLIST dV n’
- >> qabbrev_tac ‘Vs = MAP (\i. i + n) (REVERSE vs)’
- >> Know ‘lift (N ISUB ZIP (Ms,Vs)) n =
-          (lift N n) ISUB (ZIP (MAP (\e. lift e n) Ms,MAP SUC Vs))’
- >- (MATCH_MP_TAC lift_isub \\
-     rw [Abbr ‘Ms’, Abbr ‘Vs’, EVERY_MEM, MEM_MAP] >> rw [])
- >> Rewr'
- >> ‘MAP SUC Vs = MAP (\i. i + SUC n) (REVERSE vs)’
-       by (rw [LIST_EQ_REWRITE, EL_MAP, Abbr ‘Vs’]) >> POP_ORW
- >> qunabbrev_tac ‘Vs’ (* now useless *)
- >> rw [sub_def, GSYM ADD1]
- >> ‘MAP (\e. lift e n) Ms = Ms’
-       by (rw [LIST_EQ_REWRITE, EL_MAP, Abbr ‘Ms’]) >> POP_ORW
- >> qabbrev_tac ‘Ns = MAP (\i. i + SUC n) (REVERSE vs)’
- >> qabbrev_tac ‘N' = lift N n’
- >> Suff ‘N' ISUB ZIP (SNOC (dV n) Ms,SNOC (h + SUC n) Ns) =
-          [dV n/h + SUC n] (N' ISUB ZIP (Ms,Ns))’ >- rw []
- >> MATCH_MP_TAC isub_SNOC
- >> rw [Abbr ‘Ms’, Abbr ‘Ns’, MEM_EL, EL_MAP]
- >> rename1 ‘~(i < n)’
- >> ‘LENGTH (REVERSE vs) = n’ by rw [Abbr ‘n’]
- >> CCONTR_TAC >> gs [EL_MAP]
- >> ‘h = EL i (REVERSE vs)’ by rw []
- >> Suff ‘MEM h (REVERSE vs)’ >- rw [MEM_REVERSE]
- >> Q.PAT_X_ASSUM ‘~MEM h vs’ K_TAC
- >> ‘LENGTH (REVERSE vs) = n’ by rw [Abbr ‘n’]
- >> REWRITE_TAC [MEM_EL]
- >> Q.EXISTS_TAC ‘i’ >> art []
-QED
-
-(* |- !t vs.
-        ALL_DISTINCT vs ==>
-        dLAMl vs t =
-        dABSi (LENGTH vs)
-          (FOLDL lift t (GENLIST I (LENGTH vs)) ISUB
-           ZIP (GENLIST dV (LENGTH vs),MAP (\i. i + LENGTH vs) (REVERSE vs)))
- *)
-Theorem dLAMl_to_dABSi_applied[local] =
-    GEN_ALL (SIMP_RULE std_ss [LET_DEF] dLAMl_to_dABSi)
-
-(* dB version of hnf_cases (only the ==> direction) *)
-Theorem dhnf_cases :
-    !M. dhnf M ==> ?n y Ms. M = dABSi n (dV y @* Ms)
-Proof
-    RW_TAC std_ss [hnf_cases]
- >> qabbrev_tac ‘n = LENGTH vs’
- >> Q.EXISTS_TAC ‘n’
- >> Know ‘fromTerm (toTerm M) = fromTerm (LAMl vs (VAR y @* args))’
- >- (art [fromTerm_11])
- >> Q.PAT_X_ASSUM ‘toTerm M = LAMl vs (VAR y @* args)’ K_TAC
- >> rw [fromTerm_LAMl, fromTerm_appstar, Excl "fromTerm_11"]
- >> qabbrev_tac ‘vs' = MAP s2n vs’
- >> qabbrev_tac ‘Ms = MAP fromTerm args’
- >> qabbrev_tac ‘y' = s2n y’
- >> Know ‘dLAMl vs' (dV y' @* Ms) =
-          dABSi (LENGTH vs')
-            (FOLDL lift (dV y' @* Ms) (GENLIST I (LENGTH vs')) ISUB
-             ZIP (GENLIST dV (LENGTH vs'),
-                  MAP (\i. i + LENGTH vs') (REVERSE vs')))’
- >- (MATCH_MP_TAC dLAMl_to_dABSi_applied \\
-     qunabbrev_tac ‘vs'’ \\
-     MATCH_MP_TAC ALL_DISTINCT_MAP_INJ >> rw [])
- >> ‘LENGTH vs' = n’ by rw [Abbr ‘vs'’] >> POP_ORW
- >> Rewr'
- >> simp [FOLDL_lift_appstar, isub_appstar]
- >> Know ‘FOLDL lift (dV y') (GENLIST I n) = dV (y' + n)’
- >- (KILL_TAC \\
-     Induct_on ‘n’ >> rw [GENLIST, FOLDL_SNOC])
- >> Rewr'
- >> qabbrev_tac ‘Ms' = MAP (\e. FOLDL lift e (GENLIST I n)) Ms’
- >> reverse (Cases_on ‘MEM y vs’)
- >- (‘~MEM y' vs'’ by (rw [Abbr ‘y'’, Abbr ‘vs'’, MEM_MAP]) \\
-     ‘~MEM y' (REVERSE vs')’ by PROVE_TAC [MEM_REVERSE] \\
-     Suff ‘dV (y' + n) ISUB ZIP (GENLIST dV n,MAP (\i. i + n) (REVERSE vs')) =
-           dV (y' + n)’ >- (Rewr' >> METIS_TAC []) \\
-     MATCH_MP_TAC isub_dV_fresh \\
-     qabbrev_tac ‘l1 = GENLIST dV n’ \\
-     qabbrev_tac ‘l2 = MAP (\i. i + n) (REVERSE vs')’ \\
-    ‘LENGTH l1 = n’ by rw [Abbr ‘l1’] \\
-    ‘LENGTH l2 = n’ by rw [Abbr ‘l2’, Abbr ‘n’, Abbr ‘vs'’] \\
-     simp [DOM_ALT_MAP_SND, MAP_ZIP] \\
-     rw [Abbr ‘l2’, MEM_MAP])
- (* stage work *)
- >> ‘MEM y' vs'’ by (rw [Abbr ‘y'’, Abbr ‘vs'’, MEM_MAP])
- >> ‘MEM y' (REVERSE vs')’ by PROVE_TAC [MEM_REVERSE]
- >> ‘?j. j < LENGTH (REVERSE vs') /\ y' = EL j (REVERSE vs')’
-        by METIS_TAC [MEM_EL]
- >> ‘LENGTH (REVERSE vs') = n’ by rw [Abbr ‘vs'’, Abbr ‘n’]
- >> qabbrev_tac ‘Ns = MAP (\i. i + n) (REVERSE vs')’
- >> ‘LENGTH Ns = n’ by rw [Abbr ‘Ns’]
- >> Know ‘ALL_DISTINCT Ns’
- >- (qunabbrev_tac ‘Ns’ \\
-     MATCH_MP_TAC ALL_DISTINCT_MAP_INJ >> rw [] \\
-     qunabbrev_tac ‘vs'’ \\
-     MATCH_MP_TAC ALL_DISTINCT_MAP_INJ >> rw [])
- >> DISCH_TAC
- >> Suff ‘dV (y' + n) ISUB ZIP (GENLIST dV n,Ns) = EL j (GENLIST dV n)’
- >- (Rewr' \\
-     simp [EL_GENLIST] >> METIS_TAC [])
- >> MATCH_MP_TAC isub_dV_once >> simp []
- >> CONJ_TAC >- (rw [Abbr ‘Ns’, EL_MAP])
- >> Q.X_GEN_TAC ‘i’ >> DISCH_TAC
- >> ‘n <= EL i Ns’ by rw [Abbr ‘Ns’, EL_MAP]
- >> Suff ‘FVS (ZIP (GENLIST dV n,Ns)) = count n’ >- rw []
- >> Q.PAT_X_ASSUM ‘LENGTH Ns = n’ MP_TAC
- >> KILL_TAC >> Q.ID_SPEC_TAC ‘Ns’
- >> Induct_on ‘n’ >> rw [dFVS_def]
- >> ‘Ns <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
- >> ‘LENGTH (FRONT Ns) = n’ by rw [LENGTH_FRONT]
- >> ‘Ns = SNOC (LAST Ns) (FRONT Ns)’
-      by (rw [APPEND_FRONT_LAST, SNOC_APPEND]) >> POP_ORW
- >> Q.PAT_X_ASSUM ‘!Ns. LENGTH Ns = n ==> P’ (MP_TAC o (Q.SPEC ‘FRONT Ns’))
- >> rw [GENLIST, COUNT_SUC, dFVS_SNOC, ZIP_SNOC, dFV_def]
- >> SET_TAC []
-QED
-
 val _ = export_theory ();
 val _ = html_theory "boehm_tree";
 
diff --git a/examples/lambda/other-models/pure_dBScript.sml b/examples/lambda/other-models/pure_dBScript.sml
index cee4462f2d..643d8a932f 100644
--- a/examples/lambda/other-models/pure_dBScript.sml
+++ b/examples/lambda/other-models/pure_dBScript.sml
@@ -1532,6 +1532,82 @@ Proof
  >> MATCH_MP_TAC isub_SNOC_lemma >> art []
 QED
 
+(* Translations from dLAMl to dABSi.
+
+   Some samples for guessing out the statements of this theorem:
+
+> SIMP_CONV arith_ss [dLAM_def, lift_def, sub_def, lift_sub]
+                     “dLAM v1 (dLAM v0 t)”;
+# val it =
+   |- dLAM v1 (dLAM v0 t) =
+      dABS (dABS ([dV 1/v1 + 2] ([dV 0/v0 + 2] (lift (lift t 0) 1)))): thm
+
+> SIMP_CONV arith_ss [dLAM_def, lift_def, sub_def, lift_sub]
+                     “dLAM v2 (dLAM v1 (dLAM v0 t))”;
+# val it =
+   |- dLAM v2 (dLAM v1 (dLAM v0 t)) =
+      dABS
+        (dABS
+           (dABS ([dV 2/v2 + 3]
+                    ([dV 1/v1 + 3]
+                       ([dV 0/v0 + 3]
+                          (lift (lift (lift t 0) 1) 2)))))): thm
+ *)
+Theorem dLAMl_to_dABSi :
+    !vs. ALL_DISTINCT (vs :num list) ==>
+         let n = LENGTH vs;
+             body = FOLDL lift t (GENLIST I n);
+             phi = ZIP (GENLIST dV n, MAP (\i. i + n) (REVERSE vs))
+         in dLAMl vs t = dABSi n (body ISUB phi)
+Proof
+    Induct_on ‘vs’ >- rw [isub_def]
+ >> rw [isub_def, GSYM SNOC_APPEND, MAP_SNOC, FUNPOW_SUC, GENLIST, FOLDL_SNOC,
+        dLAM_def]
+ >> fs []
+ >> qabbrev_tac ‘n = LENGTH vs’
+ >> rw [lift_dABSi]
+ >> Q.PAT_X_ASSUM ‘dLAMl vs t = _’ K_TAC
+ >> qabbrev_tac ‘N = FOLDL lift t (GENLIST I n)’
+ >> qabbrev_tac ‘Ms = GENLIST dV n’
+ >> qabbrev_tac ‘Vs = MAP (\i. i + n) (REVERSE vs)’
+ >> Know ‘lift (N ISUB ZIP (Ms,Vs)) n =
+          (lift N n) ISUB (ZIP (MAP (\e. lift e n) Ms,MAP SUC Vs))’
+ >- (MATCH_MP_TAC lift_isub \\
+     rw [Abbr ‘Ms’, Abbr ‘Vs’, EVERY_MEM, MEM_MAP] >> rw [])
+ >> Rewr'
+ >> ‘MAP SUC Vs = MAP (\i. i + SUC n) (REVERSE vs)’
+       by (rw [LIST_EQ_REWRITE, EL_MAP, Abbr ‘Vs’]) >> POP_ORW
+ >> qunabbrev_tac ‘Vs’ (* now useless *)
+ >> rw [sub_def, GSYM ADD1]
+ >> ‘MAP (\e. lift e n) Ms = Ms’
+       by (rw [LIST_EQ_REWRITE, EL_MAP, Abbr ‘Ms’]) >> POP_ORW
+ >> qabbrev_tac ‘Ns = MAP (\i. i + SUC n) (REVERSE vs)’
+ >> qabbrev_tac ‘N' = lift N n’
+ >> Suff ‘N' ISUB ZIP (SNOC (dV n) Ms,SNOC (h + SUC n) Ns) =
+          [dV n/h + SUC n] (N' ISUB ZIP (Ms,Ns))’ >- rw []
+ >> MATCH_MP_TAC isub_SNOC
+ >> rw [Abbr ‘Ms’, Abbr ‘Ns’, MEM_EL, EL_MAP]
+ >> rename1 ‘~(i < n)’
+ >> ‘LENGTH (REVERSE vs) = n’ by rw [Abbr ‘n’]
+ >> CCONTR_TAC >> gs [EL_MAP]
+ >> ‘h = EL i (REVERSE vs)’ by rw []
+ >> Suff ‘MEM h (REVERSE vs)’ >- rw [MEM_REVERSE]
+ >> Q.PAT_X_ASSUM ‘~MEM h vs’ K_TAC
+ >> ‘LENGTH (REVERSE vs) = n’ by rw [Abbr ‘n’]
+ >> REWRITE_TAC [MEM_EL]
+ >> Q.EXISTS_TAC ‘i’ >> art []
+QED
+
+(* |- !t vs.
+        ALL_DISTINCT vs ==>
+        dLAMl vs t =
+        dABSi (LENGTH vs)
+          (FOLDL lift t (GENLIST I (LENGTH vs)) ISUB
+           ZIP (GENLIST dV (LENGTH vs),MAP (\i. i + LENGTH vs) (REVERSE vs)))
+ *)
+Theorem dLAMl_to_dABSi_applied =
+    GEN_ALL (SIMP_RULE std_ss [LET_DEF] dLAMl_to_dABSi)
+
 val _ = export_theory();
 val _ = html_theory "pure_dB";
 
diff --git a/src/list/src/listScript.sml b/src/list/src/listScript.sml
index 1ecb47507b..46c59d6e34 100644
--- a/src/list/src/listScript.sml
+++ b/src/list/src/listScript.sml
@@ -1918,6 +1918,9 @@ Proof
   ASM_SIMP_TAC (srw_ss()) [TAKE_def]
 QED
 
+(* |- !n l. 0 < n ==> HD (TAKE n l) = HD l *)
+Theorem HD_TAKE = GEN_ALL (REWRITE_RULE [EL] (Q.SPECL [‘n’, ‘0’] EL_TAKE))
+
 val MAP_TAKE = store_thm(
   "MAP_TAKE",
   “!f n l. MAP f (TAKE n l) = TAKE n (MAP f l)”,
@@ -2626,6 +2629,10 @@ val SNOC_APPEND = store_thm("SNOC_APPEND",
    “!x (l:('a) list). SNOC x l = APPEND l [x]”,
    GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [SNOC, APPEND]);
 
+(* |- !l. l <> [] ==> SNOC (LAST l) (FRONT l) = l *)
+Theorem SNOC_LAST_FRONT =
+     REWRITE_RULE [GSYM SNOC_APPEND] APPEND_FRONT_LAST
+
 val LIST_TO_SET_SNOC = Q.store_thm("LIST_TO_SET_SNOC",
     ‘set (SNOC x ls) = x INSERT set ls’,
     Induct_on ‘ls’ THEN SRW_TAC [] [INSERT_COMM]);
diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml
index 827b36aec1..629e8c09de 100644
--- a/src/list/src/rich_listScript.sml
+++ b/src/list/src/rich_listScript.sml
@@ -2959,6 +2959,22 @@ val FRONT_APPEND = Q.store_thm ("FRONT_APPEND",
    `!l1 l2 e. FRONT (l1 ++ e::l2) = l1 ++ FRONT (e::l2)`,
    Induct_on `l1` THEN ASM_SIMP_TAC list_ss [FRONT_DEF])
 
+Theorem FRONT_APPEND_NOT_NIL :
+    !l1 l2. l2 <> [] ==> FRONT (l1 ++ l2) = l1 ++ FRONT l2
+Proof
+    rpt STRIP_TAC
+ >> Cases_on ‘l2’
+ >> FULL_SIMP_TAC std_ss [FRONT_APPEND]
+QED
+
+Theorem LAST_APPEND_NOT_NIL :
+    !l1 l2. l2 <> [] ==> LAST (l1 ++ l2) = LAST l2
+Proof
+    rpt STRIP_TAC
+ >> Cases_on ‘l2’
+ >> FULL_SIMP_TAC std_ss [LAST_APPEND_CONS]
+QED
+
 val EL_FRONT = Q.store_thm ("EL_FRONT",
    `!l n. n < LENGTH (FRONT l) /\ ~NULL l ==> (EL n (FRONT l) = EL n l)`,
    Induct_on `l`
@@ -3050,9 +3066,13 @@ Theorem EVERY_REPLICATE[simp]:
 Proof Induct_on `n` >> rw [] >> metis_tac []
 QED
 
-val ALL_DISTINCT_DROP = Q.store_thm("ALL_DISTINCT_DROP",
-   `!ls n. ALL_DISTINCT ls ==> ALL_DISTINCT (DROP n ls)`,
-   Induct >> simp[DROP_def] >> rw[])
+(* ALL_DISTINCT_DROP is already in listTheory *)
+Theorem ALL_DISTINCT_TAKE :
+    !ls n. ALL_DISTINCT ls ==> ALL_DISTINCT (TAKE n ls)
+Proof
+    Induct >> simp[TAKE_def] >> rw[]
+ >> METIS_TAC [MEM_TAKE]
+QED
 
 val MAP_SND_FILTER_NEQ = Q.store_thm("MAP_SND_FILTER_NEQ",
    `MAP SND (FILTER (\(x,y). y <> z) ls) = FILTER ($<> z) (MAP SND ls)`,
diff --git a/src/relation/relationScript.sml b/src/relation/relationScript.sml
index 874dcb00dc..b23aba696b 100644
--- a/src/relation/relationScript.sml
+++ b/src/relation/relationScript.sml
@@ -2403,4 +2403,20 @@ Proof
   ]
 QED
 
+(* ‘RINSERT’ inserts one more element into an existing relation *)
+val RINSERT = new_definition ("RINSERT",
+   “RINSERT R a b = \x y. R x y \/ (x = a /\ y = b)”);
+
+Theorem RINSERT_IDEM :
+    !R a b. (RINSERT R a b) a b
+Proof
+    SRW_TAC [] [RINSERT]
+QED
+
+Theorem RSUBSET_RINSERT :
+    !R a b. R RSUBSET (RINSERT R a b)
+Proof
+    SRW_TAC [] [RSUBSET, RINSERT]
+QED
+
 val _ = export_theory();