Minor tweaks and polishing in examples/lambda

examples/lambda/barendregt/chap3Script.sml

@@ -311,7 +311,7 @@ val bvc_cases = store_thm(
 
 (* Definition 3.2.3 [1, p60] (one-step parallel beta-reduction) *)
 Inductive grandbeta :
-[~REFL:]
+[~REFL[simp]:]
   !M. grandbeta M M
 [~ABS:]
   !M M' x. grandbeta M M' ==> grandbeta (LAM x M) (LAM x M')
@@ -1472,13 +1472,6 @@ Proof
   Induct_on ‘RTC’ >> metis_tac[reduction_rules, LAMl_beta_cong]
 QED
 
-Theorem tpm_eql:
-  tpm π t = u ⇔ t = tpm π⁻¹ u
-Proof
-  simp[tpm_eqr]
-QED
-
-
 Theorem has_benf_thm:
   has_benf M ⇔ ∃N. M -βη->* N ∧ benf N
 Proof

examples/lambda/barendregt/finite_developmentsScript.sml

@@ -2332,22 +2332,20 @@ val size_vsubst = prove(
   HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN
   SRW_TAC [][SUB_THM, SUB_VAR]);
 
-val old_induction = prove(
-  ``!P. (!x. P (VAR x)) /\
-        (!t u. P t /\ P u ==> P (t @@ u)) /\
-        (!x u. (!y'. P ([VAR y'/x] u)) ==> P (LAM x u)) ==>
-        !u:term. P u``,
+Theorem old_induction[local]:
+  !P. (!x. P (VAR x)) /\
+      (!t u. P t /\ P u ==> P (t @@ u)) /\
+      (!x u. (!y'. P ([VAR y'/x] u)) ==> P (LAM x u)) ==>
+      !u:term. P u
+Proof
   REPEAT STRIP_TAC THEN
   completeInduct_on `size u` THEN GEN_TAC THEN
   Q.SPEC_THEN `u` STRUCT_CASES_TAC term_CASES THEN
-  SRW_TAC [][] THENL [
-    FIRST_X_ASSUM MATCH_MP_TAC THEN
-    FULL_SIMP_TAC (srw_ss()) [GSYM RIGHT_FORALL_IMP_THM] THEN
-    SRW_TAC [numSimps.ARITH_ss][],
-    FIRST_X_ASSUM MATCH_MP_TAC THEN
-    FULL_SIMP_TAC (srw_ss()) [GSYM RIGHT_FORALL_IMP_THM] THEN
-    SRW_TAC [numSimps.ARITH_ss][size_vsubst]
-  ]);
+  SRW_TAC [][] THEN
+  FIRST_X_ASSUM MATCH_MP_TAC THEN
+  FULL_SIMP_TAC (srw_ss()) [GSYM RIGHT_FORALL_IMP_THM] THEN
+  SRW_TAC [numSimps.ARITH_ss][]
+QED
 
 
 val weight_at_subst = store_thm(