diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
index 2a1a0d0333..6b8a3014b9 100644
--- a/examples/lambda/barendregt/boehmScript.sml
+++ b/examples/lambda/barendregt/boehmScript.sml
@@ -9,7 +9,7 @@ open optionTheory arithmeticTheory pred_setTheory listTheory rich_listTheory
      llistTheory relationTheory ltreeTheory pathTheory posetTheory hurdUtils
      finite_mapTheory;
 
-open binderLib nomsetTheory termTheory appFOLDLTheory chap2Theory chap3Theory
+open binderLib termTheory appFOLDLTheory chap2Theory chap3Theory
      head_reductionTheory standardisationTheory solvableTheory reductionEval;
 
 open horeductionTheory takahashiS3Theory;
@@ -37,7 +37,7 @@ val o_DEF = combinTheory.o_DEF;
  *)
 Type boehm_tree[pp] = “:(string list # string) option ltree”
 
-(* Definition 10.1.9 [1, p.221] (Effective Boehm tree)
+(* Definition 10.1.9 [1, p.221] (Effective Boehm Tree)
 
    NOTE: The setup of ‘X UNION FV M’ when calling ‘FRESH_list’ guarentees that
    the generated Boehm tree is "correct" no matter what X is supplied.
@@ -210,8 +210,8 @@ Proof
  >> qabbrev_tac ‘Q1 = principle_hnf (Q0 @* MAP VAR vs')’
  >> qabbrev_tac ‘Ps = hnf_children P1’
  >> qabbrev_tac ‘Qs = hnf_children Q1’
- >> qabbrev_tac ‘y  = hnf_headvar P1’
- >> qabbrev_tac ‘y' = hnf_headvar Q1’
+ >> qabbrev_tac ‘y  = hnf_head P1’
+ >> qabbrev_tac ‘y' = hnf_head Q1’
  (* applying ltree_unfold *)
  >> Q.PAT_X_ASSUM ‘_ = BTe Y Q’ MP_TAC
  >> simp [BT_def, Once ltree_unfold, BT_generator_def]
@@ -254,7 +254,7 @@ Proof
     Here, once again, we need to get suitable explicit forms of P0 and Q0,
     to show that, P1 and Q1 are absfree hnf.
   *)
- >> ‘hnf P0 /\ hnf Q0’ by PROVE_TAC [hnf_principle_hnf, solvable_iff_has_hnf]
+ >> ‘hnf P0 /\ hnf Q0’ by PROVE_TAC [hnf_principle_hnf']
  >> qabbrev_tac ‘n = LAMl_size Q0’
  >> ‘ALL_DISTINCT vs /\ LENGTH vs = n /\ DISJOINT (set vs) Y’
       by rw [Abbr ‘vs’, FRESH_list_def]
@@ -345,11 +345,33 @@ Definition subterm_def :
         NONE
 End
 
-(* This assumes ‘subterm X M p <> NONE’ *)
+Theorem subterm_of_solvables :
+    !X M x xs. solvable M ==>
+               subterm X M (x::xs) =
+        let M0 = principle_hnf M;
+             n = LAMl_size M0;
+            vs = FRESH_list n (X UNION FV M);
+            M1 = principle_hnf (M0 @* (MAP VAR vs));
+            Ms = hnf_children M1;
+             m = LENGTH Ms
+        in
+            if x < m then subterm (X UNION set vs) (EL x Ms) xs else NONE
+Proof
+    RW_TAC std_ss []
+ >> rw [subterm_def]
+QED
+
+(* NOTE: The uses of ‘subterm' X M p’ assumes ‘subterm X M p <> NONE’ *)
 Overload subterm' = “\X M p. SND (THE (subterm X M p))”
 
-(* |- !X M. subterm X M [] = SOME M *)
-Theorem subterm_NIL[simp] = cj 1 subterm_def
+(* |- !X M. subterm X M [] = SOME (X,M) *)
+Theorem subterm_NIL[simp] = SPEC_ALL (cj 1 subterm_def)
+
+Theorem subterm_NIL'[simp] :
+    subterm' X M [] = M
+Proof
+    rw [subterm_NIL]
+QED
 
 (* Lemma 10.1.15 [1, p.222] *)
 Theorem BT_subterm_thm :
@@ -383,7 +405,8 @@ QED
 Theorem subterm_is_none_iff_parent_unsolvable :
     !p X M. p IN ltree_paths (BTe X M) ==>
            (subterm X M p = NONE <=>
-            p <> [] /\ unsolvable (subterm' X M (FRONT p)))
+            p <> [] /\ subterm X M (FRONT p) <> NONE /\
+            unsolvable (subterm' X M (FRONT p)))
 Proof
     Induct_on ‘p’ >> rw [subterm_def] (* 2 subgoals, only one left *)
  >> qabbrev_tac ‘M0 = principle_hnf M’
@@ -423,6 +446,226 @@ Proof
         ltree_lookup_def, LNTH_fromList, EL_MAP]
 QED
 
+Theorem subterm_is_none_imp_parent_not :
+    !p X M. p IN ltree_paths (BTe X M) /\
+            subterm X M p = NONE ==> subterm X M (FRONT p) <> NONE
+Proof
+    METIS_TAC [subterm_is_none_iff_parent_unsolvable]
+QED
+
+(* NOTE: for whatever reasons such that ‘subterm X M p = NONE’, even when
+        ‘p NOTIN ltree_paths (BTe X M)’, the conclusion (rhs) always holds.
+ *)
+Theorem subterm_is_none_iff_children :
+    !X M p. subterm X M p = NONE <=> !p'. p <<= p' ==> subterm X M p' = NONE
+Proof
+    rpt GEN_TAC
+ >> reverse EQ_TAC
+ >- (DISCH_THEN (MP_TAC o (Q.SPEC ‘p’)) >> rw [])
+ >> Q.ID_SPEC_TAC ‘M’
+ >> Q.ID_SPEC_TAC ‘X’
+ >> Q.ID_SPEC_TAC ‘p’
+ >> Induct_on ‘p’ >- rw [subterm_NIL]
+ >> rw [subterm_def]
+ >> Cases_on ‘p'’ >> fs [subterm_def]
+QED
+
+Theorem lameq_subterm_cong_none :
+    !p X M N. FINITE X /\ FV M UNION FV N SUBSET X /\ M == N ==>
+             (subterm X M p = NONE <=> subterm X N p = NONE)
+Proof
+    Q.X_GEN_TAC ‘p’
+ >> Cases_on ‘p = []’ >- rw []
+ >> POP_ASSUM MP_TAC
+ >> Q.ID_SPEC_TAC ‘p’
+ >> Induct_on ‘p’ >- rw []
+ >> RW_TAC std_ss []
+ >> reverse (Cases_on ‘solvable M’)
+ >- (‘unsolvable N’ by METIS_TAC [lameq_solvable_cong] \\
+     Cases_on ‘p’ >> fs [subterm_def])
+ >> ‘solvable N’ by METIS_TAC [lameq_solvable_cong]
+ >> RW_TAC std_ss [subterm_of_solvables]
+ >> Know ‘X UNION FV M = X /\ X UNION FV N = X’
+ >- (Q.PAT_X_ASSUM ‘FV M UNION FV N SUBSET X’ MP_TAC >> SET_TAC [])
+ >> DISCH_THEN (fs o wrap)
+ >> Know ‘n = n' /\ vs = vs'’
+ >- (reverse CONJ_ASM1_TAC >- rw [Abbr ‘vs’, Abbr ‘vs'’] \\
+     qunabbrevl_tac [‘n’, ‘n'’, ‘M0’, ‘M0'’] \\
+     MATCH_MP_TAC lameq_principle_hnf_size_eq' >> art [])
+ (* clean up now duplicated abbreviations: n' and vs' *)
+ >> qunabbrevl_tac [‘n'’, ‘vs'’]
+ >> DISCH_THEN (rfs o wrap o GSYM)
+ (* applying lameq_principle_hnf_thm' *)
+ >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘N’, ‘M0’, ‘M0'’, ‘n’, ‘vs’, ‘M1’, ‘M1'’]
+                     lameq_principle_hnf_thm') >> simp []
+ >> RW_TAC std_ss [Abbr ‘m’, Abbr ‘m'’]
+ >> qabbrev_tac ‘m = LENGTH Ms'’
+ >> Cases_on ‘h < m’ >> simp []
+ >> Cases_on ‘p = []’ >> fs []
+ (* preparing for hnf_children_FV_SUBSET
+
+    Here, once again, we need to get suitable explicit forms of P0 and Q0,
+    to show that, P1 and Q1 are absfree hnf.
+  *)
+ >> ‘hnf M0 /\ hnf M0'’ by PROVE_TAC [hnf_principle_hnf']
+ >> qabbrev_tac ‘n = LAMl_size M0’
+ >> ‘ALL_DISTINCT vs /\ LENGTH vs = n /\ DISJOINT (set vs) X’
+      by rw [Abbr ‘vs’, FRESH_list_def]
+ >> Know ‘DISJOINT (set vs) (FV M0)’
+ >- (MATCH_MP_TAC DISJOINT_SUBSET \\
+     Q.EXISTS_TAC ‘X’ >> art [] \\
+     MATCH_MP_TAC SUBSET_TRANS \\
+     Q.EXISTS_TAC ‘FV M’ >> art [] \\
+     qunabbrev_tac ‘M0’ \\
+     MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [])
+ >> DISCH_TAC
+ >> Know ‘DISJOINT (set vs) (FV M0')’
+ >- (MATCH_MP_TAC DISJOINT_SUBSET \\
+     Q.EXISTS_TAC ‘X’ >> art [] \\
+     MATCH_MP_TAC SUBSET_TRANS \\
+     Q.EXISTS_TAC ‘FV N’ >> art [] \\
+     qunabbrev_tac ‘M0'’ \\
+     MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [])
+ >> DISCH_TAC
+ (* NOTE: the next two hnf_tac will refine M1 and M1' *)
+ >> qunabbrevl_tac [‘M1’, ‘M1'’]
+ >> hnf_tac (“M0 :term”, “vs :string list”,
+             “M1 :term”, “y  :string”, “args :term list”)
+ >> hnf_tac (“M0':term”, “vs :string list”,
+             “M1':term”, “y' :string”, “args':term list”)
+ >> Q.PAT_X_ASSUM ‘n = LAMl_size M0'’ (rfs o wrap o SYM)
+ >> ‘TAKE n vs = vs’ by rw [TAKE_LENGTH_ID_rwt]
+ >> POP_ASSUM (rfs o wrap)
+ (* refine P1 and Q1 again for clear assumptions using them *)
+ >> qunabbrevl_tac [‘M1’, ‘M1'’]
+ >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’
+ >> qabbrev_tac ‘M1' = principle_hnf (M0' @* MAP VAR vs)’
+ (* final stage *)
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> simp []
+ >> CONJ_TAC (* 2 subgoals *)
+ >| [ (* goal 1 (of 2) *)
+      Know ‘!i. i < LENGTH Ms ==> FV (EL i Ms) SUBSET FV M1’
+      >- (MATCH_MP_TAC hnf_children_FV_SUBSET \\
+          rw [Abbr ‘Ms’, hnf_appstar]) >> DISCH_TAC \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV M1’ \\
+      CONJ_TAC >- (FIRST_X_ASSUM MATCH_MP_TAC >> art []) \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV M0 UNION set vs’ \\
+      CONJ_TAC >- simp [FV_LAMl] \\
+      Suff ‘FV M0 SUBSET X’ >- SET_TAC [] \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV M’ \\
+      reverse CONJ_TAC >- art [] (* FV M SUBSET X *) \\
+      qunabbrev_tac ‘M0’ >> MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [],
+      (* goal 2 (of 2) *)
+      Know ‘!i. i < LENGTH Ms' ==> FV (EL i Ms') SUBSET FV M1'’
+      >- (MATCH_MP_TAC hnf_children_FV_SUBSET \\
+          rw [Abbr ‘Ms'’, hnf_appstar]) >> DISCH_TAC \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV M1'’ \\
+      CONJ_TAC >- (FIRST_X_ASSUM MATCH_MP_TAC >> rw [Abbr ‘m’]) \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV M0' UNION set vs’ \\
+      CONJ_TAC >- simp [FV_LAMl] \\
+      Suff ‘FV M0' SUBSET X’ >- SET_TAC [] \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV N’ \\
+      reverse CONJ_TAC >- art [] (* FV N SUBSET X *) \\
+      qunabbrev_tac ‘M0'’ >> MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [] ]
+QED
+
+Theorem lameq_subterm_cong :
+    !p X M N. FINITE X /\ FV M UNION FV N SUBSET X /\ M == N /\
+              subterm X M p <> NONE /\ subterm X N p <> NONE ==>
+              subterm' X M p == subterm' X N p
+Proof
+    Q.X_GEN_TAC ‘p’
+ >> Cases_on ‘p = []’ >- rw []
+ >> POP_ASSUM MP_TAC
+ >> Q.ID_SPEC_TAC ‘p’
+ >> Induct_on ‘p’ >- rw []
+ >> RW_TAC std_ss []
+ >> reverse (Cases_on ‘solvable M’)
+ >- (‘unsolvable N’ by METIS_TAC [lameq_solvable_cong] \\
+     Cases_on ‘p’ >> fs [subterm_def])
+ >> ‘solvable N’ by METIS_TAC [lameq_solvable_cong]
+ >> Q.PAT_X_ASSUM ‘subterm X N (h::p) <> NONE’ MP_TAC
+ >> Q.PAT_X_ASSUM ‘subterm X M (h::p) <> NONE’ MP_TAC
+ >> RW_TAC std_ss [subterm_of_solvables]
+ >> gs []
+ >> Know ‘X UNION FV M = X /\ X UNION FV N = X’ >- ASM_SET_TAC []
+ >> DISCH_THEN (fs o wrap)
+ >> Know ‘n = n' /\ vs = vs'’
+ >- (reverse CONJ_ASM1_TAC >- rw [Abbr ‘vs’, Abbr ‘vs'’] \\
+     qunabbrevl_tac [‘n’, ‘n'’, ‘M0’, ‘M0'’] \\
+     MATCH_MP_TAC lameq_principle_hnf_size_eq' >> art [])
+ (* clean up now duplicated abbreviations: n' and vs' *)
+ >> qunabbrevl_tac [‘n'’, ‘vs'’]
+ >> DISCH_THEN (rfs o wrap o GSYM)
+ (* applying lameq_principle_hnf_thm' *)
+ >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘N’, ‘M0’, ‘M0'’, ‘n’, ‘vs’, ‘M1’, ‘M1'’]
+                     lameq_principle_hnf_thm') >> simp []
+ >> RW_TAC std_ss [Abbr ‘m’, Abbr ‘m'’]
+ >> qabbrev_tac ‘m = LENGTH Ms'’
+ >> Cases_on ‘p = []’ >> fs []
+ (* preparing for hnf_children_FV_SUBSET *)
+ >> ‘hnf M0 /\ hnf M0'’ by PROVE_TAC [hnf_principle_hnf']
+ >> qabbrev_tac ‘n = LAMl_size M0’
+ >> ‘ALL_DISTINCT vs /\ LENGTH vs = n /\ DISJOINT (set vs) X’
+      by rw [Abbr ‘vs’, FRESH_list_def]
+ >> Know ‘DISJOINT (set vs) (FV M0)’
+ >- (MATCH_MP_TAC DISJOINT_SUBSET \\
+     Q.EXISTS_TAC ‘X’ >> art [] \\
+     MATCH_MP_TAC SUBSET_TRANS \\
+     Q.EXISTS_TAC ‘FV M’ >> art [] \\
+     qunabbrev_tac ‘M0’ \\
+     MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [])
+ >> DISCH_TAC
+ >> Know ‘DISJOINT (set vs) (FV M0')’
+ >- (MATCH_MP_TAC DISJOINT_SUBSET \\
+     Q.EXISTS_TAC ‘X’ >> art [] \\
+     MATCH_MP_TAC SUBSET_TRANS \\
+     Q.EXISTS_TAC ‘FV N’ >> art [] \\
+     qunabbrev_tac ‘M0'’ \\
+     MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [])
+ >> DISCH_TAC
+ (* NOTE: the next two hnf_tac will refine M1 and M1' *)
+ >> qunabbrevl_tac [‘M1’, ‘M1'’]
+ >> hnf_tac (“M0 :term”, “vs :string list”,
+             “M1 :term”, “y  :string”, “args :term list”)
+ >> hnf_tac (“M0':term”, “vs :string list”,
+             “M1':term”, “y' :string”, “args':term list”)
+ >> Q.PAT_X_ASSUM ‘n = LAMl_size M0'’ (rfs o wrap o SYM)
+ >> ‘TAKE n vs = vs’ by rw [TAKE_LENGTH_ID_rwt]
+ >> POP_ASSUM (rfs o wrap)
+ (* refine P1 and Q1 again for clear assumptions using them *)
+ >> qunabbrevl_tac [‘M1’, ‘M1'’]
+ >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’
+ >> qabbrev_tac ‘M1' = principle_hnf (M0' @* MAP VAR vs)’
+ (* final stage *)
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> simp []
+ >> CONJ_TAC (* 2 subgoals *)
+ >| [ (* goal 1 (of 2) *)
+      Know ‘!i. i < LENGTH Ms ==> FV (EL i Ms) SUBSET FV M1’
+      >- (MATCH_MP_TAC hnf_children_FV_SUBSET \\
+          rw [Abbr ‘Ms’, hnf_appstar]) >> DISCH_TAC \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV M1’ \\
+      CONJ_TAC >- (FIRST_X_ASSUM MATCH_MP_TAC >> art []) \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV M0 UNION set vs’ \\
+      CONJ_TAC >- simp [FV_LAMl] \\
+      Suff ‘FV M0 SUBSET X’ >- SET_TAC [] \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV M’ \\
+      reverse CONJ_TAC >- art [] (* FV M SUBSET X *) \\
+      qunabbrev_tac ‘M0’ >> MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [],
+      (* goal 2 (of 2) *)
+      Know ‘!i. i < LENGTH Ms' ==> FV (EL i Ms') SUBSET FV M1'’
+      >- (MATCH_MP_TAC hnf_children_FV_SUBSET \\
+          rw [Abbr ‘Ms'’, hnf_appstar]) >> DISCH_TAC \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV M1'’ \\
+      CONJ_TAC >- (FIRST_X_ASSUM MATCH_MP_TAC >> rw [Abbr ‘m’]) \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV M0' UNION set vs’ \\
+      CONJ_TAC >- simp [FV_LAMl] \\
+      Suff ‘FV M0' SUBSET X’ >- SET_TAC [] \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV N’ \\
+      reverse CONJ_TAC >- art [] (* FV N SUBSET X *) \\
+      qunabbrev_tac ‘M0'’ >> MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [] ]
+QED
+
 (*---------------------------------------------------------------------------*
  *  Equivalent terms
  *---------------------------------------------------------------------------*)
@@ -445,7 +688,7 @@ Definition equivalent_def :
                N0 = principle_hnf N;
                n  = LAMl_size M0;
                n' = LAMl_size N0;
-               vs = FRESH_list (MAX n n') (FV M0 UNION FV N0);
+               vs = FRESH_list (MAX n n') (FV M UNION FV N);
               vsM = TAKE n  vs;
               vsN = TAKE n' vs;
                M1 = principle_hnf (M0 @* (MAP VAR vsM));
@@ -481,7 +724,7 @@ Theorem equivalent_of_solvables :
               N0 = principle_hnf N;
               n  = LAMl_size M0;
               n' = LAMl_size N0;
-              vs = FRESH_list (MAX n n') (FV M0 UNION FV N0);
+              vs = FRESH_list (MAX n n') (FV M UNION FV N);
              vsM = TAKE n  vs;
              vsN = TAKE n' vs;
               M1 = principle_hnf (M0 @* (MAP VAR vsM));
@@ -496,6 +739,31 @@ Proof
     RW_TAC std_ss [equivalent_def]
 QED
 
+(* beta-equivalent terms are also equivalent here *)
+Theorem lameq_imp_equivalent :
+    !M N. M == N ==> equivalent M N
+Proof
+    rpt STRIP_TAC
+ >> reverse (Cases_on ‘solvable M’)
+ >- (‘unsolvable N’ by METIS_TAC [lameq_solvable_cong] \\
+     rw [equivalent_def])
+ >> ‘solvable N’ by METIS_TAC [lameq_solvable_cong]
+ >> qabbrev_tac ‘X = FV M UNION FV N’
+ >> ‘FINITE X’ by rw [Abbr ‘X’]
+ >> ‘LAMl_size (principle_hnf M) = LAMl_size (principle_hnf N)’
+       by METIS_TAC [lameq_principle_hnf_size_eq']
+ (* stage work *)
+ >> RW_TAC std_ss [equivalent_of_solvables] (* 2 subgoals, same tactics *)
+ >> ‘ALL_DISTINCT vs /\ DISJOINT (set vs) X /\ LENGTH vs = n’
+       by rw [Abbr ‘vs’, FRESH_list_def]
+ >> ‘vsM = vs’ by rw [Abbr ‘vsM’, TAKE_LENGTH_ID_rwt]
+ >> POP_ASSUM (fs o wrap)
+ >> Q.PAT_X_ASSUM ‘vs = vsN’ (fs o wrap o SYM)
+ >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘N’, ‘M0’, ‘N0’, ‘n’, ‘vs’, ‘M1’, ‘N1’]
+                    lameq_principle_hnf_thm')
+ >> simp [Abbr ‘X’]
+QED
+
 (* NOTE: the initial calls of ‘principle_hnf’ get eliminated if the involved
          terms are already in head normal forms.
  *)
@@ -522,14 +790,20 @@ Proof
  >> METIS_TAC []
 QED
 
-(* The following combined tactic is useful after:
-
-   RW_TAC std_ss [equivalent_of_solvables, principle_hnf_reduce]
-
-   NOTE: it doesn't work with equivalent_of_hnf
+(* 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.
  *)
-val equivalent_tac =
-    ‘hnf M0 /\ hnf N0’ by PROVE_TAC [hnf_principle_hnf, solvable_iff_has_hnf]
+Theorem not_equivalent_example :
+    !x y. x <> y ==> ~equivalent (LAM x (VAR y @@ t)) (LAM y (VAR y @@ t))
+Proof
+    qx_genl_tac [‘x’, ‘v’] >> DISCH_TAC
+ >> ‘hnf (LAM x (VAR v @@ t)) /\ hnf (LAM v (VAR v @@ t))’ by rw []
+ >> ‘solvable (LAM x (VAR v @@ t)) /\ solvable (LAM v (VAR v @@ t))’
+       by rw [solvable_iff_has_hnf, hnf_has_hnf]
+ >> RW_TAC std_ss [equivalent_of_solvables, principle_hnf_reduce]
+ (* fix M0 *)
+ >> qunabbrev_tac ‘M0’ >> qabbrev_tac ‘M0 = LAM x (VAR v @@ t)’
  >> ‘ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M0 UNION FV N0) /\
      LENGTH vs = MAX n n'’ by rw [Abbr ‘vs’, FRESH_list_def]
  >> ‘DISJOINT (set vs) (FV M0) /\ DISJOINT (set vs) (FV N0)’
@@ -552,54 +826,43 @@ val equivalent_tac =
  >> Q.PAT_X_ASSUM ‘M1 = _’ ASSUME_TAC
  >> Q.PAT_X_ASSUM ‘N1 = _’ ASSUME_TAC
  >> ‘VAR y1 = y’  by rw [Abbr ‘y’ , absfree_hnf_head]
- >> ‘VAR y2 = y'’ by rw [Abbr ‘y'’, absfree_hnf_head];
-
-(* 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_reduce]
- (* applying shared tactics *)
- >> equivalent_tac
+ >> ‘VAR y2 = y'’ by rw [Abbr ‘y'’, absfree_hnf_head]
  >> 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)
+ >> ‘vsN = vs’ by rw [Abbr ‘vsN’, TAKE_LENGTH_ID_rwt]
+ >> POP_ASSUM (rfs o wrap)
+ >> Q.PAT_X_ASSUM ‘vs = vsM’ (rfs o wrap o SYM)
+ >> qunabbrev_tac ‘vsN’
+ (* stage work *)
  >> 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’
+ >> Q.PAT_X_ASSUM ‘VAR y1 = hnf_head M1’ (rfs o wrap o SYM)
+ >> Q.PAT_X_ASSUM ‘_ = LAM z (VAR y1 @* args1)’ (rfs o wrap o SYM)
+ >> Q.PAT_X_ASSUM ‘_ = LAM z (VAR y2 @* args2)’ (rfs o wrap o SYM)
+ (* now the goal is ‘y1 <> y2’ *)
+ >> qabbrev_tac ‘u = VAR v @@ t’
+ >> ‘hnf u’ by rw [Abbr ‘u’]
+ >> Know ‘M1 = [VAR z/x] u’
  >- (qunabbrev_tac ‘M1’ \\
-     Cases_on ‘z = x’ >- POP_ASSUM (rfs o wrap) \\
-     MATCH_MP_TAC principle_hnf_beta >> simp [Abbr ‘t’] \\
+     Cases_on ‘z = x’ >- (POP_ASSUM (gs o wrap) \\
+                          fs [principle_hnf_beta_reduce1]) \\
+     MATCH_MP_TAC principle_hnf_beta >> simp [Abbr ‘u’] \\
      rfs [FV_thm])
- >> Rewr'
- >> Know ‘N1 = [VAR z/v] t’
+ >> DISCH_THEN (rfs o wrap)
+ >> Know ‘N1 = [VAR z/v] u’
  >- (qunabbrev_tac ‘N1’ \\
-     Cases_on ‘z = v’ >- POP_ASSUM (rfs o wrap) \\
-     MATCH_MP_TAC principle_hnf_beta >> simp [Abbr ‘t’] \\
+     Cases_on ‘z = v’ >- (POP_ASSUM (rfs o wrap)) \\
+     MATCH_MP_TAC principle_hnf_beta >> simp [Abbr ‘u’] \\
      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]
+ >> DISCH_THEN (rfs o wrap)
+ >> qunabbrevl_tac [‘M1’, ‘N1’]
+ >> rfs [Abbr ‘u’, app_eq_appstar]
  >> METIS_TAC []
 QED
 
@@ -613,14 +876,6 @@ QED
  *  Boehm transformations
  *---------------------------------------------------------------------------*)
 
-(* Definition 10.3.2 [1, p.246] *)
-val _ = set_fixity "is_substitution_instance_of" (Infixr 490);
-
-(* NOTE: ‘(DOM phi) SUBSET (FV M)’ is not necessary *)
-Definition is_substitution_instance_of :
-    N is_substitution_instance_of M <=> ?phi. N = M ISUB phi
-End
-
 (* Definition 10.3.3 (i) [1, p.246] *)
 Type transform[pp] = “:(term -> term) list”
 
@@ -744,10 +999,7 @@ Proof
  >> irule lameq_sub_cong >> rw []
 QED
 
-(* Lemma 10.3.4 (ii) [1, p.246]
-
-   Used by: Boehm_transform_lameq_appstar
- *)
+(* Lemma 10.3.4 (ii) [1, p.246] *)
 Theorem Boehm_transform_lameq_LAMl_appstar :
     !pi. Boehm_transform pi ==>
          ?c. ctxt c /\ (!M. apply pi M == c M) /\
@@ -796,10 +1048,7 @@ Proof
  >> Q.PAT_X_ASSUM ‘FV M SUBSET (set vs)’ MP_TAC >> SET_TAC []
 QED
 
-(* An corollary of the above lemma with ‘xs = {}’
-
-   Used by: closed_separability_thm
- *)
+(* An corollary of the above lemma with ‘xs = {}’ *)
 Theorem Boehm_transform_lameq_appstar :
     !pi. Boehm_transform pi ==>
          ?Ns. !M. closed M ==> apply pi M == M @* Ns
@@ -812,8 +1061,7 @@ Proof
  >> RW_TAC (betafy (srw_ss())) []
 QED
 
-(* Used by: distinct_benf_imp_inconsistent *)
-Theorem asmlam_apply_cong :
+Theorem Boehm_apply_asmlam_cong :
     !pi M N. Boehm_transform pi /\ asmlam eqns M N ==>
              asmlam eqns (apply pi M) (apply pi N)
 Proof
@@ -824,8 +1072,7 @@ Proof
  >> MATCH_MP_TAC asmlam_subst >> art []
 QED
 
-(* Used by: separability_lemma2 *)
-Theorem lameq_apply_cong :
+Theorem Boehm_apply_lameq_cong :
     !pi M N. Boehm_transform pi /\ M == N ==> apply pi M == apply pi N
 Proof
     Induct_on ‘pi’ using SNOC_INDUCT >> rw []
@@ -833,14 +1080,12 @@ Proof
  >> MATCH_MP_TAC solving_transform_lameq >> art []
 QED
 
-(* Used by separability_thm *)
 Theorem Boehm_transform_APPEND :
     !p1 p2. Boehm_transform p1 /\ Boehm_transform p2 ==> Boehm_transform (p1 ++ p2)
 Proof
     rw [Boehm_transform_def]
 QED
 
-(* Used by separability_thm *)
 Theorem Boehm_apply_APPEND :
     !p1 p2 M. apply (p1 ++ p2) M = apply p1 (apply p2 M)
 Proof
@@ -849,7 +1094,6 @@ Proof
  >> rw [APPEND_SNOC]
 QED
 
-(* Used by separability_lemma2 *)
 Theorem Boehm_apply_MAP_rightctxt :
     !Ns t. apply (MAP rightctxt Ns) t = t @* (REVERSE Ns)
 Proof
@@ -857,7 +1101,6 @@ Proof
  >> 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
@@ -867,7 +1110,6 @@ Proof
  >> 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
@@ -970,32 +1212,15 @@ Proof
              “M1 :term”, “y :string”, “args :term list”)
  >> ‘TAKE (LAMl_size M0) vs = vs’ by rw []
  >> POP_ASSUM (REV_FULL_SIMP_TAC std_ss o wrap)
- >> qabbrev_tac ‘xs :term list = MAP VAR vs’
- >> qabbrev_tac ‘p1 = MAP rightctxt (REVERSE xs)’
- >> ‘apply p1 M0 == M1’
-       by (rw [Abbr ‘p1’, Boehm_apply_MAP_rightctxt', Abbr ‘xs’])
+ >> qabbrev_tac ‘p1 = MAP rightctxt (REVERSE (MAP VAR vs))’
+ >> ‘Boehm_transform p1’ by rw [Abbr ‘p1’, MAP_MAP_o, GSYM MAP_REVERSE]
+ >> ‘apply p1 M0 == M1’  by rw [Abbr ‘p1’, Boehm_apply_MAP_rightctxt']
  >> qabbrev_tac ‘m = LENGTH args’
- (* X collects all free variables in ‘args’ *)
- >> qabbrev_tac ‘X = BIGUNION (IMAGE FV (set args))’
- >> Know ‘FINITE X’
- >- (qunabbrev_tac ‘X’ \\
-     MATCH_MP_TAC FINITE_BIGUNION >> rw [] >> rw [])
- >> DISCH_TAC
- (* Z needs to avoid any free variables in args' *)
- >> FRESH_list_tac (“Z :string list”, “(m + 1) :num”, “X :string set”)
- >> ‘Z <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
- >> qabbrev_tac ‘z = LAST Z’
- >> ‘MEM z Z’ by rw [Abbr ‘z’, MEM_LAST_NOT_NIL]
- (* P is a permutator *)
- >> qabbrev_tac ‘P = LAMl Z (VAR z @* MAP VAR (FRONT Z))’
- >> Know ‘FV P = {}’
- >- (rw [Abbr ‘P’, FV_LAMl] \\
-     Suff ‘FV (VAR z @* MAP VAR (FRONT Z)) SUBSET set Z’ >- SET_TAC [] \\
-     rw [FV_appstar, SUBSET_DEF, MEM_MAP] >- art [] \\
-     rfs [MEM_FRONT_NOT_NIL])
- >> DISCH_TAC
+ >> qabbrev_tac ‘P = permutator m’
+ >> ‘FV P = {}’ by rw [Abbr ‘P’, closed_permutator, GSYM closed_def]
  >> qabbrev_tac ‘p2 = [[P/y]]’
- >> ‘apply p2 M1 = P @* MAP [P/y] args’ by (rw [Abbr ‘p2’, appstar_SUB])
+ >> ‘Boehm_transform p2’ by rw [Abbr ‘p2’]
+ >> ‘apply p2 M1 = P @* MAP [P/y] args’ by rw [Abbr ‘p2’, appstar_SUB]
  >> qabbrev_tac ‘args' = MAP [P/y] args’
  >> ‘!i. i < m ==> FV (EL i args') SUBSET FV (EL i args)’
          by rw [Abbr ‘args'’, EL_MAP, FV_SUB]
@@ -1011,90 +1236,22 @@ Proof
      FIRST_X_ASSUM MATCH_MP_TAC >> art [])
  >> DISCH_TAC
  (* a needs to avoid any free variables in args' *)
+ >> qabbrev_tac ‘X = BIGUNION (IMAGE (FV :term -> string set) (set args'))’
+ >> Know ‘FINITE X’
+ >- (rw [Abbr ‘X’] >> rw [])
+ >> DISCH_TAC
  >> NEW_TAC "a" “X :string set”
  >> qabbrev_tac ‘p3 = [rightctxt (VAR a)]’
+ >> ‘Boehm_transform p3’ by rw [Abbr ‘p3’, MAP_MAP_o, GSYM MAP_REVERSE]
  >> Know ‘apply p3 (P @* args') == VAR a @* args'’
- >- (rw [Abbr ‘p3’, Abbr ‘P’, rightctxt_thm] \\
-    ‘!t. LAMl Z t = LAMl (SNOC z (FRONT Z)) t’
-         by (ASM_SIMP_TAC std_ss [Abbr ‘z’, SNOC_LAST_FRONT]) >> POP_ORW \\
-     REWRITE_TAC [LAMl_SNOC] \\
-     qabbrev_tac ‘t = LAM z (VAR z @* MAP VAR (FRONT Z))’ \\
-     MATCH_MP_TAC lameq_TRANS \\
-     Q.EXISTS_TAC ‘LAM z (VAR z @* args') @@ VAR a’ \\
-  (* applying lameq_LAMl_appstar_ssub *)
-     CONJ_TAC
-     >- (MATCH_MP_TAC lameq_APPL \\
-         Suff ‘LAM z (VAR z @* args') = (FEMPTY |++ ZIP (FRONT Z,args')) ' t’
-         >- (Rewr' >> MATCH_MP_TAC lameq_LAMl_appstar_ssub \\
-             CONJ_TAC >- rw [ALL_DISTINCT_FRONT] \\
-             CONJ_TAC >- rw [LENGTH_FRONT] \\
-             ONCE_REWRITE_TAC [DISJOINT_SYM] \\
-             MATCH_MP_TAC DISJOINT_SUBSET >> Q.EXISTS_TAC ‘set Z’ \\
-             reverse CONJ_TAC >- rw [SUBSET_DEF, MEM_FRONT_NOT_NIL] \\
-             ASM_SIMP_TAC std_ss [Once DISJOINT_SYM, Abbr ‘X’] \\
-             MATCH_MP_TAC DISJOINT_SUBSET \\
-             Q.EXISTS_TAC ‘BIGUNION (IMAGE FV (set args))’ >> art []) \\
-         qunabbrev_tac ‘t’ \\
-         qabbrev_tac ‘fm = FEMPTY |++ ZIP (FRONT Z,args')’ \\
-        ‘LENGTH (FRONT Z) = LENGTH args'’ by rw [LENGTH_FRONT] \\
-        ‘FDOM fm = set (FRONT Z)’ by rw [Abbr ‘fm’, FDOM_FUPDATE_LIST, MAP_ZIP] \\
-         Know ‘z NOTIN FDOM fm’
-         >- (rw [Abbr ‘z’] \\
-             Know ‘ALL_DISTINCT (SNOC (LAST Z) (FRONT Z))’
-             >- rw [SNOC_LAST_FRONT] \\
-             rw [ALL_DISTINCT_SNOC]) >> DISCH_TAC \\
-         qabbrev_tac ‘t = VAR z @* MAP VAR (FRONT Z)’ \\
-         qabbrev_tac ‘L = ZIP (FRONT Z,args')’ \\
-         Know ‘!n. n < LENGTH args' ==> (FEMPTY |++ L) ' (EL n (FRONT Z)) = EL n args'’
-         >- (rpt STRIP_TAC \\
-             MATCH_MP_TAC FUPDATE_LIST_APPLY_MEM \\
-             Q.EXISTS_TAC ‘n’ >> rw [Abbr ‘L’, MAP_ZIP] \\
-            ‘m <> n’ by rw [] \\
-            ‘ALL_DISTINCT (FRONT Z)’ by METIS_TAC [ALL_DISTINCT_FRONT] \\
-             METIS_TAC [EL_ALL_DISTINCT_EL_EQ]) >> DISCH_TAC \\
-         Know ‘fm ' (LAM z t) = LAM z (fm ' t)’
-         >- (MATCH_MP_TAC ssub_LAM >> art [] \\
-             rw [Abbr ‘fm’, FDOM_FUPDATE_LIST, MAP_ZIP, MEM_EL] \\
-             Know ‘(FEMPTY |++ L) ' (EL n (FRONT Z)) = EL n args'’
-             >- (FIRST_X_ASSUM MATCH_MP_TAC >> art []) >> Rewr' \\
-             Suff ‘z # EL n args’
-             >- (DISCH_TAC >> CCONTR_TAC >> fs [] >> METIS_TAC [SUBSET_DEF]) \\
-             CCONTR_TAC >> fs [] \\
-             Q.PAT_X_ASSUM ‘DISJOINT (set Z) X’ MP_TAC \\
-             rw [DISJOINT_ALT, Abbr ‘X’] \\
-             Q.EXISTS_TAC ‘FV (EL n args)’ \\
-             CONJ_TAC >- (Q.EXISTS_TAC ‘EL n args’ >> rw [MEM_EL] \\
-                          Q.EXISTS_TAC ‘n’ >> rw []) \\
-             Q.EXISTS_TAC ‘z’ >> rw [MEM_LAST_NOT_NIL, Abbr ‘z’]) >> Rewr' \\
-         simp [Abbr ‘t’, ssub_appstar] \\
-         simp [Once LIST_EQ_REWRITE] \\
-         Q.X_GEN_TAC ‘i’ \\
-         Q.PAT_X_ASSUM ‘LENGTH args = LENGTH args'’ K_TAC \\
-         REWRITE_TAC [MAP_MAP_o] \\
-         DISCH_TAC >> ‘i < LENGTH (FRONT Z)’ by rw [] \\
-         ASM_SIMP_TAC std_ss [EL_MAP] \\
-        ‘MEM (EL i (FRONT Z)) (FRONT Z)’ by METIS_TAC [MEM_EL] \\
-         rw [Abbr ‘fm’, ssub_thm]) \\
-     Suff ‘VAR a @* args' = [VAR a/z](VAR z @* args')’
-     >- (Rewr' >> rw [lameq_BETA]) \\
-     rw [appstar_SUB] \\
-     rw [Once LIST_EQ_REWRITE] >> rename1 ‘n < LENGTH args'’ \\
-     rw [EL_MAP] \\
-     MATCH_MP_TAC (GSYM lemma14b) \\
-     Know ‘DISJOINT (set Z) (BIGUNION (IMAGE FV (set args')))’
-     >- (MATCH_MP_TAC DISJOINT_SUBSET \\
-         Q.EXISTS_TAC ‘X’ >> rw [Abbr ‘X’]) \\
-     rw [DISJOINT_ALT] >> FIRST_X_ASSUM irule >> art [] \\
-     Q.EXISTS_TAC ‘EL n args'’ >> rw [MEM_EL] \\
-     Q.EXISTS_TAC ‘n’ >> art [])
+ >- (rw [Abbr ‘p3’, Abbr ‘P’, rightctxt_thm, Boehm_apply_MAP_rightctxt'] \\
+     MATCH_MP_TAC permutator_thm >> art [])
  >> DISCH_TAC
  (* final stage *)
  >> Q.EXISTS_TAC ‘p3 ++ p2 ++ p1’
  >> CONJ_ASM1_TAC
- >- (MATCH_MP_TAC Boehm_transform_APPEND \\
-     reverse CONJ_TAC
-     >- (rw [Abbr ‘p1’, Abbr ‘xs’, MAP_MAP_o, GSYM MAP_REVERSE]) \\
-     MATCH_MP_TAC Boehm_transform_APPEND >> rw [Abbr ‘p2’, Abbr ‘p3’])
+ >- (MATCH_MP_TAC Boehm_transform_APPEND >> art [] \\
+     MATCH_MP_TAC Boehm_transform_APPEND >> art [])
  (* applying is_ready_alt *)
  >> simp [is_ready_alt]
  >> DISJ2_TAC
@@ -1102,15 +1259,12 @@ Proof
  >> reverse CONJ_TAC
  >- (rw [EVERY_MEM] \\
      Suff ‘FV e SUBSET X’ >- METIS_TAC [SUBSET_DEF] \\
-     MATCH_MP_TAC SUBSET_TRANS \\
-     Q.EXISTS_TAC ‘BIGUNION (IMAGE FV (set args'))’ \\
-     reverse CONJ_TAC >- rw [Abbr ‘X’] \\
-     rw [SUBSET_DEF, IN_BIGUNION_IMAGE] \\
+     rw [Abbr ‘X’, SUBSET_DEF, IN_BIGUNION_IMAGE] \\
      Q.EXISTS_TAC ‘e’ >> art [])
  >> MATCH_MP_TAC lameq_TRANS
  >> Q.EXISTS_TAC ‘apply (p3 ++ p2 ++ p1) M0’
  >> CONJ_TAC
- >- (MATCH_MP_TAC lameq_apply_cong \\
+ >- (MATCH_MP_TAC Boehm_apply_lameq_cong \\
      CONJ_TAC >- art [] \\
      qunabbrev_tac ‘M0’ \\
      MATCH_MP_TAC lameq_SYM \\
@@ -1119,13 +1273,12 @@ Proof
  >> MATCH_MP_TAC lameq_TRANS
  >> Q.EXISTS_TAC ‘apply (p3 ++ p2) M1’
  >> CONJ_TAC
- >- (MATCH_MP_TAC lameq_apply_cong >> art [] \\
-     MATCH_MP_TAC Boehm_transform_APPEND >> rw [Abbr ‘p2’, Abbr ‘p3’])
+ >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> art [] \\
+     MATCH_MP_TAC Boehm_transform_APPEND >> art [])
  >> REWRITE_TAC [Boehm_apply_APPEND]
  >> MATCH_MP_TAC lameq_TRANS
  >> Q.EXISTS_TAC ‘apply p3 (P @* args')’ >> art []
- >> MATCH_MP_TAC lameq_apply_cong
- >> rw [Abbr ‘p3’]
+ >> MATCH_MP_TAC Boehm_apply_lameq_cong >> rw []
 QED
 
 (*---------------------------------------------------------------------------*
@@ -1172,8 +1325,8 @@ Proof
      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' \\
+         Q.PAT_X_ASSUM ‘DISJOINT (set vs) _’ MP_TAC \\
+         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] \\
@@ -1190,7 +1343,7 @@ Proof
      >- (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] \\
+     rw [GSYM I_thm] \\
      MATCH_MP_TAC lameq_appstar_cong >> rw [lameq_I])
  >> DISCH_TAC
  >> qabbrev_tac ‘b0 = LAST bs’
@@ -1199,8 +1352,8 @@ Proof
      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' \\
+         Q.PAT_X_ASSUM ‘DISJOINT (set vs) _’ MP_TAC \\
+         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] \\
@@ -1225,7 +1378,7 @@ Proof
                   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])
+     rw [Abbr ‘t’, GSYM I_thm, lameq_I])
  >> DISCH_TAC
  (* p3 *)
  >> qabbrev_tac ‘f1 = [LAMl bs P/a]’
@@ -1276,7 +1429,7 @@ Proof
       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 []) \\
+      CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> art []) \\
       rw [Abbr ‘p3’] \\
       MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘f2 P’ \\
       reverse CONJ_TAC >- rw [] \\
@@ -1287,7 +1440,7 @@ Proof
       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 [] ]
+      MATCH_MP_TAC Boehm_apply_lameq_cong >> art [] ]
 QED
 
 Theorem separability_lemma0[local] :
@@ -1297,8 +1450,39 @@ Theorem separability_lemma0[local] :
           !P Q. ?pi. Boehm_transform pi /\ apply pi M == P /\ apply pi N == Q
 Proof
     RW_TAC std_ss [equivalent_of_solvables]
- (* applying the shared equivalent_tac *)
- >> equivalent_tac
+ >> ‘hnf M0 /\ hnf N0’ by PROVE_TAC [hnf_principle_hnf, solvable_iff_has_hnf]
+ >> ‘ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M UNION FV N) /\
+     LENGTH vs = MAX n n'’ by rw [Abbr ‘vs’, FRESH_list_def]
+ >> ‘DISJOINT (set vs) (FV M) /\ DISJOINT (set vs) (FV N)’
+      by METIS_TAC [DISJOINT_SYM, DISJOINT_UNION]
+ (* applying principle_hnf_FV_SUBSET' *)
+ >> Know ‘DISJOINT (set vs) (FV M0)’
+ >- (MATCH_MP_TAC DISJOINT_SUBSET >> Q.EXISTS_TAC ‘FV M’ >> art [] \\
+     qunabbrev_tac ‘M0’ >> MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [])
+ >> DISCH_TAC
+ >> Know ‘DISJOINT (set vs) (FV N0)’
+ >- (MATCH_MP_TAC DISJOINT_SUBSET >> Q.EXISTS_TAC ‘FV N’ >> art [] \\
+     qunabbrev_tac ‘N0’ >> MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [])
+ >> DISCH_TAC
+ >> qunabbrevl_tac [‘M1’, ‘N1’]
+ >> hnf_tac (“M0 :term”, “vs :string list”,
+             “M1 :term”, “y1 :string”, “args1 :term list”)
+ >> hnf_tac (“N0 :term”, “vs :string list”,
+             “N1 :term”, “y2 :string”, “args2 :term list”)
+ >> ‘TAKE (LAMl_size M0) vs = vsM’ by rw [Abbr ‘vsM’, Abbr ‘n’]
+ >> ‘TAKE (LAMl_size N0) vs = vsN’ by rw [Abbr ‘vsN’, Abbr ‘n'’]
+ >> NTAC 2 (POP_ASSUM (rfs o wrap))
+ (* reshaping and reordering assumptions *)
+ >> qunabbrev_tac ‘M1’
+ >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vsM)’
+ >> qunabbrev_tac ‘N1’
+ >> qabbrev_tac ‘N1 = principle_hnf (N0 @* MAP VAR vsN)’
+ >> Q.PAT_X_ASSUM ‘M0 = _’ ASSUME_TAC
+ >> Q.PAT_X_ASSUM ‘N0 = _’ ASSUME_TAC
+ >> Q.PAT_X_ASSUM ‘M1 = _’ ASSUME_TAC
+ >> Q.PAT_X_ASSUM ‘N1 = _’ ASSUME_TAC
+ >> ‘VAR y1 = y’  by rw [Abbr ‘y’ , absfree_hnf_head]
+ >> ‘VAR y2 = y'’ by rw [Abbr ‘y'’, absfree_hnf_head]
  (* cleanup MAX and vsN *)
  >> ‘MAX n n' = n'’ by rw [MAX_DEF]
  >> POP_ASSUM (REV_FULL_SIMP_TAC std_ss o wrap)
@@ -1376,14 +1560,14 @@ Proof
      [ (* 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) \\
+       CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
                     qunabbrev_tac ‘N0’ >> MATCH_MP_TAC lameq_SYM \\
                     MATCH_MP_TAC lameq_principle_hnf_reduce >> 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 []) \\
+       CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> art []) \\
        SIMP_TAC (srw_ss()) [Abbr ‘p1’] (* f4 (f3 (f2 (f1 N1))) == Q *) \\
     (* eliminating f1 *)
       ‘f1 N1 = VAR y2 @* (MAP f1 args2)’
@@ -1413,7 +1597,7 @@ Proof
        (* 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) \\
+       CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
                     qunabbrev_tac ‘M0’ \\
                     MATCH_MP_TAC lameq_SYM \\
                     MATCH_MP_TAC lameq_principle_hnf_reduce >> art [GSYM solvable_iff_has_hnf]) \\
@@ -1421,7 +1605,7 @@ Proof
        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 []) \\
+       CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> art []) \\
        SIMP_TAC (srw_ss()) [Abbr ‘p1’] (* f4 (f3 (f2 (f1 M1))) == P *) \\
     (* eliminating f1 *)
        MATCH_MP_TAC lameq_TRANS \\
@@ -1440,9 +1624,8 @@ Proof
        >- (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' \\
+           Q.PAT_X_ASSUM ‘DISJOINT (set Z) (FV P UNION FV Q)’ MP_TAC \\
+           rw [DISJOINT_ALT'] >> METIS_TAC []) >> Rewr' \\
     (* eliminating f3 *)
        Know ‘f3 ([VAR z2/y2] P) = [VAR z2/y2] P’
        >- (qunabbrev_tac ‘f3’ \\
@@ -1503,7 +1686,7 @@ Proof
      [ (* 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) \\
+       CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
                     qunabbrev_tac ‘M0’ >> MATCH_MP_TAC lameq_SYM \\
                     MATCH_MP_TAC lameq_principle_hnf_reduce \\
                     ASM_REWRITE_TAC [GSYM solvable_iff_has_hnf]) \\
@@ -1511,12 +1694,12 @@ Proof
        MATCH_MP_TAC lameq_TRANS \\
        Q.EXISTS_TAC ‘apply pi (y' @* args1')’ \\
        reverse CONJ_TAC >- art [] \\
-       MATCH_MP_TAC lameq_apply_cong \\
+       MATCH_MP_TAC Boehm_apply_lameq_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) \\
+       CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
                     qunabbrev_tac ‘N0’ >> MATCH_MP_TAC lameq_SYM \\
                     MATCH_MP_TAC lameq_principle_hnf_reduce \\
                     ASM_REWRITE_TAC [GSYM solvable_iff_has_hnf]) \\
@@ -1524,7 +1707,7 @@ Proof
        MATCH_MP_TAC lameq_TRANS \\
        Q.EXISTS_TAC ‘apply pi (y @* args2)’ \\
        reverse CONJ_TAC >- art [] \\
-       MATCH_MP_TAC lameq_apply_cong \\
+       MATCH_MP_TAC Boehm_apply_lameq_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
@@ -1578,7 +1761,7 @@ Proof
  (* stage work *)
  >> MATCH_MP_TAC lameq_TRANS
  >> Q.EXISTS_TAC ‘apply pi M0’
- >> CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> art [])
+ >> CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_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)))’
diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml
index 0c940c17ca..723d20755c 100644
--- a/examples/lambda/barendregt/chap2Script.sml
+++ b/examples/lambda/barendregt/chap2Script.sml
@@ -4,7 +4,8 @@
 
 open HolKernel Parse boolLib bossLib;
 
-open pred_setTheory pred_setLib listTheory finite_mapTheory hurdUtils;
+open pred_setTheory pred_setLib listTheory rich_listTheory finite_mapTheory
+     arithmeticTheory hurdUtils;
 
 open termTheory BasicProvers nomsetTheory binderLib appFOLDLTheory;
 
@@ -375,20 +376,11 @@ Theorem FV_I[simp]: FV I = {}
 Proof SRW_TAC [][I_def]
 QED
 
-Theorem I_alt :
+Theorem I_thm :
     !s. I = LAM s (VAR s)
 Proof
-    Q.X_GEN_TAC ‘x’
- >> REWRITE_TAC [I_def, Once EQ_SYM_EQ]
- >> Cases_on ‘x = "x"’ >- rw []
- >> qabbrev_tac ‘u :term = VAR x’
- >> qabbrev_tac ‘y = "x"’
- >> ‘y NOTIN FV u’ by rw [Abbr ‘u’]
- >> Know ‘LAM x u = LAM y ([VAR y/x] u)’
- >- (MATCH_MP_TAC SIMPLE_ALPHA >> art [])
- >> Rewr'
- >> Suff ‘[VAR y/x] u = VAR y’ >- rw []
- >> rw [Abbr ‘u’]
+    rw [I_def, Once EQ_SYM_EQ]
+ >> Cases_on ‘s = "x"’ >> rw [LAM_eq_thm]
 QED
 
 Theorem SUB_I[simp] :
@@ -403,6 +395,14 @@ Proof
     rw [ssub_value]
 QED
 
+Theorem I_cases :
+    !Y t. I = LAM Y t ==> t = VAR Y
+Proof
+    rw [I_def]
+ >> qabbrev_tac ‘X = "x"’
+ >> Cases_on ‘X = Y’ >> fs [LAM_eq_thm]
+QED
+
 val Omega_def =
     Define`Omega = (LAM "x" (VAR "x" @@ VAR "x")) @@
                      (LAM "x" (VAR "x" @@ VAR "x"))`
@@ -1149,6 +1149,195 @@ QED
 
 val _ = remove_ovl_mapping "Y" {Thy = "chap2", Name = "Y"}
 
+(*---------------------------------------------------------------------------*
+ *  More combinators
+ *---------------------------------------------------------------------------*)
+
+(* permutator [1, p.247] *)
+Definition permutator_def :
+    permutator n = let Z = FRESH_list (n + 1) {};
+                       z = LAST Z;
+                   in
+                       LAMl Z (VAR z @* MAP VAR (FRONT Z))
+End
+
+Theorem closed_permutator :
+    !n. closed (permutator n)
+Proof
+    rw [closed_def, permutator_def, FV_LAMl]
+ >> qabbrev_tac ‘Z = FRESH_list (n + 1) {}’
+ >> ‘ALL_DISTINCT Z /\ LENGTH Z = n + 1’ by rw [FRESH_list_def, Abbr ‘Z’]
+ >> ‘Z <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
+ >> qabbrev_tac ‘z = LAST Z’
+ >> ‘MEM z Z’ by rw [Abbr ‘z’, MEM_LAST_NOT_NIL]
+ >> Suff ‘FV (VAR z @* MAP VAR (FRONT Z)) SUBSET set Z’ >- SET_TAC []
+ >> rw [FV_appstar, SUBSET_DEF, MEM_MAP] >- art []
+ >> rfs [MEM_FRONT_NOT_NIL]
+QED
+
+(* |- !n. FV (permutator n) = {} *)
+Theorem FV_permutator[simp] = REWRITE_RULE [closed_def] closed_permutator
+
+Theorem permutator_thm :
+    !n N Ns. LENGTH Ns = n ==> permutator n @* Ns @@ N == N @* Ns
+Proof
+    RW_TAC std_ss [permutator_def]
+ >> qabbrev_tac ‘n = LENGTH Ns’
+ >> qabbrev_tac ‘Z = FRESH_list (n + 1) {}’
+ >> ‘ALL_DISTINCT Z /\ LENGTH Z = n + 1’ by rw [FRESH_list_def, Abbr ‘Z’]
+ >> ‘Z <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
+ >> qabbrev_tac ‘z = LAST Z’
+ >> ‘MEM z Z’ by rw [Abbr ‘z’, MEM_LAST_NOT_NIL]
+ >> qabbrev_tac ‘M = VAR z @* MAP VAR (FRONT Z)’
+ (* preparing for LAMl_ALPHA_ssub *)
+ >> qabbrev_tac
+     ‘Y = FRESH_list (n + 1) (set Z UNION (BIGUNION (IMAGE FV (set Ns))))’
+ >> Know ‘FINITE (set Z UNION (BIGUNION (IMAGE FV (set Ns))))’
+ >- (rw [] >> rw [FINITE_FV])
+ >> DISCH_TAC
+ >> Know ‘ALL_DISTINCT Y /\
+          DISJOINT (set Y) (set Z UNION (BIGUNION (IMAGE FV (set Ns)))) /\
+          LENGTH Y = n + 1’
+ >- (ASM_SIMP_TAC std_ss [FRESH_list_def, Abbr ‘Y’])
+ >> rw []
+ (* applying LAMl_ALPHA_ssub *)
+ >> Know ‘LAMl Z M = LAMl Y ((FEMPTY |++ ZIP (Z,MAP VAR Y)) ' M)’
+ >- (MATCH_MP_TAC LAMl_ALPHA_ssub >> rw [DISJOINT_SYM] \\
+     Suff ‘FV M = set Z’ >- METIS_TAC [DISJOINT_SYM] \\
+     rw [Abbr ‘M’, FV_appstar] \\
+    ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_LAST_FRONT] \\
+     POP_ORW \\
+     simp [LIST_TO_SET_SNOC] \\
+     rw [Once EXTENSION, MEM_MAP] \\
+     EQ_TAC >> rw [] >> fs [] \\
+     DISJ2_TAC \\
+     Q.EXISTS_TAC ‘FV (VAR x)’ >> rw [] \\
+     Q.EXISTS_TAC ‘VAR x’ >> rw [])
+ >> Rewr'
+ >> ‘Y <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
+ >> REWRITE_TAC [GSYM fromPairs_def]
+ >> qabbrev_tac ‘fm = fromPairs Z (MAP VAR Y)’
+ >> ‘FDOM fm = set Z’ by rw [FDOM_fromPairs, Abbr ‘fm’]
+ >> qabbrev_tac ‘y = LAST Y’
+ (* postfix for LAMl_ALPHA_ssub *)
+ >> ‘!t. LAMl Y t = LAMl (SNOC y (FRONT Y)) t’
+       by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_LAST_FRONT]) >> POP_ORW
+ >> REWRITE_TAC [LAMl_SNOC]
+ >> Know ‘fm ' M = VAR y @* MAP VAR (FRONT Y)’
+ >- (simp [Abbr ‘M’, ssub_appstar] \\
+     Know ‘fm ' z = VAR y’
+     >- (rw [Abbr ‘fm’, Abbr ‘z’, LAST_EL] \\
+         Know ‘fromPairs Z (MAP VAR Y) ' (EL (PRE (n + 1)) Z) =
+               EL (PRE (n + 1)) (MAP VAR Y)’
+         >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\
+         rw [EL_MAP, Abbr ‘y’, LAST_EL]) >> Rewr' \\
+     Suff ‘MAP ($' fm) (MAP VAR (FRONT Z)) = MAP VAR (FRONT Y)’ >- rw [] \\
+     rw [LIST_EQ_REWRITE, LENGTH_FRONT] \\
+    ‘PRE (n + 1) = n’ by rw [] >> POP_ASSUM (fs o wrap) \\
+     rename1 ‘i < n’ \\
+     simp [EL_MAP, LENGTH_FRONT] \\
+     Know ‘MEM (EL i (FRONT Z)) Z’
+     >- (rw [MEM_EL] \\
+         Q.EXISTS_TAC ‘i’ >> rw [] \\
+         MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) \\
+     rw [Abbr ‘fm’] \\
+     Know ‘EL i (FRONT Z) = EL i Z’
+     >- (MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) >> Rewr' \\
+     Know ‘EL i (FRONT Y) = EL i Y’
+     >- (MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) >> Rewr' \\
+     Know ‘fromPairs Z (MAP VAR Y) ' (EL i Z) = EL i (MAP VAR Y)’
+     >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\
+     rw [EL_MAP])
+ >> Rewr'
+ (* stage work *)
+ >> qabbrev_tac ‘t = LAM y (VAR y @* MAP VAR (FRONT Y))’
+ >> MATCH_MP_TAC lameq_TRANS
+ >> Q.EXISTS_TAC ‘((FEMPTY |++ ZIP (FRONT Y,Ns)) ' t) @@ N’
+ >> CONJ_TAC
+ >- (MATCH_MP_TAC lameq_APPL \\
+     MATCH_MP_TAC lameq_LAMl_appstar_ssub \\
+     rw [ALL_DISTINCT_FRONT, LENGTH_FRONT] \\
+     MATCH_MP_TAC DISJOINT_SUBSET' \\
+     Q.EXISTS_TAC ‘set Y’ \\
+     reverse CONJ_TAC >- rw [SUBSET_DEF, MEM_FRONT_NOT_NIL] \\
+     ONCE_REWRITE_TAC [DISJOINT_SYM] \\
+     FIRST_X_ASSUM MATCH_MP_TAC \\
+     Q.EXISTS_TAC ‘x’ >> art [])
+ (* cleanup ‘fm’ *)
+ >> Q.PAT_X_ASSUM ‘FDOM fm = set Z’ K_TAC
+ >> qunabbrev_tac ‘fm’
+ (* stage work *)
+ >> REWRITE_TAC [GSYM fromPairs_def]
+ >> qabbrev_tac ‘fm = fromPairs (FRONT Y) Ns’
+ >> ‘FDOM fm = set (FRONT Y)’ by rw [Abbr ‘fm’, FDOM_fromPairs, LENGTH_FRONT]
+ >> qunabbrev_tac ‘t’
+ >> qabbrev_tac ‘t = VAR y @* MAP VAR (FRONT Y)’
+ >> Know ‘fm ' (LAM y t) = LAM y (fm ' t)’
+ >- (MATCH_MP_TAC ssub_LAM \\
+     simp [Abbr ‘y’, LAST_EL] \\
+     CONJ_TAC
+     >- (simp [MEM_EL, LENGTH_FRONT, GSYM ADD1] \\
+         Q.X_GEN_TAC ‘i’ \\
+         ONCE_REWRITE_TAC [DECIDE “P ==> ~Q <=> Q ==> ~P”] \\
+         DISCH_TAC \\
+         Know ‘EL i (FRONT Y) = EL i Y’
+         >- (MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ, GSYM ADD1]) >> Rewr' \\
+         rw [ALL_DISTINCT_EL_IMP]) \\
+     Q.X_GEN_TAC ‘y’ \\
+     rw [MEM_EL, GSYM ADD1] >> rename1 ‘i < LENGTH (FRONT Y)’ \\
+     qunabbrev_tac ‘fm’ \\
+     Know ‘fromPairs (FRONT Y) Ns ' (EL i (FRONT Y)) = EL i Ns’
+     >- (MATCH_MP_TAC fromPairs_FAPPLY_EL \\
+         rw [ALL_DISTINCT_FRONT, LENGTH_FRONT]) >> Rewr' \\
+     Know ‘DISJOINT (FV (EL i Ns)) (set Y)’
+     >- (FIRST_X_ASSUM MATCH_MP_TAC \\
+         Q.EXISTS_TAC ‘EL i Ns’ >> rw [MEM_EL] \\
+         Q.EXISTS_TAC ‘i’ >> rfs [LENGTH_FRONT]) \\
+     ONCE_REWRITE_TAC [DISJOINT_SYM] \\
+     rw [DISJOINT_ALT] \\
+     POP_ASSUM MATCH_MP_TAC >> rw [MEM_EL] \\
+     Q.EXISTS_TAC ‘n’ >> rw [])
+ >> Rewr'
+ >> Q.PAT_X_ASSUM ‘FDOM fm = set (FRONT Y)’ K_TAC
+ >> simp [Abbr ‘fm’]
+ >> ‘FDOM (fromPairs (FRONT Y) Ns) = set (FRONT Y)’
+       by rw [FDOM_fromPairs, LENGTH_FRONT]
+ >> Know ‘~MEM y (FRONT Y)’
+ >- (simp [Abbr ‘y’, MEM_EL, LAST_EL, LENGTH_FRONT, GSYM ADD1] \\
+     Q.X_GEN_TAC ‘i’ \\
+     ONCE_REWRITE_TAC [DECIDE “P ==> ~Q <=> Q ==> ~P”] \\
+     DISCH_TAC \\
+     Know ‘EL i (FRONT Y) = EL i Y’
+     >- (MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) >> Rewr' \\
+     rw [ALL_DISTINCT_EL_IMP])
+ >> DISCH_TAC
+ >> simp [Abbr ‘t’, ssub_appstar]
+ >> Know ‘MAP ($' (fromPairs (FRONT Y) Ns)) (MAP VAR (FRONT Y)) = Ns’
+ >- (rw [LIST_EQ_REWRITE, LENGTH_FRONT] \\
+     rw [MAP_MAP_o, LENGTH_FRONT, EL_MAP]
+     >- (MATCH_MP_TAC fromPairs_FAPPLY_EL \\
+         rw [LENGTH_FRONT, ALL_DISTINCT_FRONT]) \\
+     NTAC 2 (POP_ASSUM MP_TAC) \\
+     simp [GSYM ADD1, MEM_EL, LENGTH_FRONT] \\
+     METIS_TAC [])
+ >> Rewr'
+ >> Suff ‘N @* Ns = [N/y] (VAR y @* Ns)’
+ >- (Rewr' >> rw [lameq_BETA])
+ >> simp [appstar_SUB]
+ >> Suff ‘MAP [N/y] Ns = Ns’ >- rw []
+ >> rw [LIST_EQ_REWRITE, EL_MAP]
+ >> rename1 ‘i < n’
+ >> MATCH_MP_TAC lemma14b
+ >> Know ‘DISJOINT (FV (EL i Ns)) (set Y)’
+ >- (FIRST_X_ASSUM MATCH_MP_TAC \\
+     Q.EXISTS_TAC ‘EL i Ns’ >> rw [MEM_EL] \\
+     Q.EXISTS_TAC ‘i’ >> art [])
+ >> ONCE_REWRITE_TAC [DISJOINT_SYM]
+ >> rw [DISJOINT_ALT]
+ >> POP_ASSUM MATCH_MP_TAC
+ >> rw [Abbr ‘y’, MEM_LAST_NOT_NIL]
+QED
+
 (* ----------------------------------------------------------------------
     closed terms and closures of (open or closed) terms, leading into
     B's Chapter 2's section “Solvable and unsolvable terms” p41.
@@ -1238,8 +1427,6 @@ QED
 (* 8.3.1 (iii) [1, p.171] *)
 Overload unsolvable = “\M. ~solvable M”
 
-
-
 val _ = export_theory()
 val _ = html_theory "chap2";
 
diff --git a/examples/lambda/barendregt/head_reductionScript.sml b/examples/lambda/barendregt/head_reductionScript.sml
index 12e4b4ab33..f59523ffe1 100644
--- a/examples/lambda/barendregt/head_reductionScript.sml
+++ b/examples/lambda/barendregt/head_reductionScript.sml
@@ -1375,10 +1375,36 @@ Proof
  >> rw [appstar_SNOC]
 QED
 
-(* Another variant of ‘hnf_cases’ with a given (shared) list of fresh variables
+(*---------------------------------------------------------------------------*
+ *  hnf_children_size (of hnf)
+ *---------------------------------------------------------------------------*)
 
-   NOTE: "irule (iffLR hnf_cases_shared)" is a useful tactic for this theorem.
- *)
+val (hnf_children_size_thm, _) = define_recursive_term_function
+   ‘(hnf_children_size ((VAR :string -> term) s) = 0) /\
+    (hnf_children_size (t1 @@ t2) = 1 + hnf_children_size t1) /\
+    (hnf_children_size (LAM v t) = hnf_children_size t)’;
+
+val _ = export_rewrites ["hnf_children_size_thm"];
+
+Theorem hnf_children_size_LAMl[simp] :
+    hnf_children_size (LAMl vs t) = hnf_children_size t
+Proof
+    Induct_on ‘vs’ >> rw []
+QED
+
+Theorem hnf_children_size_hnf[simp] :
+    hnf_children_size (LAMl vs (VAR y @* Ms)) = LENGTH Ms
+Proof
+    rw []
+ >> Induct_on ‘Ms’ using SNOC_INDUCT >- rw []
+ >> rw [appstar_SNOC]
+QED
+
+(*---------------------------------------------------------------------------*
+ *  hnf_cases_shared - ‘hnf_cases’ with a given list of fresh variables
+ *---------------------------------------------------------------------------*)
+
+(* NOTE: "irule (iffLR hnf_cases_shared)" is a useful tactic *)
 Theorem hnf_cases_shared :
     !vs M. ALL_DISTINCT vs /\ LAMl_size M <= LENGTH vs /\
            DISJOINT (set vs) (FV M) ==>
diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml
index 86657898f8..90fa8ebd07 100644
--- a/examples/lambda/barendregt/solvableScript.sml
+++ b/examples/lambda/barendregt/solvableScript.sml
@@ -56,7 +56,7 @@ Proof
     Know ‘closure (VAR x) = LAM x (VAR x)’
  >- (MATCH_MP_TAC closure_open_sing >> rw [])
  >> Rewr'
- >> REWRITE_TAC [Q.SPEC ‘x’ I_alt]
+ >> REWRITE_TAC [Q.SPEC ‘x’ I_thm]
 QED
 
 Theorem closures_imp_closed :
@@ -1062,7 +1062,7 @@ Theorem lameq_principle_hnf_lemma :
                 M1 = principle_hnf (M @* MAP VAR vs);
                 N1 = principle_hnf (N @* MAP VAR vs)
             in
-                hnf_headvar M1 = hnf_headvar N1 /\
+                hnf_head M1 = hnf_head N1 /\
                 LENGTH (hnf_children M1) = LENGTH (hnf_children N1) /\
                 !i. i < LENGTH (hnf_children M1) ==>
                     EL i (hnf_children M1) == EL i (hnf_children N1)
@@ -1166,7 +1166,7 @@ Theorem lameq_principle_hnf_headvar_eq :
          n = LAMl_size M0 /\ vs = FRESH_list n X /\
          M1 = principle_hnf (M0 @* MAP VAR vs) /\
          N1 = principle_hnf (N0 @* MAP VAR vs)
-     ==> hnf_headvar M1 = hnf_headvar N1
+     ==> hnf_head M1 = hnf_head N1
 Proof
     RW_TAC std_ss [UNION_SUBSET]
  >> qabbrev_tac ‘M0 = principle_hnf M’
@@ -1205,7 +1205,7 @@ Theorem lameq_principle_hnf_thm :
          M1 = principle_hnf (M0 @* MAP VAR vs) /\
          N1 = principle_hnf (N0 @* MAP VAR vs)
      ==> LAMl_size M0 = LAMl_size N0 /\
-         hnf_headvar M1 = hnf_headvar N1 /\
+         hnf_head M1 = hnf_head N1 /\
          LENGTH (hnf_children M1) = LENGTH (hnf_children N1) /\
          !i. i < LENGTH (hnf_children M1) ==>
              EL i (hnf_children M1) == EL i (hnf_children N1)
diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml
index a039ceee98..4a4ae1ef3d 100644
--- a/examples/lambda/basics/appFOLDLScript.sml
+++ b/examples/lambda/basics/appFOLDLScript.sml
@@ -1,6 +1,7 @@
 open HolKernel Parse boolLib bossLib;
 
-open arithmeticTheory listTheory rich_listTheory pred_setTheory hurdUtils;
+open arithmeticTheory listTheory rich_listTheory pred_setTheory finite_mapTheory
+     hurdUtils;
 
 open termTheory binderLib;
 
@@ -57,18 +58,7 @@ val take_lemma = prove(
   ``∀l n. 0 < n ∧ n ≤ LENGTH l ⇒ TAKE n l ≠ []``,
   Induct THEN SRW_TAC [ARITH_ss][]);
 
-val _ = augment_srw_ss[rewrites[listTheory.TAKE_def,listTheory.DROP_def]];
-
-val DROP_PREn_LAST_CONS = store_thm(
-  "DROP_PREn_LAST_CONS",
-  ``∀t n. 0 < n ∧ n ≤ LENGTH t ⇒
-          (DROP (n - 1) t = LAST (TAKE n t) :: DROP n t)``,
-  Induct THEN SRW_TAC [ARITH_ss][] THENL [
-    `n = 1` by DECIDE_TAC THEN SRW_TAC [][],
-    `n = 1` by DECIDE_TAC THEN SRW_TAC [][],
-    `(t = []) ∨ ∃h t0. t = h :: t0` by METIS_TAC [listTheory.list_CASES] THEN
-    FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) []
-  ]);
+val _ = augment_srw_ss[rewrites[TAKE_def, DROP_def]];
 
 val appstar_eq_appstar = store_thm(
   "appstar_eq_appstar",
@@ -326,6 +316,54 @@ Proof
   ]
 QED
 
+Theorem LAMl_ALPHA_ssub :
+    !vs vs' M.
+       LENGTH vs = LENGTH vs' /\ ALL_DISTINCT vs /\ ALL_DISTINCT vs' /\
+       DISJOINT (LIST_TO_SET vs') (LIST_TO_SET vs UNION FV M) ==>
+       LAMl vs M = LAMl vs' ((FEMPTY |++ ZIP (vs, MAP VAR vs')) ' M)
+Proof
+    rpt STRIP_TAC
+ >> Suff ‘(FEMPTY |++ ZIP (vs, MAP VAR vs')) ' M =
+          M ISUB REVERSE (ZIP (MAP VAR vs', vs))’
+ >- (Rewr' >> MATCH_MP_TAC LAMl_ALPHA >> art [])
+ >> rpt (POP_ASSUM MP_TAC)
+ >> Q.ID_SPEC_TAC ‘vs'’
+ >> Q.ID_SPEC_TAC ‘vs’
+ >> Induct_on ‘vs’ >- rw [FUPDATE_LIST_THM, ISUB_def]
+ >> rw []
+ >> Cases_on ‘vs'’ >- fs []
+ >> fs [] >> rename1 ‘v # M’
+ (* RHS rewriting *)
+ >> REWRITE_TAC [GSYM ISUB_APPEND, GSYM SUB_ISUB_SINGLETON]
+ (* LHS rewriting *)
+ >> rw [FUPDATE_LIST_THM]
+ >> Know ‘(FEMPTY :string |-> term) |+ (h,VAR v) |++ ZIP (vs,MAP VAR t) =
+          (FEMPTY |++ ZIP (vs,MAP VAR t)) |+ (h,VAR v)’
+ >- (MATCH_MP_TAC FUPDATE_FUPDATE_LIST_COMMUTES \\
+     rw [MAP_ZIP])
+ >> Rewr'
+ >> qabbrev_tac ‘fm = (FEMPTY :string |-> term) |++ ZIP (vs,MAP VAR t)’
+ >> ‘FDOM fm = set vs’ by (rw [Abbr ‘fm’, FDOM_FUPDATE_LIST, MAP_ZIP])
+ (* applying ssub_update_apply_SUBST' *)
+ >> Know ‘(fm |+ (h,VAR v)) ' M = [fm ' (VAR v)/h] (fm ' M)’
+ >- (MATCH_MP_TAC ssub_update_apply_SUBST' >> rw [] \\
+    ‘fm = fromPairs vs (MAP VAR t)’ by rw [Abbr ‘fm’, fromPairs_def] \\
+     POP_ORW \\
+     Q.PAT_X_ASSUM ‘MEM k vs’ MP_TAC >> rw [MEM_EL] \\
+     Know ‘fromPairs vs (MAP VAR t) ' (EL n vs) = EL n (MAP VAR t)’
+     >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\
+     rw [EL_MAP] \\
+     Q.PAT_X_ASSUM ‘~MEM h t’ MP_TAC >> rw [MEM_EL] \\
+     POP_ASSUM (MP_TAC o (Q.SPEC ‘n’)) >> rw [])
+ >> Rewr'
+ >> Know ‘fm ' (VAR v) = VAR v’
+ >- (MATCH_MP_TAC ssub_14b >> rw [GSYM DISJOINT_DEF])
+ >> Rewr'
+ >> Suff ‘fm ' M = M ISUB REVERSE (ZIP (MAP VAR t,vs))’ >- rw []
+ >> qunabbrev_tac ‘fm’
+ >> FIRST_X_ASSUM irule >> rw []
+QED
+
 Theorem LAMl_SNOC[simp] :
     LAMl (SNOC v vs) t = LAMl vs (LAM v t)
 Proof
diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml
index cc54cf1e7e..6d7144d665 100644
--- a/examples/lambda/basics/termScript.sml
+++ b/examples/lambda/basics/termScript.sml
@@ -463,6 +463,9 @@ val SUB_THM = save_thm(
 val _ = export_rewrites ["SUB_THM"]
 val SUB_VAR = save_thm("SUB_VAR", hd (CONJUNCTS SUB_DEF))
 
+(* |- !v u N t. v <> u /\ v # N ==> [N/u] (LAM v t) = LAM v ([N/u] t) *)
+Theorem SUB_LAM = List.nth (CONJUNCTS SUB_DEF, 2)
+
 (* ----------------------------------------------------------------------
     Results about substitution
    ---------------------------------------------------------------------- *)
@@ -1082,6 +1085,402 @@ Proof
  >> fs [closed_def, DISJOINT_DEF]
 QED
 
+Theorem ssub_reduce_thm :
+    !t. FV t INTER FDOM fm = {s} ==> fm ' t = [fm ' s/s] t
+Proof
+    HO_MATCH_MP_TAC nc_INDUCTION2
+ >> Q.EXISTS_TAC ‘fmFV fm UNION {s}’
+ >> rw [SUB_THM, ssub_thm]
+ >- (‘s' = s’ by ASM_SET_TAC [] >> fs [])
+ >- (‘s' = s’ by ASM_SET_TAC [] >> fs [ssub_thm] \\
+     ‘s IN FDOM fm’ by ASM_SET_TAC [])
+ >- (‘FV t INTER FDOM fm = {s} \/ FV t INTER FDOM fm = {}’ by ASM_SET_TAC []
+     >- rw [] \\
+     rw [ssub_14b] \\
+     MATCH_MP_TAC (GSYM lemma14b) \\
+     ASM_SET_TAC [])
+ >- (‘FV t' INTER FDOM fm = {s} \/ FV t' INTER FDOM fm = {}’ by ASM_SET_TAC []
+     >- rw [] \\
+     rw [ssub_14b] \\
+     MATCH_MP_TAC (GSYM lemma14b) \\
+     ASM_SET_TAC [])
+ >> ‘s IN FDOM fm’ by ASM_SET_TAC []
+ >> Know ‘[fm ' s/s] (LAM y t) = LAM y ([fm ' s/s] t)’
+ >- (MATCH_MP_TAC SUB_LAM >> rw [])
+ >> Rewr'
+ >> rw []
+ >> FIRST_X_ASSUM MATCH_MP_TAC
+ >> ASM_SET_TAC []
+QED
+
+Theorem ssub_reduce :
+    !t. FV t = {s} /\ s IN FDOM fm ==> fm ' t = [fm ' s/s] t
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC ssub_reduce_thm
+ >> ASM_SET_TAC []
+QED
+
+(* ----------------------------------------------------------------------
+    Simultaneous substitution given by a pair of key list and value list
+   ---------------------------------------------------------------------- *)
+
+(* from a key list and a value list (of same length) to an alist *)
+Definition fromPairs_def :
+    fromPairs (Xs :string list) (Ps :term list) = FEMPTY |++ ZIP (Xs,Ps)
+End
+
+Theorem fromPairs_single :
+    !X E E'. ssub (fromPairs [X] [E']) E = [E'/X] E
+Proof
+    RW_TAC list_ss [fromPairs_def, ZIP, FUPDATE_LIST_THM]
+ >> rw [FEMPTY_update_apply]
+QED
+
+Theorem fromPairs_EMPTY :
+    fromPairs [] [] = FEMPTY
+Proof
+    SRW_TAC [] [fromPairs_def, FUPDATE_LIST_THM]
+QED
+
+Theorem fromPairs_HD :
+    !X Xs P Ps. ~MEM X Xs /\ LENGTH Ps = LENGTH Xs ==>
+                fromPairs (X::Xs) (P::Ps) = fromPairs Xs Ps |+ (X,P)
+Proof
+    SRW_TAC [] [fromPairs_def, FUPDATE_LIST_THM]
+ >> MATCH_MP_TAC FUPDATE_FUPDATE_LIST_COMMUTES
+ >> METIS_TAC [MAP_ZIP]
+QED
+
+Theorem FDOM_fromPairs :
+    !Xs Ps. LENGTH Ps = LENGTH Xs ==> FDOM (fromPairs Xs Ps) = set Xs
+Proof
+    SRW_TAC [] [fromPairs_def, FDOM_FUPDATE_LIST, MAP_ZIP]
+QED
+
+Theorem fromPairs_DOMSUB_NOT_IN_DOM :
+    !X Xs Ps. ~MEM X Xs /\ (LENGTH Ps = LENGTH Xs) ==>
+              fromPairs Xs Ps \\ X = fromPairs Xs Ps
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC DOMSUB_NOT_IN_DOM
+ >> fs [FDOM_fromPairs]
+QED
+
+Theorem fromPairs_FAPPLY_HD :
+    !X Xs P Ps n. ~MEM X Xs /\ ALL_DISTINCT Xs /\ (LENGTH Ps = LENGTH Xs) ==>
+                  fromPairs (X::Xs) (P::Ps) ' X = P
+Proof
+    RW_TAC std_ss [fromPairs_HD, FAPPLY_FUPDATE]
+QED
+
+Theorem fromPairs_FAPPLY_EL :
+    !Xs Ps n. ALL_DISTINCT Xs /\ LENGTH Ps = LENGTH Xs /\ n < LENGTH Xs ==>
+              fromPairs Xs Ps ' (EL n Xs) = EL n Ps
+Proof
+    RW_TAC std_ss [fromPairs_def]
+ >> MATCH_MP_TAC FUPDATE_LIST_APPLY_MEM
+ >> Q.EXISTS_TAC `n`
+ >> fs [LENGTH_ZIP, MAP_ZIP]
+ >> RW_TAC list_ss []
+ >> CCONTR_TAC >> fs []
+ >> `n < LENGTH Xs /\ m <> n` by RW_TAC arith_ss []
+ >> METIS_TAC [ALL_DISTINCT_EL_IMP]
+QED
+
+Theorem fromPairs_FAPPLY_EL' :
+    !X P Xs Ps n. ~MEM X Xs /\ ALL_DISTINCT Xs /\ LENGTH Ps = LENGTH Xs /\
+                  n < LENGTH Xs
+              ==> fromPairs (X::Xs) (P::Ps) ' (EL n Xs) = EL n Ps
+Proof
+    RW_TAC std_ss [fromPairs_HD, fromPairs_def]
+ >> Know `((FEMPTY |++ ZIP (Xs,Ps)) |+ (X,P)) = ((FEMPTY |+ (X,P)) |++ ZIP (Xs,Ps))`
+ >- (MATCH_MP_TAC EQ_SYM \\
+     MATCH_MP_TAC FUPDATE_FUPDATE_LIST_COMMUTES \\
+     fs [MAP_ZIP])
+ >> Rewr'
+ >> MATCH_MP_TAC FUPDATE_LIST_APPLY_MEM
+ >> Q.EXISTS_TAC `n`
+ >> fs [LENGTH_ZIP, MAP_ZIP]
+ >> RW_TAC list_ss []
+ >> CCONTR_TAC >> fs []
+ >> `n < LENGTH Xs /\ m <> n` by RW_TAC arith_ss []
+ >> METIS_TAC [ALL_DISTINCT_EL_IMP]
+QED
+
+Theorem fromPairs_elim :
+    !Xs Ps E. DISJOINT (FV E) (set Xs) /\ LENGTH Ps = LENGTH Xs ==>
+              fromPairs Xs Ps ' E = E
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC ssub_14b
+ >> fs [FDOM_fromPairs, DISJOINT_DEF]
+QED
+
+Theorem lemma0[local] :
+    !X P E fm. X NOTIN FDOM fm /\ DISJOINT (FDOM fm) (FV P) /\
+               FEVERY (\(k,v). X NOTIN (FV v)) fm ==>
+              (fm |+ (X,P)) ' E = [P/X] (fm ' E)
+Proof
+    rw []
+ (* applying ssub_update_apply_subst *)
+ >> Know ‘ssub (fm |+ (X,P)) E = [ssub fm P/X] (ssub fm E)’
+ >- (MATCH_MP_TAC ssub_update_apply_SUBST' >> fs [FEVERY_DEF])
+ >> Rewr'
+ >> Suff ‘ssub fm P = P’ >- rw []
+ >> MATCH_MP_TAC ssub_14b
+ >> rw [GSYM DISJOINT_DEF, DISJOINT_SYM]
+QED
+
+(* fromPairs_reduce leads to fromPairs_FOLDR
+
+   NOTE: added ‘DISJOINT (set Xs) (FV P)’ when switching to ‘ssub’
+ *)
+Theorem fromPairs_reduce :
+    !X Xs P Ps. ~MEM X Xs /\ ALL_DISTINCT Xs /\ LENGTH Ps = LENGTH Xs /\
+                EVERY (\e. X NOTIN (FV e)) Ps /\
+                DISJOINT (set Xs) (FV P) ==>
+         !E. fromPairs (X::Xs) (P::Ps) ' E = [P/X] (fromPairs Xs Ps ' E)
+Proof
+    rpt STRIP_TAC
+ >> Know `fromPairs (X::Xs) (P::Ps) = (fromPairs Xs Ps) |+ (X,P)`
+ >- (MATCH_MP_TAC fromPairs_HD >> art [])
+ >> Rewr'
+ >> MATCH_MP_TAC lemma0
+ >> fs [FDOM_fromPairs, FEVERY_DEF]
+ >> RW_TAC std_ss []
+ >> rename1 `MEM Y Xs`
+ >> `?n. n < LENGTH Xs /\ (Y = EL n Xs)` by PROVE_TAC [MEM_EL]
+ >> fs [fromPairs_FAPPLY_EL, EVERY_MEM]
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> rw [MEM_EL]
+ >> Q.EXISTS_TAC `n` >> art []
+QED
+
+(* fromPairs_reduce in another form *)
+Theorem lemma1[local] :
+   !E E' map.
+      map <> [] /\
+      ~MEM (FST (HD map)) (MAP FST (TL map)) /\
+      ALL_DISTINCT (MAP FST (TL map)) /\
+      DISJOINT (set (MAP FST (TL map))) (FV (SND (HD map))) /\
+      EVERY (\e. (FST (HD map)) NOTIN (FV e)) (MAP SND (TL map)) /\
+      (FEMPTY |++ (TL map)) ' E = E'
+   ==>
+      (FEMPTY |++ map) ' E = [SND (HD map)/FST (HD map)] E'
+Proof
+    rpt GEN_TAC
+ >> Cases_on `map` >- SRW_TAC [] []
+ >> RW_TAC std_ss [HD, TL]
+ >> Cases_on `h` >> fs []
+ >> Q.ABBREV_TAC `Xs = FST (UNZIP t)`
+ >> Q.ABBREV_TAC `Ps = SND (UNZIP t)`
+ >> Know `t = ZIP (Xs,Ps)`
+ >- (qunabbrevl_tac [`Xs`, `Ps`] >> fs [])
+ >> Know `LENGTH Ps = LENGTH Xs`
+ >- (qunabbrevl_tac [`Xs`, `Ps`] >> fs [])
+ >> RW_TAC std_ss []
+ >> Know `(MAP FST (ZIP (Xs,Ps))) = Xs` >- PROVE_TAC [MAP_ZIP]
+ >> DISCH_THEN (fs o wrap)
+ >> Know `(MAP SND (ZIP (Xs,Ps))) = Ps` >- PROVE_TAC [MAP_ZIP]
+ >> DISCH_THEN (fs o wrap)
+ >> rename1 ‘~MEM X Xs’
+ >> MP_TAC (REWRITE_RULE [fromPairs_def]
+                         (Q.SPECL [`X`,`Xs`,`r`,`Ps`] fromPairs_reduce))
+ >> simp []
+QED
+
+(* Let map = ZIP(Xs,Ps), to convert ssub to a folding of CCS_Subst, each P
+   of Ps must contains free variables up to the corresponding X of Xs.
+ *)
+Theorem lemma2[local] :
+    !E map. ALL_DISTINCT (MAP FST map) /\
+            EVERY (\(x,p). DISJOINT (set (MAP FST map)) (FV p)) map ==>
+           (ssub (FEMPTY |++ map) E =
+            FOLDR (\l e. [SND l/FST l] e) E map)
+Proof
+    GEN_TAC >> Induct_on `map`
+ >- SRW_TAC [] [FUPDATE_LIST_THM, ssub_FEMPTY]
+ >> rpt STRIP_TAC >> fs [MAP]
+ >> MP_TAC (Q.SPECL [`E`, `ssub (FEMPTY |++ map) E`,
+                     `h::map`] lemma1) >> fs []
+ >> Know ‘DISJOINT (set (MAP FST map)) (FV (SND h)) /\
+          EVERY (\e. FST h # e) (MAP SND map)’
+ >- (Cases_on ‘h’ >> fs [] \\
+     Q.PAT_X_ASSUM ‘EVERY (\(x,p). DISJOINT (set (MAP FST map)) (FV p) /\ q # p) map’
+       MP_TAC >> rw [EVERY_MEM, MEM_MAP] \\
+     Q.PAT_X_ASSUM ‘!e. MEM e map ==> _’ (MP_TAC o (Q.SPEC ‘y’)) \\
+     Cases_on ‘y’ >> rw [])
+ >> rw []
+ >> Cases_on `h` >> fs []
+ >> rename1 `X # P`
+ >> Suff ‘ssub (FEMPTY |++ map) E =
+          FOLDR (\l e. [SND l/FST l] e) E map’ >- rw []
+ >> FIRST_X_ASSUM MATCH_MP_TAC
+ >> Q.PAT_X_ASSUM
+     ‘EVERY (\(x,p). DISJOINT (set (MAP FST map)) (FV p) /\ X # p) map’ MP_TAC
+ >> rw [EVERY_MEM]
+ >> Q.PAT_X_ASSUM ‘!e. MEM e map ==> _’ (MP_TAC o (Q.SPEC ‘e’))
+ >> Cases_on ‘e’ >> rw []
+QED
+
+(* lemma2 in another form; this is less general than fromPairs_reduce *)
+Theorem fromPairs_FOLDR :
+    !Xs Ps E. ALL_DISTINCT Xs /\ LENGTH Ps = LENGTH Xs /\
+              EVERY (\p. DISJOINT (set Xs) (FV p)) Ps ==>
+              (fromPairs Xs Ps) ' E =
+              FOLDR (\(x,y) e. [y/x] e) E (ZIP (Xs,Ps))
+Proof
+    RW_TAC std_ss []
+ >> MP_TAC (Q.SPECL [`E`, `ZIP (Xs,Ps)`] lemma2)
+ >> RW_TAC std_ss [MAP_ZIP, fromPairs_def]
+ >> Know `(\l e. [SND l/FST l] e) = (\(x,y) e. [y/x] e)`
+ >- (rw [FUN_EQ_THM] >> Cases_on `l` >> rw [])
+ >> DISCH_THEN (fs o wrap)
+ >> POP_ASSUM MATCH_MP_TAC
+ >> POP_ASSUM MP_TAC >> rw [EVERY_MEM, MEM_ZIP]
+ >> simp []
+ >> FIRST_X_ASSUM MATCH_MP_TAC
+ >> rw [MEM_EL]
+ >> Q.EXISTS_TAC ‘n’ >> art []
+QED
+
+Theorem fromPairs_FOLDR' :
+    !Xs Ps E. ALL_DISTINCT Xs /\ LENGTH Ps = LENGTH Xs /\
+              EVERY (\p. DISJOINT (set Xs) (FV p)) Ps ==>
+              (fromPairs Xs Ps) ' E =
+              FOLDR (\(x,y) e. [y/x] e) E (ZIP (Xs,Ps))
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC fromPairs_FOLDR >> art []
+ >> fs [FEVERY_DEF, EVERY_MEM]
+ >> RW_TAC std_ss [MEM_ZIP]
+QED
+
+Theorem fromPairs_self :
+    !E Xs. ALL_DISTINCT Xs ==> fromPairs Xs (MAP VAR Xs) ' E = E
+Proof
+    Q.X_GEN_TAC ‘E’
+ >> Induct_on `Xs`
+ >> SRW_TAC [] [ssub_FEMPTY, fromPairs_EMPTY]
+ >> Q.PAT_X_ASSUM `ALL_DISTINCT Xs ==> _` MP_TAC
+ >> RW_TAC std_ss []
+ >> MP_TAC (Q.SPECL [`h`, `Xs`, `VAR h`, `MAP VAR Xs`] fromPairs_reduce)
+ >> `LENGTH (MAP VAR Xs) = LENGTH Xs` by PROVE_TAC [LENGTH_MAP]
+ >> simp []
+ >> Suff ‘EVERY (\e. h # e) (MAP VAR Xs)’
+ >- RW_TAC std_ss [EVERY_MEM, MEM_MAP]
+ >> rw [EVERY_MAP, EVERY_MEM, FV_thm]
+QED
+
+Theorem fromPairs_nested :
+    !Xs Ps Es E.
+        ALL_DISTINCT Xs /\ LENGTH Ps = LENGTH Xs /\ LENGTH Es = LENGTH Xs ==>
+        fromPairs Xs Ps ' (fromPairs Xs Es ' E) =
+        fromPairs Xs (MAP ($' (fromPairs Xs Ps)) Es) ' E
+Proof
+    Suff (* rewriting for induction *)
+   `!Xs Ps Es. ALL_DISTINCT Xs /\
+              (LENGTH Ps = LENGTH Xs) /\ (LENGTH Es = LENGTH Xs) ==>
+        !E. fromPairs Xs Ps ' (fromPairs Xs Es ' E) =
+            fromPairs Xs (MAP ($' (fromPairs Xs Ps)) Es) ' E`
+ >- METIS_TAC []
+ >> rpt GEN_TAC >> STRIP_TAC
+ >> HO_MATCH_MP_TAC nc_INDUCTION2
+ >> qabbrev_tac ‘fm2 = fromPairs Xs Ps’
+ >> Q.EXISTS_TAC ‘set Xs UNION BIGUNION (IMAGE FV (set Es))
+                         UNION BIGUNION (IMAGE FV (set Ps))
+                         UNION BIGUNION (IMAGE (\e. FV (ssub fm2 e)) (set Es))’
+ >> rw [Abbr ‘fm2’, FDOM_fromPairs] (* 5 subgoals *)
+ >> TRY (rw [FINITE_FV]) (* 2 subgoals left *)
+ >- (fs [MEM_EL] >> rename1 `X = EL n Xs` \\
+    `LENGTH (MAP (ssub (fromPairs Xs Ps)) Es) = LENGTH Xs`
+       by PROVE_TAC [LENGTH_MAP] \\
+     ASM_SIMP_TAC std_ss [fromPairs_FAPPLY_EL, EL_MAP])
+ >> `LENGTH (MAP (ssub (fromPairs Xs Ps)) Es) = LENGTH Xs`
+       by PROVE_TAC [LENGTH_MAP]
+ (* stage work *)
+ >> qabbrev_tac ‘fm1 = fromPairs Xs Es’
+ >> qabbrev_tac ‘fm2 = fromPairs Xs Ps’
+ (* applying ssub_rec *)
+ >> Know ‘ssub fm1 (LAM y E) = LAM y (ssub fm1 E)’
+ >- (MATCH_MP_TAC ssub_LAM >> rw [Abbr ‘fm1’, FDOM_fromPairs] \\
+     fs [MEM_EL] >> rename1 `X = EL n Xs` \\
+     ASM_SIMP_TAC std_ss [fromPairs_FAPPLY_EL, EL_MAP] \\
+     METIS_TAC [])
+ >> Rewr'
+ >> Know ‘ssub fm2 (LAM y (ssub fm1 E)) =
+          LAM y (ssub fm2 (ssub fm1 E))’
+ >- (MATCH_MP_TAC ssub_LAM >> rw [Abbr ‘fm2’, FDOM_fromPairs] \\
+     fs [MEM_EL] >> rename1 `X = EL n Xs` \\
+     ASM_SIMP_TAC std_ss [fromPairs_FAPPLY_EL, EL_MAP] \\
+     METIS_TAC [])
+ >> Rewr'
+ >> qabbrev_tac ‘fm3 = fromPairs Xs (MAP (ssub fm2) Es)’
+ >> Know ‘ssub fm3 (LAM y E) = LAM y (ssub fm3 E)’
+ >- (MATCH_MP_TAC ssub_LAM >> rw [Abbr ‘fm3’, FDOM_fromPairs] \\
+     FULL_SIMP_TAC std_ss [MEM_EL] >> rename1 `X = EL n Xs` \\
+     ASM_SIMP_TAC std_ss [fromPairs_FAPPLY_EL, EL_MAP] \\
+     (* NOTE: this is why we put
+          ‘BIGUNION (IMAGE (\e. FV (ssub fm2 e)) (set Es))’
+        into the exclusive set required by nc_INDUCTION2. *)
+     METIS_TAC [])
+ >> Rewr'
+ >> rw [LAM_eq_thm]
+QED
+
+(* A (non-trivial) generalization of FV_SUBSET *)
+Theorem FV_fromPairs :
+    !Xs Ps E. ALL_DISTINCT Xs /\ LENGTH Ps = LENGTH Xs ==>
+              FV (fromPairs Xs Ps ' E) SUBSET
+                 (FV E) UNION BIGUNION (IMAGE FV (set Ps))
+Proof
+    NTAC 2 GEN_TAC
+ >> HO_MATCH_MP_TAC nc_INDUCTION2
+ >> Q.EXISTS_TAC ‘set Xs UNION BIGUNION (IMAGE FV (set Ps))’
+ >> rw [FDOM_fromPairs, ssub_thm] (* 7 subgoals *)
+ >- (fs [MEM_EL, fromPairs_FAPPLY_EL] \\
+    `MEM (EL n Ps) Ps` by PROVE_TAC [MEM_EL] >> ASM_SET_TAC [])
+ >> TRY (rw [FINITE_FV] >> ASM_SET_TAC [])
+ >> qabbrev_tac ‘fm = fromPairs Xs Ps’
+ >> Know ‘ssub fm (LAM y E) = LAM y (ssub fm E)’
+ >- (MATCH_MP_TAC ssub_LAM \\
+     rw [Abbr ‘fm’, FDOM_fromPairs] \\
+     fs [MEM_EL, fromPairs_FAPPLY_EL] \\
+     METIS_TAC [])
+ >> Rewr'
+ >> fs [FV_thm]
+ >> qabbrev_tac ‘A = ssub fm E’
+ >> qabbrev_tac ‘B = BIGUNION (IMAGE FV (set Ps))’
+ >> Q.PAT_X_ASSUM ‘FV A SUBSET FV E UNION B’ MP_TAC
+ >> SET_TAC []
+QED
+
+(* A more precise estimation with `set Xs` *)
+Theorem FV_fromPairs' :
+    !Xs Ps E. ALL_DISTINCT Xs /\ LENGTH Ps = LENGTH Xs ==>
+              FV (fromPairs Xs Ps ' E) SUBSET
+                 ((FV E) DIFF (set Xs)) UNION BIGUNION (IMAGE FV (set Ps))
+Proof
+    NTAC 2 GEN_TAC
+ >> HO_MATCH_MP_TAC nc_INDUCTION2
+ >> Q.EXISTS_TAC ‘set Xs UNION BIGUNION (IMAGE FV (set Ps))’
+ >> rw [FDOM_fromPairs, ssub_thm] (* 7 subgoals *)
+ >- (fs [MEM_EL, fromPairs_FAPPLY_EL] \\
+    `MEM (EL n Ps) Ps` by PROVE_TAC [MEM_EL] >> ASM_SET_TAC [])
+ >> TRY (rw [FINITE_FV] >> ASM_SET_TAC [])
+ >> qabbrev_tac ‘fm = fromPairs Xs Ps’
+ >> Know ‘ssub fm (LAM y E) = LAM y (ssub fm E)’
+ >- (MATCH_MP_TAC ssub_LAM \\
+     rw [Abbr ‘fm’, FDOM_fromPairs] \\
+     fs [MEM_EL, fromPairs_FAPPLY_EL] \\
+     METIS_TAC []) >> Rewr'
+ >> fs [FV_thm]
+ >> qabbrev_tac ‘A = fm ' E’
+ >> qabbrev_tac ‘B = BIGUNION (IMAGE FV (set Ps))’
+ >> Q.PAT_X_ASSUM ‘FV A SUBSET FV E DIFF set Xs UNION B’ MP_TAC
+ >> SET_TAC []
+QED
+
 (* ----------------------------------------------------------------------
     Set up the recursion functionality in binderLib
    ---------------------------------------------------------------------- *)
diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml
index 9d164670a0..5eeae0357d 100644
--- a/src/list/src/rich_listScript.sml
+++ b/src/list/src/rich_listScript.sml
@@ -2382,6 +2382,18 @@ Proof
   simp[LASTN_DROP_UNCOND]
 QED
 
+(* from examples/lambda/basics/appFOLDLScript.sml *)
+Theorem DROP_PREn_LAST_CONS :
+    !l n. 0 < n /\ n <= LENGTH l ==>
+          (DROP (n - 1) l = LAST (TAKE n l) :: DROP n l)
+Proof
+  Induct THEN SRW_TAC [numSimps.ARITH_ss][TAKE_def, DROP_def] THENL [
+    `n = 1` by numLib.DECIDE_TAC THEN SRW_TAC [][],
+    `n = 1` by numLib.DECIDE_TAC THEN SRW_TAC [][],
+    `(l = []) \/ ?h t0. l = h :: t0` by METIS_TAC [list_CASES] THEN
+    FULL_SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) [] ]
+QED
+
 val SUB_ADD_lem =
    numLib.DECIDE ``!l n m. n + m <= l ==> ((l - (n + m)) + n = l - m)``
 
@@ -2569,6 +2581,14 @@ val IS_PREFIX_BUTLAST = Q.store_thm ("IS_PREFIX_BUTLAST",
    THEN INDUCT_THEN list_INDUCT ASSUME_TAC
    THEN ASM_SIMP_TAC boolSimps.bool_ss [FRONT_CONS, IS_PREFIX]);
 
+Theorem IS_PREFIX_BUTLAST' :
+    !l. l <> [] ==> IS_PREFIX l (FRONT l)
+Proof
+    Q.X_GEN_TAC ‘l’
+ >> Cases_on ‘l’ >- SRW_TAC[][]
+ >> SRW_TAC[][IS_PREFIX_BUTLAST]
+QED
+
 val IS_PREFIX_LENGTH = Q.store_thm ("IS_PREFIX_LENGTH",
    `!x y. IS_PREFIX y x ==> LENGTH x <= LENGTH y`,
    INDUCT_THEN list_INDUCT ASSUME_TAC
diff --git a/src/pred_set/src/pred_setScript.sml b/src/pred_set/src/pred_setScript.sml
index 28b75ecbac..dea72b5418 100644
--- a/src/pred_set/src/pred_setScript.sml
+++ b/src/pred_set/src/pred_setScript.sml
@@ -829,6 +829,14 @@ val DISJOINT_ALT = store_thm (* from util_prob *)
    RW_TAC std_ss [IN_DISJOINT]
    >> PROVE_TAC []);
 
+Theorem DISJOINT_ALT' :
+    !s t. DISJOINT s t <=> !x. x IN t ==> x NOTIN s
+Proof
+    ONCE_REWRITE_TAC [DISJOINT_SYM]
+ >> RW_TAC std_ss [IN_DISJOINT]
+ >> PROVE_TAC []
+QED
+
 (* --------------------------------------------------------------------- *)
 (* A theorem from homeier@org.aero.uniblab (Peter Homeier)               *)
 (* --------------------------------------------------------------------- *)
@@ -863,6 +871,13 @@ Proof
      ASM_REWRITE_TAC []
 QED
 
+Theorem DISJOINT_UNION' :
+    !s t u. DISJOINT u (s UNION t) <=> DISJOINT u s /\ DISJOINT u t
+Proof
+    ONCE_REWRITE_TAC [DISJOINT_SYM]
+ >> REWRITE_TAC [DISJOINT_UNION]
+QED
+
 Theorem DISJOINT_UNION_BOTH:
   !s t u:'a set.
         (DISJOINT (s UNION t) u <=> DISJOINT s u /\ DISJOINT t u) /\