diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml
index 8c6746961c..e73bb1be60 100644
--- a/examples/lambda/barendregt/chap2Script.sml
+++ b/examples/lambda/barendregt/chap2Script.sml
@@ -235,9 +235,12 @@ val (asmlam_rules, asmlam_ind, asmlam_cases) = Hol_reln`
   (!x M M'. asmlam eqns M M' ==> asmlam eqns (LAM x M) (LAM x M'))
 `;
 
+(* This is also Definition 2.1.32 [1, p.33] *)
 val incompatible_def =
     Define`incompatible x y = ~consistent (asmlam {(x,y)})`
 
+Overload "#" = “incompatible”
+
 val S_def =
     Define`S = LAM "x" (LAM "y" (LAM "z"
                                      ((VAR "x" @@ VAR "z") @@
@@ -550,12 +553,31 @@ Proof
  >> qexistsl_tac [‘v’, ‘t0’] >> REWRITE_TAC []
 QED
 
+Theorem is_abs_appstar[simp]:
+  is_abs (M @* Ns) ⇔ is_abs M ∧ (Ns = [])
+Proof
+  Induct_on ‘Ns’ using SNOC_INDUCT >>
+  simp[appstar_SNOC]
+QED
+
+Theorem is_abs_LAMl[simp]:
+  is_abs (LAMl vs M) ⇔ vs ≠ [] ∨ is_abs M
+Proof
+  Cases_on ‘vs’ >> simp[]
+QED
+
 val (is_comb_thm, _) = define_recursive_term_function
   `(is_comb (VAR s) = F) /\
    (is_comb (t1 @@ t2) = T) /\
    (is_comb (LAM v t) = F)`;
 val _ = export_rewrites ["is_comb_thm"]
 
+Theorem is_comb_LAMl[simp] :
+    is_comb (LAMl vs M) <=> (vs = []) /\ is_comb M
+Proof
+  Cases_on `vs` THEN SRW_TAC [][]
+QED
+
 Theorem is_comb_vsubst_invariant[simp]:
   !t. is_comb ([VAR v/u] t) = is_comb t
 Proof
@@ -628,6 +650,39 @@ Proof
   SRW_TAC [][SUB_THM, SUB_VAR]
 QED
 
+Theorem bnf_characterisation:
+  ∀M.
+    bnf M ⇔
+      ∃vs v Ms. ALL_DISTINCT vs ∧ M = LAMl vs (VAR v ·· Ms) ∧
+                (∀M. MEM M Ms ⇒ bnf M)
+Proof
+  ho_match_mp_tac nc_INDUCTION2 >> qexists ‘∅’ >> rw[] >~
+  [‘VAR _ ·· _ = M1 @@ M2’]
+  >- (simp[] >> eq_tac >> rpt strip_tac >~
+      [‘M1 = LAMl vs1 _’, ‘M1 @@ M2’]
+      >- (gvs[app_eq_appstar] >>
+          Q.REFINE_EXISTS_TAC ‘SNOC M Mt’ >>
+          simp[DISJ_IMP_THM, rich_listTheory.FRONT_APPEND] >>
+          metis_tac[]) >>
+      Cases_on ‘Ms’ using rich_listTheory.SNOC_CASES >>
+      gvs[rich_listTheory.SNOC_APPEND, appstar_APPEND] >>
+      dsimp[LAMl_eq_appstar] >> irule_at Any EQ_REFL >> simp[]) >>
+  pop_assum SUBST_ALL_TAC >> eq_tac >> rpt strip_tac >> gvs[] >~
+  [‘LAM y (LAMl vs _)’]
+  >- (reverse (Cases_on ‘MEM y vs’)
+      >- (qexists ‘y::vs’ >> simp[]) >>
+      ‘y # LAMl vs (VAR v ·· Ms)’ by simp[FV_LAMl] >>
+      Q_TAC (NEW_TAC "z") ‘y INSERT set vs ∪ FV (VAR v ·· Ms)’ >>
+      ‘z # LAMl vs (VAR v ·· Ms)’ by simp[FV_LAMl] >>
+      dxrule_then (qspec_then ‘y’ mp_tac) tpm_ALPHA >>
+      simp[tpm_fresh, FV_LAMl] >> strip_tac >> qexists ‘z::vs’ >> simp[]) >>
+  rename [‘LAM y M = LAMl vs (VAR v ·· Ms)’] >>
+  Cases_on ‘vs’ >> gvs[] >> gvs[LAM_eq_thm]
+  >- metis_tac[] >>
+  simp[tpm_LAMl, tpm_appstar] >> irule_at Any EQ_REFL >>
+  simp[MEM_listpm] >> rpt strip_tac >> first_assum drule >> simp[]
+QED
+
 val _ = augment_srw_ss [rewrites [LAM_eq_thm]]
 val (rand_thm, _) = define_recursive_term_function `rand (t1 @@ t2) = t2`;
 val _ = export_rewrites ["rand_thm"]
@@ -739,6 +794,117 @@ Proof
   Induct_on ‘Ns’ using SNOC_INDUCT >> rw [appstar_SNOC, lameq_APPL]
 QED
 
+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
+Proof
+    rpt STRIP_TAC
+ >> NewQ.ABBREV_TAC ‘L = ZIP (vs,Ns)’
+ >> ‘(Ns = MAP SND L) /\ (vs = MAP FST L)’ by rw [Abbr ‘L’, MAP_ZIP]
+ >> FULL_SIMP_TAC std_ss []
+ >> Q.PAT_X_ASSUM ‘EVERY closed (MAP SND L)’ MP_TAC
+ >> Q.PAT_X_ASSUM ‘ALL_DISTINCT (MAP FST L)’ MP_TAC
+ >> KILL_TAC
+ >> Q.ID_SPEC_TAC ‘M’
+ >> Induct_on ‘L’ >> rw []
+ >- (Suff ‘FEMPTY |++ [] = FEMPTY :string |-> term’ >- rw [] \\
+     rw [FUPDATE_LIST_EQ_FEMPTY])
+ >> NewQ.ABBREV_TAC ‘v = FST h’
+ >> NewQ.ABBREV_TAC ‘vs = MAP FST L’
+ >> NewQ.ABBREV_TAC ‘N = SND h’
+ >> NewQ.ABBREV_TAC ‘Ns = MAP SND L’
+ (* RHS rewriting *)
+ >> ‘h :: L = [h] ++ L’ by rw [] >> POP_ORW
+ >> rw [FUPDATE_LIST_APPEND]
+ >> Know ‘FEMPTY |++ [h] |++ L = FEMPTY |++ L |++ [h]’
+ >- (MATCH_MP_TAC FUPDATE_LIST_APPEND_COMMUTES \\
+     rw [DISJOINT_ALT])
+ >> Rewr'
+ >> rw [GSYM FUPDATE_EQ_FUPDATE_LIST]
+ >> NewQ.ABBREV_TAC ‘fm = FEMPTY |++ L’
+ >> FULL_SIMP_TAC std_ss []
+ >> ‘h = (v,N)’ by rw [Abbr ‘v’, Abbr ‘N’] >> POP_ORW
+ >> Know ‘(fm |+ (v,N)) ' M = fm ' ([N/v] M)’
+ >- (MATCH_MP_TAC ssub_update_apply' \\
+     Q.PAT_X_ASSUM ‘closed N’ MP_TAC \\
+     rw [Abbr ‘fm’, FDOM_FUPDATE_LIST, closed_def] \\
+     Cases_on ‘INDEX_OF y vs’ >- fs [INDEX_OF_eq_NONE] \\
+     rename1 ‘INDEX_OF y vs = SOME n’ \\
+     fs [INDEX_OF_eq_SOME] \\
+     Q.PAT_X_ASSUM ‘EL n vs = y’ (ONCE_REWRITE_TAC o wrap o SYM) \\
+    ‘LENGTH L = LENGTH vs’ by rw [Abbr ‘vs’, LENGTH_MAP] \\
+     Know ‘(FEMPTY |++ L) ' (EL n vs) = EL n Ns’
+     >- (MATCH_MP_TAC FUPDATE_LIST_APPLY_MEM \\
+         Q.EXISTS_TAC ‘n’ >> rw [] \\
+        ‘m <> n’ by rw [] \\
+         METIS_TAC [EL_ALL_DISTINCT_EL_EQ]) >> Rewr' \\
+     Q.PAT_X_ASSUM ‘EVERY closed Ns’ MP_TAC \\
+     rw [EVERY_MEM, closed_def] \\
+     POP_ASSUM MATCH_MP_TAC >> rw [MEM_EL] \\
+    ‘LENGTH L = LENGTH Ns’ by rw [Abbr ‘Ns’, LENGTH_MAP] \\
+     Q.EXISTS_TAC ‘n’ >> rw [])
+ >> Rewr'
+ (* LHS rewriting *)
+ >> Know ‘LAM v (LAMl vs M) @@ N == LAMl vs ([N/v] M)’
+ >- (SIMP_TAC (betafy (srw_ss())) [] \\
+     Suff ‘[N/v] (LAMl vs M) = LAMl vs ([N/v] M)’ >- rw [lameq_rules] \\
+     MATCH_MP_TAC LAMl_SUB \\
+     Q.PAT_X_ASSUM ‘closed N’ MP_TAC >> rw [closed_def])
+ >> DISCH_TAC
+ >> MATCH_MP_TAC lameq_TRANS
+ >> Q.EXISTS_TAC ‘LAMl vs ([N/v] M) @* Ns’ >> art []
+ >> MATCH_MP_TAC lameq_appstar_cong >> art []
+QED
+
+val foldl_snoc = prove(
+  ``!l f x y. FOLDL f x (APPEND l [y]) = f (FOLDL f x l) y``,
+  Induct THEN SRW_TAC [][]);
+
+val combs_not_size_1 = prove(
+  ``(size M = 1) ==> ~is_comb M``,
+  Q.SPEC_THEN `M` STRUCT_CASES_TAC term_CASES THEN
+  SRW_TAC [][size_thm, size_nz]);
+
+Theorem strange_cases :
+    !M : term. (?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/
+               (?vs args t.
+                         (M = LAMl vs (FOLDL APP t args)) /\
+                         ~(args = []) /\ ~is_comb t)
+Proof
+  HO_MATCH_MP_TAC simple_induction THEN REPEAT CONJ_TAC THENL [
+    (* VAR *) GEN_TAC THEN DISJ1_TAC THEN
+              MAP_EVERY Q.EXISTS_TAC [`[]`, `VAR s`] THEN SRW_TAC [][size_thm],
+    (* app *) MAP_EVERY Q.X_GEN_TAC [`M`,`N`] THEN
+              DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) THEN
+              DISJ2_TAC THEN Q.EXISTS_TAC `[]` THEN
+              SIMP_TAC (srw_ss()) [] THEN
+              `(?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/
+               (?vs args t.
+                        (M = LAMl vs (FOLDL APP t args)) /\ ~(args = []) /\
+                        ~is_comb t)` by PROVE_TAC []
+              THENL [
+                MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN
+                ASM_SIMP_TAC (srw_ss()) [] THEN
+                PROVE_TAC [combs_not_size_1],
+                ASM_SIMP_TAC (srw_ss()) [] THEN
+                Cases_on `vs` THENL [
+                  MAP_EVERY Q.EXISTS_TAC [`APPEND args [N]`, `t`] THEN
+                  ASM_SIMP_TAC (srw_ss()) [foldl_snoc],
+                  MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN
+                  ASM_SIMP_TAC (srw_ss()) []
+                ]
+              ],
+    (* LAM *) MAP_EVERY Q.X_GEN_TAC [`x`,`M`] THEN STRIP_TAC THENL [
+                DISJ1_TAC THEN
+                MAP_EVERY Q.EXISTS_TAC [`x::vs`, `M'`] THEN
+                ASM_SIMP_TAC (srw_ss()) [],
+                DISJ2_TAC THEN
+                MAP_EVERY Q.EXISTS_TAC [`x::vs`, `args`, `t`] THEN
+                ASM_SIMP_TAC (srw_ss()) []
+              ]
+  ]
+QED
+
 val _ = remove_ovl_mapping "Y" {Thy = "chap2", Name = "Y"}
 
 val _ = export_theory()
diff --git a/examples/lambda/barendregt/head_reductionScript.sml b/examples/lambda/barendregt/head_reductionScript.sml
index 8ecda24d66..d9040b199d 100644
--- a/examples/lambda/barendregt/head_reductionScript.sml
+++ b/examples/lambda/barendregt/head_reductionScript.sml
@@ -1,8 +1,10 @@
 open HolKernel Parse boolLib bossLib
 
-open pred_setTheory boolSimps;
+open boolSimps relationTheory pred_setTheory listTheory finite_mapTheory
+     hurdUtils;
 
-open termTheory chap2Theory chap3Theory nomsetTheory binderLib;
+open termTheory appFOLDLTheory chap2Theory chap3Theory nomsetTheory binderLib
+     term_posnsTheory;
 
 val _ = new_theory "head_reduction"
 
@@ -12,11 +14,13 @@ fun Store_thm(trip as (n,t,tac)) = store_thm trip before export_rewrites [n]
 
 val _ = set_trace "Unicode" 1
 
-val (hreduce1_rules, hreduce1_ind, hreduce1_cases) = Hol_reln`
+Inductive hreduce1 :
   (∀v M N. hreduce1 (LAM v M @@ N) ([N/v]M)) ∧
+[~LAM:]
   (∀v M1 M2. hreduce1 M1 M2 ⇒ hreduce1 (LAM v M1) (LAM v M2)) ∧
+[~APP:]
   (∀M1 M2 N. hreduce1 M1 M2 ∧ ¬is_abs M1 ⇒ hreduce1 (M1 @@ N) (M2 @@ N))
-`;
+End
 
 val _ = set_fixity "-h->" (Infix(NONASSOC, 450))
 val _ = overload_on ("-h->", ``hreduce1``)
@@ -43,18 +47,17 @@ val _ = temp_add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT,2)),
                        term_name = "apply_perm"}
 val _ = temp_overload_on ("apply_perm", ``λp M. tpm [p] M``)
 val _ = temp_overload_on ("apply_perm", ``tpm``)
-val _ = temp_overload_on ("#", ``λv t. v ∉ FV t``)
-val _ = temp_set_fixity "#" (Infix(NONASSOC, 450))
 
 val tpm_hreduce_I = store_thm(
   "tpm_hreduce_I",
   ``∀M N. M -h-> N ⇒ ∀π. π·M -h-> π·N``,
   HO_MATCH_MP_TAC hreduce1_ind THEN SRW_TAC [][tpm_subst, hreduce1_rules]);
 
-val tpm_hreduce = store_thm(
-  "tpm_hreduce",
-  ``∀M N π. π·M -h-> π·N ⇔ M -h-> N``,
-  METIS_TAC [pmact_inverse, tpm_hreduce_I]);
+Theorem tpm_hreduce[simp] :
+    ∀M N π. π·M -h-> π·N ⇔ M -h-> N
+Proof
+  METIS_TAC [pmact_inverse, tpm_hreduce_I]
+QED
 
 val hreduce1_rwts = store_thm(
   "hreduce1_rwts",
@@ -86,6 +89,94 @@ val hreduce1_rwts = store_thm(
     METIS_TAC [lemma15a, pmact_flip_args, fresh_tpm_subst]
   ]);
 
+val hreduce1_unique = store_thm(
+  "hreduce1_unique",
+  ``∀M N1 N2. M -h-> N1 ∧ M -h-> N2 ⇒ (N1 = N2)``,
+  Q_TAC SUFF_TAC `∀M N. M -h-> N ⇒ ∀P. M -h-> P ⇒ (N = P)`
+        THEN1 METIS_TAC [] THEN
+  HO_MATCH_MP_TAC hreduce1_ind THEN
+  SIMP_TAC (srw_ss() ++ DNF_ss) [hreduce1_rwts]);
+
+Theorem hreduce1_gen_bvc_ind :
+  !P f. (!x. FINITE (f x)) /\
+        (!v M N x. v NOTIN f x ==> P (LAM v M @@ N) ([N/v] M) x) /\
+        (!v M1 M2 x. M1 -h-> M2 /\ v NOTIN f x /\ (!z. P M1 M2 z) ==>
+                     P (LAM v M1) (LAM v M2) x) /\
+        (!M1 M2 N x. M1 -h-> M2 /\ (!z. P M1 M2 z) /\ ~is_abs M1 ==>
+                     P (M1 @@ N) (M2 @@ N) x)
+    ==> !M N. M -h-> N ==> !x. P M N x
+Proof
+    rpt GEN_TAC >> STRIP_TAC
+ >> Suff ‘!M N. M -h-> N ==> !p x. P (tpm p M) (tpm p N) x’
+ >- METIS_TAC [pmact_nil]
+ >> HO_MATCH_MP_TAC hreduce1_strongind
+ >> reverse (rw []) (* easy goal first *)
+ >- (Q.ABBREV_TAC ‘u = lswapstr p v’ \\
+     Q_TAC (NEW_TAC "z") ‘(f x) UNION {v} UNION FV (tpm p M) UNION FV (tpm p N)’ \\
+    ‘(LAM u (tpm p M) = LAM z (tpm ([(z,u)] ++ p) M)) /\
+     (LAM u (tpm p N) = LAM z (tpm ([(z,u)] ++ p) N))’
+       by rw [tpm_ALPHA, pmact_decompose] >> rw [])
+ (* stage work *)
+ >> Q.ABBREV_TAC ‘u = lswapstr p v’
+ >> Q_TAC (NEW_TAC "z") ‘(f x) UNION {v} UNION FV (tpm p M) UNION FV (tpm p N)’
+ >> ‘LAM u (tpm p M) = LAM z (tpm ([(z,u)] ++ p) M)’ by rw [tpm_ALPHA, pmact_decompose]
+ >> POP_ORW
+ >> Q.ABBREV_TAC ‘M1 = apply_perm ([(z,u)] ++ p) M’
+ >> Suff ‘tpm p ([N/v] M) = [tpm p N/z] M1’ >- rw []
+ >> rw [tpm_subst, Abbr ‘M1’]
+ >> simp [Once tpm_CONS, fresh_tpm_subst]
+ >> simp [lemma15a]
+QED
+
+(* |- !P X.
+        FINITE X /\ (!v M N. v NOTIN X ==> P (LAM v M @@ N) ([N/v] M)) /\
+        (!v M1 M2. M1 -h-> M2 /\ v NOTIN X /\ P M1 M2 ==> P (LAM v M1) (LAM v M2)) /\
+        (!M1 M2 N. M1 -h-> M2 /\ P M1 M2 /\ ~is_abs M1 ==> P (M1 @@ N) (M2 @@ N)) ==>
+        !M N. M -h-> N ==> P M N
+ *)
+Theorem hreduce1_bvcX_ind =
+  hreduce1_gen_bvc_ind |> Q.SPECL [`λM N x. P' M N`, `λx. X`]
+                       |> SIMP_RULE (srw_ss()) []
+                       |> Q.INST [`P'` |-> `P`]
+                       |> Q.GEN `X` |> Q.GEN `P`
+
+(* Lemma 8.3.12 [1, p.174] *)
+Theorem hreduce1_substitutive :
+    !M N. M -h-> N ==> [P/v] M -h-> [P/v] N
+Proof
+    HO_MATCH_MP_TAC hreduce1_bvcX_ind
+ >> Q.EXISTS_TAC ‘FV P UNION {v}’ >> rw [hreduce1_rules]
+ >- METIS_TAC [substitution_lemma, hreduce1_rules]
+ >> ‘is_comb M \/ is_var M’ by METIS_TAC [term_cases]
+ >- (MATCH_MP_TAC hreduce1_APP >> art [] \\
+     gs [is_comb_APP_EXISTS, is_abs_thm])
+ >> gs [is_var_cases, hreduce1_rwts]
+QED
+
+(* This form is useful for ‘|- substitutive R ==> ...’ theorems (chap3Theory) *)
+Theorem substitutive_hreduce1 :
+    substitutive (-h->)
+Proof
+    rw [substitutive_def, hreduce1_substitutive]
+QED
+
+Theorem hreduce_substitutive :
+    !M N. M -h->* N ==> [P/v] M -h->* [P/v] N
+Proof
+    HO_MATCH_MP_TAC RTC_INDUCT >> rw []
+ >> METIS_TAC [RTC_RULES, hreduce1_substitutive]
+QED
+
+Theorem substitutive_hreduce :
+    substitutive (-h->*)
+Proof
+    rw [substitutive_def, hreduce_substitutive]
+QED
+
+(* ----------------------------------------------------------------------
+    Head normal form (hnf)
+   ---------------------------------------------------------------------- *)
+
 val hnf_def = Define`hnf M = ∀N. ¬(M -h-> N)`;
 val hnf_thm = Store_thm(
   "hnf_thm",
@@ -102,14 +193,6 @@ val hnf_tpm = Store_thm(
   ``∀M π. hnf (π·M) = hnf M``,
   HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
 
-val hreduce1_unique = store_thm(
-  "hreduce1_unique",
-  ``∀M N1 N2. M -h-> N1 ∧ M -h-> N2 ⇒ (N1 = N2)``,
-  Q_TAC SUFF_TAC `∀M N. M -h-> N ⇒ ∀P. M -h-> P ⇒ (N = P)`
-        THEN1 METIS_TAC [] THEN
-  HO_MATCH_MP_TAC hreduce1_ind THEN
-  SIMP_TAC (srw_ss() ++ DNF_ss) [hreduce1_rwts]);
-
 val strong_cc_ind = IndDefLib.derive_strong_induction (compat_closure_rules,
                                                        compat_closure_ind)
 
@@ -128,16 +211,18 @@ val hnf_ccbeta_preserved = store_thm(
     SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) []
   ]);
 
-val (weak_head_rules, weak_head_ind, weak_head_cases) = Hol_reln`
+(* ----------------------------------------------------------------------
+    Weak head reductions (weak_head or -w->)
+   ---------------------------------------------------------------------- *)
+
+Inductive weak_head :
   (∀v M N. weak_head (LAM v M @@ N) ([N/v]M)) ∧
   (∀M₁ M₂ N. weak_head M₁ M₂ ⇒ weak_head (M₁ @@ N) (M₂ @@ N))
-`;
+End
+
 val _ = set_fixity "-w->" (Infix(NONASSOC, 450))
 val _ = overload_on ("-w->", ``weak_head``)
 
-val strong_weak_ind = IndDefLib.derive_strong_induction(weak_head_rules,
-                                                        weak_head_ind)
-
 val wh_is_abs = store_thm(
   "wh_is_abs",
   ``∀M N. M -w-> N ⇒ ¬is_abs M``,
@@ -151,9 +236,8 @@ val wh_lam = Store_thm(
 val wh_head = store_thm(
   "wh_head",
   ``∀M N. M -w-> N ⇒ M -h-> N``,
-  HO_MATCH_MP_TAC strong_weak_ind THEN METIS_TAC [wh_is_abs, hreduce1_rules]);
-
-
+    HO_MATCH_MP_TAC weak_head_strongind
+ >> METIS_TAC [wh_is_abs, hreduce1_rules]);
 
 val _ = set_fixity "-w->*" (Infix(NONASSOC, 450))
 val _ = overload_on ("-w->*", ``RTC (-w->)``)
@@ -353,7 +437,111 @@ val head_reductions_have_weak_prefixes = store_thm(
    metis_tac [relationTheory.RTC_RULES, hreduce_weak_or_strong]);
 
 (* ----------------------------------------------------------------------
-    HNF and Combinators
+    Head redex
+   ---------------------------------------------------------------------- *)
+
+val _ = add_infix ("is_head_redex", 760, NONASSOC)
+
+Inductive is_head_redex :
+    (!v (t:term) u. [] is_head_redex (LAM v t @@ u)) /\
+    (!v t p. p is_head_redex t ==> (In::p) is_head_redex (LAM v t)) /\
+    (!t u v p. p is_head_redex (t @@ u) ==>
+               (Lt::p) is_head_redex (t @@ u) @@ v)
+End
+
+val ihr_bvc_ind = store_thm(
+  "ihr_bvc_ind",
+  ``!P X. FINITE X /\
+          (!v M N. ~(v IN X) /\ ~(v IN FV N) ==> P [] (LAM v M @@ N)) /\
+          (!v M p. ~(v IN X) /\ P p M ==> P (In::p) (LAM v M)) /\
+          (!M N L p. P p (M @@ N) ==> P (Lt::p) ((M @@ N) @@ L)) ==>
+          !p M. p is_head_redex M ==> P p M``,
+  REPEAT GEN_TAC THEN STRIP_TAC THEN
+  Q_TAC SUFF_TAC `!p M. p is_head_redex M ==> !pi. P p (tpm pi M)`
+        THEN1 METIS_TAC [pmact_nil] THEN
+  HO_MATCH_MP_TAC is_head_redex_ind THEN
+  SRW_TAC [][is_head_redex_rules] THENL [
+    Q.MATCH_ABBREV_TAC `P [] (LAM vv MM @@ NN)` THEN
+    markerLib.RM_ALL_ABBREVS_TAC THEN
+    Q_TAC (NEW_TAC "z") `FV MM UNION FV NN UNION X` THEN
+    `LAM vv MM = LAM z (tpm [(z,vv)] MM)` by SRW_TAC [][tpm_ALPHA] THEN
+    SRW_TAC [][],
+    Q.MATCH_ABBREV_TAC `P (In::p) (LAM vv MM)` THEN
+    Q_TAC (NEW_TAC "z") `FV MM UNION X` THEN
+    `LAM vv MM = LAM z (tpm [(z,vv)] MM)` by SRW_TAC [][tpm_ALPHA] THEN
+    SRW_TAC [][GSYM pmact_decompose, Abbr`MM`]
+  ]);
+
+val is_head_redex_subst_invariant = store_thm(
+  "is_head_redex_subst_invariant",
+  ``!p t u v. p is_head_redex t ==> p is_head_redex [u/v] t``,
+  REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`t`, `p`] THEN
+  HO_MATCH_MP_TAC ihr_bvc_ind THEN Q.EXISTS_TAC `v INSERT FV u` THEN
+  SRW_TAC [][SUB_THM, SUB_VAR, is_head_redex_rules]);
+
+Theorem is_head_redex_tpm_invariant[simp] :
+    p is_head_redex (tpm pi t) = p is_head_redex t
+Proof
+  Q_TAC SUFF_TAC `!p t. p is_head_redex t ==> !pi. p is_head_redex (tpm pi t)`
+        THEN1 METIS_TAC [pmact_inverse] THEN
+  HO_MATCH_MP_TAC is_head_redex_ind THEN SRW_TAC [][is_head_redex_rules]
+QED
+
+val is_head_redex_unique = store_thm(
+  "is_head_redex_unique",
+  ``!t p1 p2. p1 is_head_redex t /\ p2 is_head_redex t ==> (p1 = p2)``,
+  Q_TAC SUFF_TAC
+        `!p1 t. p1 is_head_redex t ==> !p2. p2 is_head_redex t ==> (p1 = p2)`
+        THEN1 PROVE_TAC [] THEN
+  HO_MATCH_MP_TAC is_head_redex_ind THEN REPEAT STRIP_TAC THEN
+  POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC [is_head_redex_cases] THEN
+  SRW_TAC [][LAM_eq_thm]);
+
+val is_head_redex_thm = store_thm(
+  "is_head_redex_thm",
+  ``(p is_head_redex (LAM v t) = ?p0. (p = In::p0) /\ p0 is_head_redex t) /\
+    (p is_head_redex (t @@ u) = (p = []) /\ is_abs t \/
+                                ?p0. (p = Lt::p0) /\ is_comb t /\
+                                          p0 is_head_redex t) /\
+    (p is_head_redex (VAR v) = F)``,
+  REPEAT CONJ_TAC THEN
+  SRW_TAC [][Once is_head_redex_cases, SimpLHS, LAM_eq_thm] THEN
+  SRW_TAC [][EQ_IMP_THM] THENL [
+    PROVE_TAC [],
+    PROVE_TAC [is_abs_thm, term_CASES],
+    METIS_TAC [is_comb_thm, term_CASES]
+  ]);
+
+val head_redex_leftmost = store_thm(
+  "head_redex_leftmost",
+  ``!p t. p is_head_redex t ==>
+          !p'. p' IN redex_posns t ==> (p = p') \/ p < p'``,
+  HO_MATCH_MP_TAC is_head_redex_ind THEN
+  SRW_TAC [][redex_posns_thm, DISJ_IMP_THM]);
+
+val hnf_no_head_redex = store_thm(
+  "hnf_no_head_redex",
+  ``!t. hnf t = !p. ~(p is_head_redex t)``,
+  HO_MATCH_MP_TAC simple_induction THEN
+  SRW_TAC [][hnf_thm, is_head_redex_thm] THEN
+  Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN
+  SRW_TAC [][is_head_redex_thm]);
+
+val head_redex_is_redex = store_thm(
+  "head_redex_is_redex",
+  ``!p t. p is_head_redex t ==> p IN redex_posns t``,
+  HO_MATCH_MP_TAC is_head_redex_ind THEN
+  SRW_TAC [][redex_posns_thm]);
+
+val is_head_redex_vsubst_invariant = store_thm(
+  "is_head_redex_vsubst_invariant",
+  ``!t v x p. p is_head_redex ([VAR v/x] t) = p is_head_redex t``,
+  REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`p`, `t`] THEN
+  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{x;v}` THEN
+  SRW_TAC [][is_head_redex_thm, SUB_THM, SUB_VAR]);
+
+(* ----------------------------------------------------------------------
+    More results about head normal forms (hnf)
    ---------------------------------------------------------------------- *)
 
 Theorem hnf_I :
@@ -362,4 +550,35 @@ Proof
     RW_TAC std_ss [hnf_thm, I_def]
 QED
 
+Theorem hnf_LAMl[simp] :
+    hnf (LAMl vs M) <=> hnf M
+Proof
+    Induct_on ‘vs’ >> rw []
+QED
+
+Theorem hnf_appstar :
+    !M Ns. hnf (M @* Ns) <=> hnf M /\ (is_abs M ⇒ (Ns = []))
+Proof
+  Induct_on ‘Ns’ using SNOC_INDUCT >> simp[appstar_SNOC] >>
+  dsimp[SF CONJ_ss] >> metis_tac[]
+QED
+
+(* FIXME: can we put ‘ALL_DISTINCT vs’ into RHS? cf. bnf_characterisation *)
+Theorem hnf_cases :
+  !M : term. hnf M <=> ?vs args y. M = LAMl vs (VAR y @* args)
+Proof
+  simp[FORALL_AND_THM, EQ_IMP_THM] >> conj_tac
+  >- (gen_tac >> MP_TAC (Q.SPEC ‘M’ strange_cases)
+      >> RW_TAC std_ss []
+      >- (FULL_SIMP_TAC std_ss [size_1_cases] \\
+          qexistsl_tac [‘vs’, ‘[]’, ‘y’] >> rw [])
+      >> FULL_SIMP_TAC std_ss [hnf_LAMl]
+      >> ‘hnf t /\ ~is_abs t’ by PROVE_TAC [hnf_appstar]
+      >> ‘is_var t’ by METIS_TAC [term_cases]
+      >> FULL_SIMP_TAC std_ss [is_var_cases]
+      >> qexistsl_tac [‘vs’, ‘args’, ‘y’] >> art []) >>
+  simp[PULL_EXISTS, hnf_appstar]
+QED
+
 val _ = export_theory()
+val _ = html_theory "head_reduction";
diff --git a/examples/lambda/barendregt/normal_orderScript.sml b/examples/lambda/barendregt/normal_orderScript.sml
index a1083f4aca..6f08fa949b 100644
--- a/examples/lambda/barendregt/normal_orderScript.sml
+++ b/examples/lambda/barendregt/normal_orderScript.sml
@@ -1,8 +1,9 @@
 open HolKernel Parse boolLib bossLib
 
-open boolSimps pred_setTheory pathTheory binderLib
-open chap3Theory standardisationTheory term_posnsTheory termTheory
-     finite_developmentsTheory appFOLDLTheory nomsetTheory
+open boolSimps pred_setTheory pathTheory;
+
+open chap3Theory standardisationTheory term_posnsTheory termTheory binderLib
+     finite_developmentsTheory appFOLDLTheory nomsetTheory head_reductionTheory;
 
 val _ = new_theory "normal_order"
 
diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml
index 4293d79c98..c00e86a45d 100644
--- a/examples/lambda/barendregt/solvableScript.sml
+++ b/examples/lambda/barendregt/solvableScript.sml
@@ -10,7 +10,7 @@ open arithmeticTheory pred_setTheory listTheory sortingTheory finite_mapTheory
 
 (* lambda theories *)
 open termTheory appFOLDLTheory chap2Theory chap3Theory standardisationTheory
-     reductionEval;
+     head_reductionTheory reductionEval;
 
 val _ = new_theory "solvable";
 
@@ -238,7 +238,7 @@ Proof
  >> Q.ABBREV_TAC ‘fm = FEMPTY |++ ZIP (vs,Ns0)’
  >> Know ‘LAMl vs M @* Ns0 == fm ' M’
  >- (Q.UNABBREV_TAC ‘fm’ \\
-     MATCH_MP_TAC LAMl_appstar >> rw [])
+     MATCH_MP_TAC lameq_LAMl_appstar >> rw [])
  >> DISCH_TAC
  >> ‘LAMl vs M @* Ns0 @* Ns1 == fm ' M @* Ns1’ by PROVE_TAC [lameq_appstar_cong]
  >> ‘fm ' M @* Ns1 == I’ by PROVE_TAC [lameq_TRANS, lameq_SYM]
@@ -290,7 +290,7 @@ Proof
  >> rw [solvable_def, closed_substitution_instances_def]
  >> Q.ABBREV_TAC ‘vss = FDOM fm’
  >> ‘FINITE vss’ by rw [FDOM_FINITE, Abbr ‘vss’]
- (* preparing for LAMl_appstar *)
+ (* preparing for lameq_LAMl_appstar *)
  >> Q.ABBREV_TAC ‘vs = SET_TO_LIST vss’
  >> ‘ALL_DISTINCT vs’ by PROVE_TAC [Abbr ‘vs’, ALL_DISTINCT_SET_TO_LIST]
  >> Q.ABBREV_TAC ‘Ps = MAP (\v. fm ' v) vs’
@@ -316,7 +316,7 @@ Proof
  >> Rewr'
  >> DISCH_TAC
  >> Know ‘LAMl vs M @* Ps == (FEMPTY |++ ZIP (vs,Ps)) ' M’
- >- (MATCH_MP_TAC LAMl_appstar >> art [] \\
+ >- (MATCH_MP_TAC lameq_LAMl_appstar >> art [] \\
      rw [Abbr ‘Ps’, EVERY_MEM, MEM_MAP] \\
      FIRST_X_ASSUM MATCH_MP_TAC \\
      POP_ASSUM MP_TAC \\
@@ -364,7 +364,7 @@ Proof
  >> Q.ABBREV_TAC ‘fm = FEMPTY |++ ZIP (vs,Ns0)’
  >> Know ‘LAMl vs M @* Ns0 == fm ' M’
  >- (Q.UNABBREV_TAC ‘fm’ \\
-     MATCH_MP_TAC LAMl_appstar >> rw [])
+     MATCH_MP_TAC lameq_LAMl_appstar >> rw [])
  >> DISCH_TAC
  >> ‘LAMl vs M @* Ns0 @* Ns1 == fm ' M @* Ns1’ by PROVE_TAC [lameq_appstar_cong]
  >> ‘fm ' M @* Ns1 == I’ by PROVE_TAC [lameq_TRANS, lameq_SYM]
@@ -387,7 +387,7 @@ Proof
  >> Q.ABBREV_TAC ‘fm' = FEMPTY |++ ZIP (vs',Ns0')’
  >> Know ‘LAMl vs' M @* Ns0' == fm' ' M’
  >- (Q.UNABBREV_TAC ‘fm'’ \\
-     MATCH_MP_TAC LAMl_appstar >> rw [])
+     MATCH_MP_TAC lameq_LAMl_appstar >> rw [])
  >> DISCH_TAC
  >> ‘LAMl vs' M @* Ns0' @* Ns1 == fm' ' M @* Ns1’ by PROVE_TAC [lameq_appstar_cong]
  >> MATCH_MP_TAC lameq_TRANS
@@ -486,7 +486,7 @@ QED
 
 Theorem ssub_LAM[local] = List.nth(CONJUNCTS ssub_thm, 2)
 
-(* Lemma 8.3.3 (ii) *)
+(* Lemma 8.3.3 (ii) [1, p.172] *)
 Theorem solvable_iff_LAM[simp] :
     !x M. solvable (LAM x M) <=> solvable M
 Proof
diff --git a/examples/lambda/barendregt/standardisationScript.sml b/examples/lambda/barendregt/standardisationScript.sml
index a3caae2a59..160de045bb 100644
--- a/examples/lambda/barendregt/standardisationScript.sml
+++ b/examples/lambda/barendregt/standardisationScript.sml
@@ -61,106 +61,6 @@ val better_standard_reduction = store_thm(
     SRW_TAC [][]
   ]);
 
-val _ = add_infix ("is_head_redex", 760, NONASSOC)
-
-val (is_head_redex_rules, is_head_redex_ind, is_head_redex_cases) =
-    IndDefLib.Hol_reln`
-      (!v (t:term) u. [] is_head_redex (LAM v t @@ u)) /\
-      (!v t p. p is_head_redex t ==> (In::p) is_head_redex (LAM v t)) /\
-      (!t u v p. p is_head_redex (t @@ u) ==>
-                 (Lt::p) is_head_redex (t @@ u) @@ v)
-    `;
-
-val ihr_bvc_ind = store_thm(
-  "ihr_bvc_ind",
-  ``!P X. FINITE X /\
-          (!v M N. ~(v IN X) /\ ~(v IN FV N) ==> P [] (LAM v M @@ N)) /\
-          (!v M p. ~(v IN X) /\ P p M ==> P (In::p) (LAM v M)) /\
-          (!M N L p. P p (M @@ N) ==> P (Lt::p) ((M @@ N) @@ L)) ==>
-          !p M. p is_head_redex M ==> P p M``,
-  REPEAT GEN_TAC THEN STRIP_TAC THEN
-  Q_TAC SUFF_TAC `!p M. p is_head_redex M ==> !pi. P p (tpm pi M)`
-        THEN1 METIS_TAC [pmact_nil] THEN
-  HO_MATCH_MP_TAC is_head_redex_ind THEN
-  SRW_TAC [][is_head_redex_rules] THENL [
-    Q.MATCH_ABBREV_TAC `P [] (LAM vv MM @@ NN)` THEN
-    markerLib.RM_ALL_ABBREVS_TAC THEN
-    Q_TAC (NEW_TAC "z") `FV MM UNION FV NN UNION X` THEN
-    `LAM vv MM = LAM z (tpm [(z,vv)] MM)` by SRW_TAC [][tpm_ALPHA] THEN
-    SRW_TAC [][],
-    Q.MATCH_ABBREV_TAC `P (In::p) (LAM vv MM)` THEN
-    Q_TAC (NEW_TAC "z") `FV MM UNION X` THEN
-    `LAM vv MM = LAM z (tpm [(z,vv)] MM)` by SRW_TAC [][tpm_ALPHA] THEN
-    SRW_TAC [][GSYM pmact_decompose, Abbr`MM`]
-  ]);
-
-val is_head_redex_subst_invariant = store_thm(
-  "is_head_redex_subst_invariant",
-  ``!p t u v. p is_head_redex t ==> p is_head_redex [u/v] t``,
-  REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`t`, `p`] THEN
-  HO_MATCH_MP_TAC ihr_bvc_ind THEN Q.EXISTS_TAC `v INSERT FV u` THEN
-  SRW_TAC [][SUB_THM, SUB_VAR, is_head_redex_rules]);
-
-val is_head_redex_tpm_invariant = Store_Thm(
-  "is_head_redex_tpm_invariant",
-  ``p is_head_redex (tpm pi t) = p is_head_redex t``,
-  Q_TAC SUFF_TAC `!p t. p is_head_redex t ==> !pi. p is_head_redex (tpm pi t)`
-        THEN1 METIS_TAC [pmact_inverse] THEN
-  HO_MATCH_MP_TAC is_head_redex_ind THEN SRW_TAC [][is_head_redex_rules]);
-
-val is_head_redex_unique = store_thm(
-  "is_head_redex_unique",
-  ``!t p1 p2. p1 is_head_redex t /\ p2 is_head_redex t ==> (p1 = p2)``,
-  Q_TAC SUFF_TAC
-        `!p1 t. p1 is_head_redex t ==> !p2. p2 is_head_redex t ==> (p1 = p2)`
-        THEN1 PROVE_TAC [] THEN
-  HO_MATCH_MP_TAC is_head_redex_ind THEN REPEAT STRIP_TAC THEN
-  POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC [is_head_redex_cases] THEN
-  SRW_TAC [][LAM_eq_thm]);
-
-val is_head_redex_thm = store_thm(
-  "is_head_redex_thm",
-  ``(p is_head_redex (LAM v t) = ?p0. (p = In::p0) /\ p0 is_head_redex t) /\
-    (p is_head_redex (t @@ u) = (p = []) /\ is_abs t \/
-                                ?p0. (p = Lt::p0) /\ is_comb t /\
-                                          p0 is_head_redex t) /\
-    (p is_head_redex (VAR v) = F)``,
-  REPEAT CONJ_TAC THEN
-  SRW_TAC [][Once is_head_redex_cases, SimpLHS, LAM_eq_thm] THEN
-  SRW_TAC [][EQ_IMP_THM] THENL [
-    PROVE_TAC [],
-    PROVE_TAC [is_abs_thm, term_CASES],
-    METIS_TAC [is_comb_thm, term_CASES]
-  ]);
-
-val head_redex_leftmost = store_thm(
-  "head_redex_leftmost",
-  ``!p t. p is_head_redex t ==>
-          !p'. p' IN redex_posns t ==> (p = p') \/ p < p'``,
-  HO_MATCH_MP_TAC is_head_redex_ind THEN
-  SRW_TAC [][redex_posns_thm, DISJ_IMP_THM]);
-
-val hnf_no_head_redex = store_thm(
-  "hnf_no_head_redex",
-  ``!t. hnf t = !p. ~(p is_head_redex t)``,
-  HO_MATCH_MP_TAC simple_induction THEN
-  SRW_TAC [][hnf_thm, is_head_redex_thm] THEN
-  Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN
-  SRW_TAC [][is_head_redex_thm]);
-
-val head_redex_is_redex = store_thm(
-  "head_redex_is_redex",
-  ``!p t. p is_head_redex t ==> p IN redex_posns t``,
-  HO_MATCH_MP_TAC is_head_redex_ind THEN
-  SRW_TAC [][redex_posns_thm]);
-
-val is_head_redex_vsubst_invariant = store_thm(
-  "is_head_redex_vsubst_invariant",
-  ``!t v x p. p is_head_redex ([VAR v/x] t) = p is_head_redex t``,
-  REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`p`, `t`] THEN
-  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{x;v}` THEN
-  SRW_TAC [][is_head_redex_thm, SUB_THM, SUB_VAR]);
-
 val _ = add_infix("is_internal_redex", 760, NONASSOC)
 (* definition 11.4.2 (i) *)
 val is_internal_redex_def = Define`
@@ -1170,15 +1070,6 @@ val lemma11_4_6 = store_thm(
     ]
   ]);
 
-val foldl_snoc = prove(
-  ``!l f x y. FOLDL f x (APPEND l [y]) = f (FOLDL f x l) y``,
-  Induct THEN SRW_TAC [][]);
-
-val combs_not_size_1 = prove(
-  ``(size M = 1) ==> ~is_comb M``,
-  Q.SPEC_THEN `M` STRUCT_CASES_TAC term_CASES THEN
-  SRW_TAC [][size_thm, size_nz]);
-
 val cant_ireduce_to_atom = prove(
   ``!M N. (size N = 1) ==> ~(M i_reduce1 N)``,
   Q_TAC SUFF_TAC `!M r N. labelled_redn beta M r N ==>
@@ -1212,124 +1103,6 @@ val i_reduce_to_LAM_underneath = prove(
     PROVE_TAC [labelled_redn_rules]
   ]);
 
-Definition LAMl_def:
-  LAMl vs (t : term) = FOLDR LAM t vs
-End
-
-Theorem LAMl_thm[simp]:
-  (LAMl [] M = M) /\
-  (LAMl (h::t) M = LAM h (LAMl t M))
-Proof SRW_TAC [][LAMl_def]
-QED
-
-Theorem LAMl_11[simp]:
-  !vs. (LAMl vs x = LAMl vs y) = (x = y)
-Proof
-  Induct THEN SRW_TAC [][]
-QED
-
-Theorem size_LAMl[simp]:
-  !vs. size (LAMl vs M) = LENGTH vs + size M
-Proof
-  Induct THEN SRW_TAC [numSimps.ARITH_ss][size_thm]
-QED
-
-Theorem LAMl_eq_VAR[simp]:
-  (LAMl vs M = VAR v) ⇔ (vs = []) ∧ (M = VAR v)
-Proof
-  Cases_on ‘vs’ >> simp[]
-QED
-
-Theorem LAMl_eq_APP[simp]:
-  (LAMl vs M = N @@ P) ⇔ (vs = []) ∧ (M = N @@ P)
-Proof
-  Cases_on ‘vs’ >> simp[]
-QED
-
-Theorem LAMl_eq_appstar:
-  (LAMl vs M = N ·· Ns) ⇔
-    (vs = []) ∧ (M = N ·· Ns) ∨ (Ns = []) ∧ (N = LAMl vs M)
-Proof
-  Cases_on ‘vs’ >> simp[] >> Cases_on ‘Ns’ >> simp[] >>
-  metis_tac[]
-QED
-
-Theorem is_abs_LAMl[simp]:
-  is_abs (LAMl vs M) ⇔ vs ≠ [] ∨ is_abs M
-Proof
-  Cases_on ‘vs’ >> simp[]
-QED
-
-val LAMl_vsub = store_thm(
-  "LAMl_vsub",
-  ``!vs u v M.
-        ~MEM u vs /\ ~MEM v vs ==>
-        ([VAR v/u] (LAMl vs M) = LAMl vs ([VAR v/u] M))``,
-  Induct THEN SRW_TAC [][] THEN
-  Q_TAC (NEW_TAC "z") `LIST_TO_SET vs UNION {h;v;u} UNION FV (LAMl vs M) UNION
-                       FV (LAMl vs ([VAR v/u] M))` THEN
-  `LAM h (LAMl vs M) = LAM z ([VAR z/h] (LAMl vs M))`
-     by SRW_TAC [][SIMPLE_ALPHA] THEN
-  `LAM h (LAMl vs ([VAR v/u] M)) = LAM z ([VAR z/h] (LAMl vs ([VAR v/u] M)))`
-     by SRW_TAC [][SIMPLE_ALPHA] THEN
-  SRW_TAC [][SUB_THM]);
-
-val FV_LAMl = store_thm(
-  "FV_LAMl",
-  ``!vs M. FV (LAMl vs M) = FV M DIFF LIST_TO_SET vs``,
-  Induct THEN SRW_TAC [][] THEN
-  SIMP_TAC (srw_ss()) [EXTENSION] THEN PROVE_TAC []);
-
-val LAMl_vsub_disappears = store_thm(
-  "LAMl_vsub_disappears",
- ``!vs u v M. MEM u vs ==> ([VAR v/u] (LAMl vs M) = LAMl vs M)``,
-  Induct THEN SRW_TAC [][] THENL [
-    SRW_TAC [][SUB_THM, lemma14b],
-    `~(u IN FV (LAMl vs M))` by SRW_TAC [][FV_LAMl] THEN
-    `LAM h (LAMl vs M) = LAM u ([VAR u/h] (LAMl vs M))`
-       by SRW_TAC [][SIMPLE_ALPHA] THEN
-    SRW_TAC [][SUB_THM, lemma14b]
-  ]);
-
-val SUB_ISUB_SINGLETON = store_thm(
-  "SUB_ISUB_SINGLETON",
-  ``!t x u. [t/x]u:term = u ISUB [(t,x)]``,
-  SRW_TAC [][ISUB_def]);
-
-val ISUB_APPEND = store_thm(
-  "ISUB_APPEND",
-  ``!R1 R2 t:term. (t ISUB R1) ISUB R2 = t ISUB (APPEND R1 R2)``,
-  Induct THEN
-  ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, ISUB_def]);
-
-val LAMl_ALPHA = store_thm(
-  "LAMl_ALPHA",
-  ``!vs vs' M.
-       (LENGTH vs = LENGTH vs') /\ ALL_DISTINCT vs' /\
-       DISJOINT (LIST_TO_SET vs') (LIST_TO_SET vs UNION FV M) ==>
-       (LAMl vs M = LAMl vs' (M ISUB REVERSE (ZIP(MAP VAR vs', vs))))``,
-  Induct THENL [
-    SRW_TAC [][] THEN
-    FULL_SIMP_TAC (srw_ss()) [ISUB_def],
-    SRW_TAC [][] THEN
-    Cases_on `vs'` THEN
-    FULL_SIMP_TAC (srw_ss()) [DISJ_IMP_THM, FORALL_AND_THM] THEN
-    `~(h' IN LIST_TO_SET vs) /\ ~(h' IN FV M) /\
-     DISJOINT (LIST_TO_SET vs) (LIST_TO_SET t) /\
-     DISJOINT (FV M) (LIST_TO_SET t)`
-        by PROVE_TAC [DISJOINT_INSERT, DISJOINT_SYM] THEN
-    Q_TAC SUFF_TAC `~(h' IN FV (LAMl vs M)) /\
-                    (LAMl t (M ISUB APPEND (REVERSE (ZIP (MAP VAR t, vs)))
-                                           [(VAR h',h)]) =
-                     [VAR h'/h] (LAMl vs M))` THEN1
-       SRW_TAC [][SIMPLE_ALPHA] THEN
-    ASM_SIMP_TAC (srw_ss()) [FV_LAMl] THEN
-    FIRST_X_ASSUM (Q.SPECL_THEN [`t`, `M`] MP_TAC) THEN
-    ASM_SIMP_TAC (srw_ss()) [] THEN
-    DISCH_THEN (K ALL_TAC) THEN
-    SRW_TAC [][LAMl_vsub, SUB_ISUB_SINGLETON, ISUB_APPEND]
-  ]);
-
 val FRESH_lists = store_thm(
   "FRESH_lists",
   ``!n s : string set.
@@ -1376,50 +1149,6 @@ val RENAMING_ZIP_MAP_VAR = store_thm(
 
 val _ = augment_srw_ss [rewrites [RENAMING_REVERSE, RENAMING_ZIP_MAP_VAR]]
 
-val is_comb_LAMl = store_thm(
-  "is_comb_LAMl",
-  ``is_comb (LAMl vs M) = (vs = []) /\ is_comb M``,
-  Cases_on `vs` THEN SRW_TAC [][]);
-val _ = export_rewrites ["is_comb_LAMl"]
-
-val strange_cases = prove(
-  ``!M : term. (?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/
-                (?vs args t.
-                         (M = LAMl vs (FOLDL APP t args)) /\
-                         ~(args = []) /\ ~is_comb t)``,
-  HO_MATCH_MP_TAC simple_induction THEN REPEAT CONJ_TAC THENL [
-    (* VAR *) GEN_TAC THEN DISJ1_TAC THEN
-              MAP_EVERY Q.EXISTS_TAC [`[]`, `VAR s`] THEN SRW_TAC [][size_thm],
-    (* app *) MAP_EVERY Q.X_GEN_TAC [`M`,`N`] THEN
-              DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) THEN
-              DISJ2_TAC THEN Q.EXISTS_TAC `[]` THEN
-              SIMP_TAC (srw_ss()) [] THEN
-              `(?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/
-               (?vs args t.
-                        (M = LAMl vs (FOLDL APP t args)) /\ ~(args = []) /\
-                        ~is_comb t)` by PROVE_TAC []
-              THENL [
-                MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN
-                ASM_SIMP_TAC (srw_ss()) [] THEN
-                PROVE_TAC [combs_not_size_1],
-                ASM_SIMP_TAC (srw_ss()) [] THEN
-                Cases_on `vs` THENL [
-                  MAP_EVERY Q.EXISTS_TAC [`APPEND args [N]`, `t`] THEN
-                  ASM_SIMP_TAC (srw_ss()) [foldl_snoc],
-                  MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN
-                  ASM_SIMP_TAC (srw_ss()) []
-                ]
-              ],
-    (* LAM *) MAP_EVERY Q.X_GEN_TAC [`x`,`M`] THEN STRIP_TAC THENL [
-                DISJ1_TAC THEN
-                MAP_EVERY Q.EXISTS_TAC [`x::vs`, `M'`] THEN
-                ASM_SIMP_TAC (srw_ss()) [],
-                DISJ2_TAC THEN
-                MAP_EVERY Q.EXISTS_TAC [`x::vs`, `args`, `t`] THEN
-                ASM_SIMP_TAC (srw_ss()) []
-              ]
-  ]);
-
 val head_reduction_standard = store_thm(
   "head_reduction_standard",
   ``!s. is_head_reduction s ==> standard_reduction s``,
@@ -2383,7 +2112,7 @@ val hnf_reflected_over_ireduction = store_thm(
   SRW_TAC [][hnf_no_head_redex, i_reduce1_def] THEN
   METIS_TAC [lemma11_4_3ii]);
 
-(* NOTE: this is also Theorem 8.3.11 [1, p. 174] *)
+(* NOTE: This is also Theorem 8.3.11 [1, p.174] *)
 val corollary11_4_8 = store_thm(
   "corollary11_4_8",
   ``!M. has_hnf M = finite (head_reduction_path M)``,
@@ -2433,130 +2162,6 @@ val has_bnf_whnf = store_thm(
   ``has_bnf M ⇒ has_whnf M``,
   METIS_TAC [has_bnf_hnf, has_hnf_whnf]);
 
-(*---------------------------------------------------------------------------*
- * More results about LAMl (added by Chun Tian)
- *---------------------------------------------------------------------------*)
-
-(* copied from chap2Script.sml *)
-fun betafy ss =
-    simpLib.add_relsimp {refl = GEN_ALL lameq_refl,
-                         trans = List.nth(CONJUNCTS lameq_rules, 3),
-                         weakenings = [lameq_weaken_cong],
-                         subsets = [],
-                         rewrs = [hd (CONJUNCTS lameq_rules)]} ss ++
-    simpLib.SSFRAG {rewrs = [],
-                    ac = [],  convs = [],
-                    congs = [lameq_app_cong,
-                             SPEC_ALL (last (CONJUNCTS lameq_rules)),
-                             lameq_sub_cong],
-                    dprocs = [], filter = NONE, name = NONE};
-
-Theorem LAMl_SUB :
-    !M N v vs. ALL_DISTINCT vs /\ ~MEM v vs /\ (FV N = {}) ==>
-               [N/v] (LAMl vs M) == LAMl vs ([N/v] M)
-Proof
-    rpt STRIP_TAC
- >> Induct_on ‘vs’ >> rw []
- >> ASM_SIMP_TAC (betafy (srw_ss())) []
-QED
-
-Theorem LAMl_appstar :
-    !vs M Ns. ALL_DISTINCT vs /\ (LENGTH vs = LENGTH Ns) /\ EVERY closed Ns ==>
-              LAMl vs M @* Ns == (FEMPTY |++ ZIP (vs,Ns)) ' M
-Proof
-    rpt STRIP_TAC
- >> NewQ.ABBREV_TAC ‘L = ZIP (vs,Ns)’
- >> ‘(Ns = MAP SND L) /\ (vs = MAP FST L)’ by rw [Abbr ‘L’, MAP_ZIP]
- >> FULL_SIMP_TAC std_ss []
- >> Q.PAT_X_ASSUM ‘EVERY closed (MAP SND L)’ MP_TAC
- >> Q.PAT_X_ASSUM ‘ALL_DISTINCT (MAP FST L)’ MP_TAC
- >> KILL_TAC
- >> Q.ID_SPEC_TAC ‘M’
- >> Induct_on ‘L’ >> rw []
- >- (Suff ‘FEMPTY |++ [] = FEMPTY :string |-> term’ >- rw [] \\
-     rw [FUPDATE_LIST_EQ_FEMPTY])
- >> NewQ.ABBREV_TAC ‘v = FST h’
- >> NewQ.ABBREV_TAC ‘vs = MAP FST L’
- >> NewQ.ABBREV_TAC ‘N = SND h’
- >> NewQ.ABBREV_TAC ‘Ns = MAP SND L’
- (* RHS rewriting *)
- >> ‘h :: L = [h] ++ L’ by rw [] >> POP_ORW
- >> rw [FUPDATE_LIST_APPEND]
- >> Know ‘FEMPTY |++ [h] |++ L = FEMPTY |++ L |++ [h]’
- >- (MATCH_MP_TAC FUPDATE_LIST_APPEND_COMMUTES \\
-     rw [DISJOINT_ALT])
- >> Rewr'
- >> rw [GSYM FUPDATE_EQ_FUPDATE_LIST]
- >> NewQ.ABBREV_TAC ‘fm = FEMPTY |++ L’
- >> FULL_SIMP_TAC std_ss []
- >> ‘h = (v,N)’ by rw [Abbr ‘v’, Abbr ‘N’] >> POP_ORW
- >> Know ‘(fm |+ (v,N)) ' M = fm ' ([N/v] M)’
- >- (MATCH_MP_TAC ssub_update_apply' \\
-     Q.PAT_X_ASSUM ‘closed N’ MP_TAC \\
-     rw [Abbr ‘fm’, FDOM_FUPDATE_LIST, closed_def] \\
-     Cases_on ‘INDEX_OF y vs’ >- fs [INDEX_OF_eq_NONE] \\
-     rename1 ‘INDEX_OF y vs = SOME n’ \\
-     fs [INDEX_OF_eq_SOME] \\
-     Q.PAT_X_ASSUM ‘EL n vs = y’ (ONCE_REWRITE_TAC o wrap o SYM) \\
-    ‘LENGTH L = LENGTH vs’ by rw [Abbr ‘vs’, LENGTH_MAP] \\
-     Know ‘(FEMPTY |++ L) ' (EL n vs) = EL n Ns’
-     >- (MATCH_MP_TAC FUPDATE_LIST_APPLY_MEM \\
-         Q.EXISTS_TAC ‘n’ >> rw [] \\
-        ‘m <> n’ by rw [] \\
-         METIS_TAC [EL_ALL_DISTINCT_EL_EQ]) >> Rewr' \\
-     Q.PAT_X_ASSUM ‘EVERY closed Ns’ MP_TAC \\
-     rw [EVERY_MEM, closed_def] \\
-     POP_ASSUM MATCH_MP_TAC >> rw [MEM_EL] \\
-    ‘LENGTH L = LENGTH Ns’ by rw [Abbr ‘Ns’, LENGTH_MAP] \\
-     Q.EXISTS_TAC ‘n’ >> rw [])
- >> Rewr'
- (* LHS rewriting *)
- >> Know ‘LAM v (LAMl vs M) @@ N == LAMl vs ([N/v] M)’
- >- (SIMP_TAC (betafy (srw_ss())) [] \\
-     MATCH_MP_TAC LAMl_SUB \\
-     Q.PAT_X_ASSUM ‘closed N’ MP_TAC >> rw [closed_def])
- >> DISCH_TAC
- >> MATCH_MP_TAC lameq_TRANS
- >> Q.EXISTS_TAC ‘LAMl vs ([N/v] M) @* Ns’ >> art []
- >> MATCH_MP_TAC lameq_appstar_cong >> art []
-QED
-
-Theorem hnf_LAMl[simp] :
-    hnf (LAMl vs M) <=> hnf M
-Proof
-    Induct_on ‘vs’ >> rw []
-QED
-
-Theorem is_abs_appstar[simp]:
-  is_abs (M @* Ns) ⇔ is_abs M ∧ (Ns = [])
-Proof
-  Induct_on ‘Ns’ using SNOC_INDUCT >>
-  simp[appstar_SNOC]
-QED
-
-Theorem hnf_appstar :
-    !M Ns. hnf (M @* Ns) <=> hnf M /\ (is_abs M ⇒ (Ns = []))
-Proof
-  Induct_on ‘Ns’ using SNOC_INDUCT >> simp[appstar_SNOC] >>
-  dsimp[SF CONJ_ss] >> metis_tac[]
-QED
-
-Theorem hnf_cases :
-  !M : term. hnf M <=> ?vs args y. M = LAMl vs (VAR y @* args)
-Proof
-  simp[FORALL_AND_THM, EQ_IMP_THM] >> conj_tac
-  >- (gen_tac >> MP_TAC (Q.SPEC ‘M’ strange_cases)
-      >> RW_TAC std_ss []
-      >- (FULL_SIMP_TAC std_ss [size_1] \\
-          qexistsl_tac [‘vs’, ‘[]’, ‘y’] >> rw [])
-      >> FULL_SIMP_TAC std_ss [hnf_LAMl]
-      >> ‘hnf t /\ ~is_abs t’ by PROVE_TAC [hnf_appstar]
-      >> ‘is_var t’ by METIS_TAC [term_cases]
-      >> FULL_SIMP_TAC std_ss [is_var_cases]
-      >> qexistsl_tac [‘vs’, ‘args’, ‘y’] >> art []) >>
-  simp[PULL_EXISTS, hnf_appstar]
-QED
-
 (* Proposition 8.3.13 (i) [1, p.174] *)
 Theorem has_hnf_iff_LAM[simp] :
     !x M. has_hnf (LAM x M) <=> has_hnf M
@@ -2566,7 +2171,6 @@ Proof
  >> rpt STRIP_TAC
  >- (Q.EXISTS_TAC ‘LAM x N’ \\
      CONJ_TAC >- PROVE_TAC [lameq_rules] \\
-    ‘?vs args y. N = LAMl vs (VAR y @* args)’ by METIS_TAC [hnf_cases] \\
      rw [hnf_cases])
  (* stage work *)
  >> ‘?Z. LAM x M -b->* Z /\ N -b->* Z’ by METIS_TAC [lameq_CR]
diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml
index b5f8605a1a..1ed781fd8c 100644
--- a/examples/lambda/basics/appFOLDLScript.sml
+++ b/examples/lambda/basics/appFOLDLScript.sml
@@ -1,9 +1,8 @@
-open HolKernel Parse boolLib bossLib
+open HolKernel Parse boolLib bossLib;
 
-open arithmeticTheory listTheory
-open termTheory
+open arithmeticTheory listTheory pred_setTheory hurdUtils;
 
-fun Store_thm(trip as (n,t,tac)) = store_thm trip before export_rewrites [n]
+open termTheory binderLib;
 
 val _ = new_theory "appFOLDL"
 
@@ -174,4 +173,134 @@ Proof
     Induct_on ‘Ns’ using SNOC_INDUCT >> simp[appstar_SNOC, MAP_SNOC]
 QED
 
+(*---------------------------------------------------------------------------*
+ *  LAMl (was in standardisationTheory)
+ *---------------------------------------------------------------------------*)
+
+Definition LAMl_def:
+  LAMl vs (t : term) = FOLDR LAM t vs
+End
+
+Theorem LAMl_thm[simp]:
+  (LAMl [] M = M) /\
+  (LAMl (h::t) M = LAM h (LAMl t M))
+Proof SRW_TAC [][LAMl_def]
+QED
+
+Theorem LAMl_11[simp]:
+  !vs. (LAMl vs x = LAMl vs y) = (x = y)
+Proof
+  Induct THEN SRW_TAC [][]
+QED
+
+Theorem size_LAMl[simp]:
+  !vs. size (LAMl vs M) = LENGTH vs + size M
+Proof
+  Induct THEN SRW_TAC [numSimps.ARITH_ss][size_thm]
+QED
+
+Theorem FV_LAMl :
+    !vs M. FV (LAMl vs M) = FV M DIFF LIST_TO_SET vs
+Proof
+  Induct THEN SRW_TAC [][] THEN
+  SIMP_TAC (srw_ss()) [EXTENSION] THEN PROVE_TAC []
+QED
+
+Theorem LAMl_eq_VAR[simp]:
+  (LAMl vs M = VAR v) ⇔ (vs = []) ∧ (M = VAR v)
+Proof
+  Cases_on ‘vs’ >> simp[]
+QED
+
+Theorem LAMl_eq_APP[simp]:
+  (LAMl vs M = N @@ P) ⇔ (vs = []) ∧ (M = N @@ P)
+Proof
+  Cases_on ‘vs’ >> simp[]
+QED
+
+Theorem LAMl_eq_appstar:
+  (LAMl vs M = N ·· Ns) ⇔
+    (vs = []) ∧ (M = N ·· Ns) ∨ (Ns = []) ∧ (N = LAMl vs M)
+Proof
+  Cases_on ‘vs’ >> simp[] >> Cases_on ‘Ns’ >> simp[] >>
+  metis_tac[]
+QED
+
+Theorem LAMl_SUB :
+    !M N v vs. ALL_DISTINCT vs /\ ~MEM v vs /\ (FV N = {}) ==>
+              ([N/v] (LAMl vs M) = LAMl vs ([N/v] M))
+Proof
+    rpt STRIP_TAC
+ >> Induct_on ‘vs’ >> rw []
+QED
+
+Theorem tpm_LAMl:
+  tpm π (LAMl vs M) = LAMl (listpm string_pmact π vs) (tpm π M)
+Proof
+  Induct_on ‘vs’ >> simp[]
+QED
+
+Theorem tpm_appstar:
+  tpm π (M ·· Ms) = tpm π M ·· listpm term_pmact π Ms
+Proof
+  qid_spec_tac ‘M’ >> Induct_on ‘Ms’ >> simp[]
+QED
+
+Theorem LAMl_vsub :
+    !vs u v M.
+        ~MEM u vs /\ ~MEM v vs ==>
+        ([VAR v/u] (LAMl vs M) = LAMl vs ([VAR v/u] M))
+Proof
+  Induct THEN SRW_TAC [][] THEN
+  Q_TAC (NEW_TAC "z") `LIST_TO_SET vs UNION {h;v;u} UNION FV (LAMl vs M) UNION
+                       FV (LAMl vs ([VAR v/u] M))` THEN
+  `LAM h (LAMl vs M) = LAM z ([VAR z/h] (LAMl vs M))`
+     by SRW_TAC [][SIMPLE_ALPHA] THEN
+  `LAM h (LAMl vs ([VAR v/u] M)) = LAM z ([VAR z/h] (LAMl vs ([VAR v/u] M)))`
+     by SRW_TAC [][SIMPLE_ALPHA] THEN
+  SRW_TAC [][SUB_THM]
+QED
+
+Theorem LAMl_vsub_disappears :
+   !vs u v M. MEM u vs ==> ([VAR v/u] (LAMl vs M) = LAMl vs M)
+Proof
+  Induct THEN SRW_TAC [][] THENL [
+    SRW_TAC [][SUB_THM, lemma14b],
+    `~(u IN FV (LAMl vs M))` by SRW_TAC [][FV_LAMl] THEN
+    `LAM h (LAMl vs M) = LAM u ([VAR u/h] (LAMl vs M))`
+       by SRW_TAC [][SIMPLE_ALPHA] THEN
+    SRW_TAC [][SUB_THM, lemma14b]
+  ]
+QED
+
+Theorem LAMl_ALPHA :
+    !vs vs' M.
+       (LENGTH vs = LENGTH vs') /\ ALL_DISTINCT vs' /\
+       DISJOINT (LIST_TO_SET vs') (LIST_TO_SET vs UNION FV M) ==>
+       (LAMl vs M = LAMl vs' (M ISUB REVERSE (ZIP(MAP VAR vs', vs))))
+Proof
+  Induct THENL [
+    SRW_TAC [][] THEN
+    FULL_SIMP_TAC (srw_ss()) [ISUB_def],
+    SRW_TAC [][] THEN
+    Cases_on `vs'` THEN
+    FULL_SIMP_TAC (srw_ss()) [DISJ_IMP_THM, FORALL_AND_THM] THEN
+    `~(h' IN LIST_TO_SET vs) /\ ~(h' IN FV M) /\
+     DISJOINT (LIST_TO_SET vs) (LIST_TO_SET t) /\
+     DISJOINT (FV M) (LIST_TO_SET t)`
+        by PROVE_TAC [DISJOINT_INSERT, DISJOINT_SYM] THEN
+    Q_TAC SUFF_TAC `~(h' IN FV (LAMl vs M)) /\
+                    (LAMl t (M ISUB APPEND (REVERSE (ZIP (MAP VAR t, vs)))
+                                           [(VAR h',h)]) =
+                     [VAR h'/h] (LAMl vs M))` THEN1
+       SRW_TAC [][SIMPLE_ALPHA] THEN
+    ASM_SIMP_TAC (srw_ss()) [FV_LAMl] THEN
+    FIRST_X_ASSUM (Q.SPECL_THEN [`t`, `M`] MP_TAC) THEN
+    ASM_SIMP_TAC (srw_ss()) [] THEN
+    DISCH_THEN (K ALL_TAC) THEN
+    SRW_TAC [][LAMl_vsub, SUB_ISUB_SINGLETON, ISUB_APPEND]
+  ]
+QED
+
 val _ = export_theory ()
+val _ = html_theory "appFOLDL";
diff --git a/examples/lambda/basics/nomsetScript.sml b/examples/lambda/basics/nomsetScript.sml
index 1b21b35f1b..303ce92367 100644
--- a/examples/lambda/basics/nomsetScript.sml
+++ b/examples/lambda/basics/nomsetScript.sml
@@ -557,6 +557,13 @@ val MEM_listpm_EXISTS = store_thm(
 val _ = overload_on("cpm_pmact", ``list_pmact (pair_pmact string_pmact string_pmact)``);
 val _ = overload_on ("cpmpm", ``pmact cpm_pmact``);
 
+(* moved here from sttScript.sml *)
+Theorem ALL_DISTINCT_listpm[simp]:
+  ALL_DISTINCT (listpm act π xs) = ALL_DISTINCT xs
+Proof
+  Induct_on ‘xs’ >> simp[MEM_listpm]
+QED
+
 (* ----------------------------------------------------------------------
     Notion of support, and calculating the smallest set of support
    ---------------------------------------------------------------------- *)
diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml
index 468cf0d060..91a012b892 100644
--- a/examples/lambda/basics/termScript.sml
+++ b/examples/lambda/basics/termScript.sml
@@ -305,6 +305,14 @@ val FV_tpm = Save_thm("FV_tpm",
 val _ = set_mapped_fixity { term_name = "APP", tok = "@@",
                             fixity = Infixl 901}
 
+(* NOTE: The following overload "incompatible" was in sttScript.sml.
+
+   The current "incompatibility" is between a (string) variable and a term.
+   See chap2Theory for the incompatibility bwtween two terms.
+ *)
+val _ = set_fixity "#" (Infix(NONASSOC, 450))
+Overload "#" = “λv M:term. v ∉ FV M”
+
 Theorem FRESH_APP[simp]: v NOTIN FV (M @@ N) <=> v NOTIN FV M /\ v NOTIN FV N
 Proof SRW_TAC [][]
 QED
@@ -570,7 +578,7 @@ QED
 Theorem size_nz =
     REWRITE_RULE [GSYM arithmeticTheory.NOT_ZERO_LT_ZERO] size_nonzero
 
-Theorem size_1 :
+Theorem size_1_cases :
     (size M = 1) <=> ?y. (M = VAR y)
 Proof
     Q.SPEC_THEN `M` STRUCT_CASES_TAC term_CASES
@@ -620,6 +628,17 @@ val ISUB_LAM = store_thm(
   ASM_SIMP_TAC (srw_ss()) [ISUB_def, pairTheory.FORALL_PROD,
                            DOM_DEF, FVS_DEF, SUB_THM]);
 
+val SUB_ISUB_SINGLETON = store_thm(
+  "SUB_ISUB_SINGLETON",
+  ``!t x u. [t/x]u:term = u ISUB [(t,x)]``,
+  SRW_TAC [][ISUB_def]);
+
+val ISUB_APPEND = store_thm(
+  "ISUB_APPEND",
+  ``!R1 R2 t:term. (t ISUB R1) ISUB R2 = t ISUB (APPEND R1 R2)``,
+  Induct THEN
+  ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, ISUB_def]);
+
 (* ----------------------------------------------------------------------
     Simultaneous substitution (using a finite map) - much more interesting
    ---------------------------------------------------------------------- *)
diff --git a/examples/lambda/typing/sttScript.sml b/examples/lambda/typing/sttScript.sml
index b880aa4470..3904619a1f 100644
--- a/examples/lambda/typing/sttScript.sml
+++ b/examples/lambda/typing/sttScript.sml
@@ -335,75 +335,6 @@ val (ground_subterms_def, _) = define_recursive_term_function ‘
 ’
 val _ = export_rewrites ["ground_subterms_def"]
 
-Theorem APP_EQ_LAMl[simp]:
-  M @@ N = LAMl vs P ⇔ vs = [] ∧ P = M @@ N
-Proof
-  Cases_on ‘vs’ >> simp[] >> metis_tac[]
-QED
-
-Theorem is_abs_appstar[simp]:
-  is_abs (M ·· Ms) ⇔ is_abs M ∧ Ms = []
-Proof
-  qid_spec_tac ‘M’ >> Induct_on ‘Ms’ >> simp[]
-QED
-
-Theorem appstar_EQ_LAMl:
-  x ·· Ms = LAMl vs M ⇔ vs = [] ∧ M = x ·· Ms ∨ Ms = [] ∧ x = LAMl vs M
-Proof
-  Cases_on ‘vs’ >> simp[] >> Cases_on ‘Ms’ >> simp[] >> metis_tac[]
-QED
-
-Theorem tpm_LAMl:
-  tpm π (LAMl vs M) = LAMl (listpm string_pmact π vs) (tpm π M)
-Proof
-  Induct_on ‘vs’ >> simp[]
-QED
-
-Theorem tpm_appstar:
-  tpm π (M ·· Ms) = tpm π M ·· listpm term_pmact π Ms
-Proof
-  qid_spec_tac ‘M’ >> Induct_on ‘Ms’ >> simp[]
-QED
-
-Theorem ALL_DISTINCT_listpm[simp]:
-  ALL_DISTINCT (listpm act π xs) = ALL_DISTINCT xs
-Proof
-  Induct_on ‘xs’ >> simp[MEM_listpm]
-QED
-
-Theorem bnf_characterisation:
-  ∀M.
-    bnf M ⇔
-      ∃vs v Ms. ALL_DISTINCT vs ∧ M = LAMl vs (VAR v ·· Ms) ∧
-                (∀M. MEM M Ms ⇒ bnf M)
-Proof
-  ho_match_mp_tac nc_INDUCTION2 >> qexists ‘∅’ >> rw[] >~
-  [‘VAR _ ·· _ = M1 @@ M2’]
-  >- (simp[] >> eq_tac >> rpt strip_tac >~
-      [‘M1 = LAMl vs1 _’, ‘M1 @@ M2’]
-      >- (gvs[app_eq_appstar] >>
-          Q.REFINE_EXISTS_TAC ‘SNOC M Mt’ >>
-          simp[DISJ_IMP_THM, rich_listTheory.FRONT_APPEND] >>
-          metis_tac[]) >>
-      Cases_on ‘Ms’ using rich_listTheory.SNOC_CASES >>
-      gvs[rich_listTheory.SNOC_APPEND, appstar_APPEND] >>
-      dsimp[appstar_EQ_LAMl] >> irule_at Any EQ_REFL >> simp[]) >>
-  pop_assum SUBST_ALL_TAC >> eq_tac >> rpt strip_tac >> gvs[] >~
-  [‘LAM y (LAMl vs _)’]
-  >- (reverse (Cases_on ‘MEM y vs’)
-      >- (qexists ‘y::vs’ >> simp[]) >>
-      ‘y # LAMl vs (VAR v ·· Ms)’ by simp[FV_LAMl] >>
-      Q_TAC (NEW_TAC "z") ‘y INSERT set vs ∪ FV (VAR v ·· Ms)’ >>
-      ‘z # LAMl vs (VAR v ·· Ms)’ by simp[FV_LAMl] >>
-      dxrule_then (qspec_then ‘y’ mp_tac) tpm_ALPHA >>
-      simp[tpm_fresh, FV_LAMl] >> strip_tac >> qexists ‘z::vs’ >> simp[]) >>
-  rename [‘LAM y M = LAMl vs (VAR v ·· Ms)’] >>
-  Cases_on ‘vs’ >> gvs[] >> gvs[LAM_eq_thm]
-  >- metis_tac[] >>
-  simp[tpm_LAMl, tpm_appstar] >> irule_at Any EQ_REFL >>
-  simp[MEM_listpm] >> rpt strip_tac >> first_assum drule >> simp[]
-QED
-
 (*