diff --git a/compiler/backend/languages/properties/env_cexp_lemmasScript.sml b/compiler/backend/languages/properties/env_cexp_lemmasScript.sml
index 4ec82258..372dcf70 100644
--- a/compiler/backend/languages/properties/env_cexp_lemmasScript.sml
+++ b/compiler/backend/languages/properties/env_cexp_lemmasScript.sml
@@ -48,7 +48,7 @@ Proof
   metis_tac[]
 QED
 
-Triviality MAPi_ID[simp]:
+Theorem MAPi_ID[local,simp]:
   ∀l. MAPi (λn v. v) l = l
 Proof
   Induct >> rw[combinTheory.o_DEF]
diff --git a/compiler/backend/languages/relations/pure_presScript.sml b/compiler/backend/languages/relations/pure_presScript.sml
index 6221a20c..38335b64 100644
--- a/compiler/backend/languages/relations/pure_presScript.sml
+++ b/compiler/backend/languages/relations/pure_presScript.sml
@@ -807,7 +807,7 @@ Proof
     )
 QED
 
-Triviality ALOOKUP_MAP_3':
+Theorem ALOOKUP_MAP_3'[local]:
   ALOOKUP (MAP (λ(k,v1,v2). (k,v1,f v1 v2)) l) =
   OPTION_MAP (λ(v1,v2). (v1, f v1 v2)) o ALOOKUP l
 Proof
diff --git a/compiler/backend/languages/semantics/pureLangScript.sml b/compiler/backend/languages/semantics/pureLangScript.sml
index 308b9ee7..232ff370 100644
--- a/compiler/backend/languages/semantics/pureLangScript.sml
+++ b/compiler/backend/languages/semantics/pureLangScript.sml
@@ -25,7 +25,7 @@ Definition rows_of_def:
       (lets_for cn v (MAPi (λi v. (i,v)) vs) b) (rows_of v k rest)
 End
 
-Triviality list_size_cepat_size_MAPi:
+Theorem list_size_cepat_size_MAPi[local]:
   list_size (λx. cepat_size (SND x)) (MAPi ( λi p. f i, p) ps) = list_size cepat_size ps
 Proof
   Induct_on ‘ps’ using SNOC_INDUCT >> rw[] >>
diff --git a/compiler/backend/languages/semantics/stateLangScript.sml b/compiler/backend/languages/semantics/stateLangScript.sml
index 20efafdc..0afd986c 100644
--- a/compiler/backend/languages/semantics/stateLangScript.sml
+++ b/compiler/backend/languages/semantics/stateLangScript.sml
@@ -692,7 +692,7 @@ Proof
   Induct_on ‘n’ >> rw[step,ADD1,step_n_add]
 QED
 
-Triviality application_Action:
+Theorem application_Action[local]:
   application p vs st k = (Action channel content,st1,k1) ⇒
   p = FFI channel ∧ ∃st1. st = SOME st1
 Proof
@@ -1509,7 +1509,7 @@ Proof
   \\ drule_all step'_append_cont \\ rw [] \\ gvs []
 QED
 
-Triviality step'_not_ForceK1:
+Theorem step'_not_ForceK1[local]:
   v1 ∉ avoid ∧
   step' avoid s k x = (r0,r1,r2) ∧
   (∀ts. x = Val v1 ⇒ k ≠ ForceK1::ts) ⇒
@@ -1544,7 +1544,7 @@ Proof
   \\ gvs [GSYM ADD1, step'_n_def, FUNPOW]
 QED
 
-Triviality step'_n_not_halt_mul:
+Theorem step'_n_not_halt_mul[local]:
   ∀m n avoid x s k.
     (∀k1. ¬is_halt (x,s,k1)) ∧
     (∀k. ∃k1. step'_n n avoid (x,s,k) = (x,s,k1)) ⇒
diff --git a/compiler/backend/passes/env_to_stateScript.sml b/compiler/backend/passes/env_to_stateScript.sml
index 145110a2..4e04e32e 100644
--- a/compiler/backend/passes/env_to_stateScript.sml
+++ b/compiler/backend/passes/env_to_stateScript.sml
@@ -44,7 +44,7 @@ Definition update_delay_def:
         App (UpdateMutThunk NotEvaluated) [Var v; Lam NONE y])
 End
 
-Triviality Letrec_split_MEM_funs:
+Theorem Letrec_split_MEM_funs[local]:
   ∀xs delays funs m n x.
     (delays,funs) = Letrec_split ns xs ∧ MEM (m,n,x) funs ⇒
     cexp_size x ≤ list_size (pair_size mlstring_size cexp_size) xs
@@ -58,7 +58,7 @@ Proof
   \\ Cases_on ‘h1’ \\ gvs [dest_Lam_def,env_cexpTheory.cexp_size_def]
 QED
 
-Triviality Letrec_split_MEM_delays:
+Theorem Letrec_split_MEM_delays[local]:
   ∀xs delays funs m n x.
     (delays,funs) = Letrec_split ns xs ∧ MEM (m,n,x) delays ⇒
     cexp_size x ≤ list_size (pair_size mlstring_size cexp_size) xs
diff --git a/compiler/backend/passes/proofs/env_to_state_2ProofScript.sml b/compiler/backend/passes/proofs/env_to_state_2ProofScript.sml
index bc5005b2..0f0cefe5 100644
--- a/compiler/backend/passes/proofs/env_to_state_2ProofScript.sml
+++ b/compiler/backend/passes/proofs/env_to_state_2ProofScript.sml
@@ -49,7 +49,7 @@ Proof
   \\ rpt $ first_x_assum $ irule_at Any
 QED
 
-Triviality MEM_explode[simp]:
+Theorem MEM_explode[local,simp]:
   ∀xs x. MEM (explode x) (MAP explode xs) = MEM x xs
 Proof
   Induct \\ fs []
@@ -233,14 +233,14 @@ Proof
   \\ fs []
 QED
 
-Triviality Letrec_imm_0:
+Theorem Letrec_imm_0[local]:
   env_to_state$Letrec_imm ts m ⇒
   (∃v. m = Var v ∧ MEM v ts) ∨ ∃x y. m = Lam x y
 Proof
   Cases_on ‘m’ \\ fs [Letrec_imm_def]
 QED
 
-Triviality Letrec_imm_1:
+Theorem Letrec_imm_1[local]:
   state_unthunkProof$Letrec_imm ts m ⇒
   (∃v. m = Var v ∧ MEM v ts) ∨ ∃x y. m = Lam (SOME x) y
 Proof
@@ -249,7 +249,7 @@ Proof
   \\ fs [state_unthunkProofTheory.Letrec_imm_def]
 QED
 
-Triviality comp_Letrec_neq:
+Theorem comp_Letrec_neq[local]:
   comp_Letrec sfns se ≠ Var v ∧
   comp_Letrec sfns se ≠ Lam m n
 Proof
@@ -261,7 +261,7 @@ Proof
   \\ fs [state_unthunkProofTheory.Lets_def]
 QED
 
-Triviality expand_Case_neq:
+Theorem expand_Case_neq[local]:
   state_caseProof$expand_Case v ses se ≠ Lam x t ∧
   state_caseProof$expand_Case v ses se ≠ False
 Proof
@@ -270,7 +270,7 @@ Proof
   \\ PairCases_on ‘h’ \\ fs [state_caseProofTheory.rows_of_def]
 QED
 
-Triviality rows_of_neq:
+Theorem rows_of_neq[local]:
   rows_of x y z ≠ Lam a b ∧
   rows_of x y z ≠ Var c
 Proof
diff --git a/compiler/backend/passes/proofs/expof_caseProofScript.sml b/compiler/backend/passes/proofs/expof_caseProofScript.sml
index aca51d04..fa0a4c59 100644
--- a/compiler/backend/passes/proofs/expof_caseProofScript.sml
+++ b/compiler/backend/passes/proofs/expof_caseProofScript.sml
@@ -273,7 +273,7 @@ Proof
     \\ irule_at Any PAIR)
 QED
 
-Triviality freevars_lets_for':
+Theorem freevars_lets_for'[local]:
   ∀xs n x y.
     freevars (exp_of' p_2) = freevars (exp_of p_2) ⇒
     freevars (lets_for' n x y xs (exp_of' p_2)) =
diff --git a/compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml b/compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml
index b0454082..524d2742 100644
--- a/compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml
@@ -2642,7 +2642,7 @@ Proof
   simp[]
 QED
 
-Triviality find_IfDisj:
+Theorem find_IfDisj[local]:
   find e1 c ∅ ds e2 NONE ⇒
   find (IfDisj s p1 e1) c ∅ ds (IfDisj s p1 e2) NONE
 Proof
@@ -3611,7 +3611,7 @@ QED
 
 (********** Prove that analysis only inserts well-defined Seqs **********)
 
-Triviality empty_map_simps[simp]:
+Theorem empty_map_simps[local,simp]:
   map_ok (empty compare) ∧
   cmp_of (empty compare) = compare ∧
   to_fmap (empty compare) = FEMPTY ∧
diff --git a/compiler/backend/passes/proofs/pure_freshenProofScript.sml b/compiler/backend/passes/proofs/pure_freshenProofScript.sml
index e8044943..72e5b7fa 100644
--- a/compiler/backend/passes/proofs/pure_freshenProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_freshenProofScript.sml
@@ -156,7 +156,7 @@ Proof
   gvs[SUBSET_DEF] >> metis_tac[]
 QED
 
-Triviality boundvars_FOLDR_Let_SUBSET:
+Theorem boundvars_FOLDR_Let_SUBSET[local]:
   boundvars (FOLDR (λ(u,e) A. Let (explode u) e A) acc binds) ⊆
     boundvars acc ∪ IMAGE explode (set (MAP FST binds)) ∪
     BIGUNION (set $ MAP (boundvars o SND) binds)
@@ -200,7 +200,7 @@ Proof
   Induct_on `cnars` >> rw[IfDisj_def, letrecs_distinct_def]
 QED
 
-Triviality ALOOKUP_MAP_3':
+Theorem ALOOKUP_MAP_3'[local]:
   ALOOKUP (MAP (λ(k,v1,v2). (k,v1,f v1 v2)) l) =
   OPTION_MAP (λ(v1,v2). (v1, f v1 v2)) o ALOOKUP l
 Proof
@@ -962,7 +962,7 @@ Proof
   simp[freshen_bind_def, combinTheory.o_DEF, UNCURRY]
 QED
 
-Triviality freshen_aux_list_LENGTH:
+Theorem freshen_aux_list_LENGTH[local]:
   ∀l m avoid l' avoid'.
     freshen_aux_list m l avoid = (l', avoid')
   ⇒ LENGTH l' = LENGTH l
@@ -1640,7 +1640,7 @@ Definition varmap_rel_def:
       FLOOKUP fmap (explode k) = SOME (explode v))
 End
 
-Triviality fresh_boundvar_rel:
+Theorem fresh_boundvar_rel[local]:
   varmap_rel varmap m ∧
   vars_ok avoid ∧
   fresh_boundvar x varmap avoid = ((y,varmap'), avoid')
@@ -1654,14 +1654,14 @@ Proof
   drule_all fresh_boundvar_varmap >> strip_tac >> simp[FLOOKUP_SIMP] >> rw[]
 QED
 
-Triviality ALOOKUP_MAP_explode_FST:
+Theorem ALOOKUP_MAP_explode_FST[local]:
   ALOOKUP (MAP (λ(a,b). (explode a,b)) l) (explode k) = ALOOKUP l k
 Proof
   Induct_on `l` >> rw[] >>
   pairarg_tac >> gvs[]
 QED
 
-Triviality fresh_boundvars_rel:
+Theorem fresh_boundvars_rel[local]:
   ∀xs varmap avoid ys varmap' avoid' m.
   varmap_rel varmap m ∧
   vars_ok avoid ∧
diff --git a/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml b/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml
index 4ea50b42..24b9239f 100644
--- a/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml
@@ -355,7 +355,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality NOT_NONE_UNIT:
+Theorem NOT_NONE_UNIT[local]:
   (x ≠ NONE) ⇔ x = SOME ()
 Proof
   Cases_on ‘x’ \\ fs []
@@ -629,7 +629,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality App_Lam_to_Lets_allvars:
+Theorem App_Lam_to_Lets_allvars[local]:
   App_Lam_to_Lets exp = SOME exp1 ⇒
   allvars (exp_of exp) = allvars (exp_of exp1)
 Proof
@@ -655,7 +655,7 @@ Proof
   \\ res_tac \\ fs []
 QED
 
-Triviality MAP2_lemma:
+Theorem MAP2_lemma[local]:
   ∀vbs vbs1.
     LENGTH vbs = LENGTH vbs1 ⇒
     MAP FST (MAP2 (λ(v,_) x. (v,x)) vbs vbs1) = MAP FST vbs ∧
@@ -832,7 +832,7 @@ Definition wf_mem_def:
                cexp_wf ce ∧ letrecs_distinct (exp_of ce)
 End
 
-Triviality BIGUNION_set_SUBSET:
+Theorem BIGUNION_set_SUBSET[local]:
   BIGUNION (set xs) ⊆ z ⇔ EVERY (λx. x ⊆ z) xs
 Proof
   Induct_on ‘xs’ \\ gvs []
@@ -847,7 +847,7 @@ Proof
   \\ gvs [AC UNION_COMM UNION_ASSOC]
 QED
 
-Triviality cexp_Lets_append:
+Theorem cexp_Lets_append[local]:
   ∀xs ys x. Lets a (xs ++ ys) x = Lets a xs (Lets a ys x)
 Proof
   Induct \\ gvs [Lets_def,FORALL_PROD]
@@ -946,7 +946,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality freevars_Disj:
+Theorem freevars_Disj[local]:
   freevars (Disj v xs) ⊆ {v}
 Proof
   Induct_on ‘xs’ \\ gvs [Disj_def]
@@ -970,7 +970,7 @@ Proof
   metis_tac[avoid_set_ok_subset]
 QED
 
-Triviality App_Lam_to_Lets_avoid_set_ok:
+Theorem App_Lam_to_Lets_avoid_set_ok[local]:
   App_Lam_to_Lets e = SOME e' ⇒
   avoid_set_ok vars e = avoid_set_ok vars e'
 Proof
@@ -1627,7 +1627,7 @@ Proof
   dxrule_all freshen_global_boundvars >> simp[]
 QED
 
-Triviality freshen_cexp_disjoint_lemma:
+Theorem freshen_cexp_disjoint_lemma[local]:
   freshen_cexp e ns = (e1,ns1) ∧ avoid_set_ok ns e ∧
   cexp_wf e ∧ NestedCase_free e ∧ letrecs_distinct (exp_of e) ∧
   s ⊆ set_of ns
@@ -1647,7 +1647,7 @@ Proof
   \\ gvs [cexp_wf_def]
 QED
 
-Triviality if_lemma:
+Theorem if_lemma[local]:
   boundvars (if b then Seq Fail x else x) = boundvars x ∧
   barendregt (if b then Seq Fail x else x) = barendregt x ∧
   letrecs_distinct (if b then Seq Fail x else x) = letrecs_distinct x
@@ -1666,7 +1666,7 @@ Proof
   rw [] \\ irule inline_rel_Prim \\ gvs [inline_rel_refl]
 QED
 
-Triviality inline_rel_rows_of:
+Theorem inline_rel_rows_of[local]:
   ∀xs1 ys1.
     inline_rel xs x y ∧
     MAP FST xs1 = MAP FST ys1 ∧
diff --git a/compiler/backend/passes/proofs/pure_letrecProofScript.sml b/compiler/backend/passes/proofs/pure_letrecProofScript.sml
index ba1007b1..ef3728d9 100644
--- a/compiler/backend/passes/proofs/pure_letrecProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_letrecProofScript.sml
@@ -46,7 +46,7 @@ Proof
   \\ rw [] \\ fs [EXTENSION] \\ metis_tac []
 QED
 
-Triviality MEM_MAP_FST_make_distinct =
+Theorem MEM_MAP_FST_make_distinct[local] =
   set_MAP_FST_make_distinct |> SIMP_RULE std_ss [EXTENSION];
 
 Theorem MEM_make_distinct:
@@ -115,7 +115,7 @@ Proof
   goal_assum drule
 QED
 
-Triviality ALOOKUP_REVERSE_make_distinct:
+Theorem ALOOKUP_REVERSE_make_distinct[local]:
   ∀l x. ALOOKUP (REVERSE (make_distinct l)) x = ALOOKUP (REVERSE l) x
 Proof
   Induct >> rw[make_distinct_def] >>
@@ -131,7 +131,7 @@ Proof
   qspec_then `l` assume_tac ALOOKUP_REVERSE_make_distinct >> simp[]
 QED
 
-Triviality make_distinct_Letrec_exp_eq:
+Theorem make_distinct_Letrec_exp_eq[local]:
   ∀xs y.  Letrec xs y ≅ Letrec (make_distinct xs) y
 Proof
   rw[] >> irule exp_eq_Letrec_cong2 >>
@@ -425,7 +425,7 @@ Proof
   irule letrec_split_subst >> simp[]
 QED
 
-Triviality letrec_rel_split_subst1:
+Theorem letrec_rel_split_subst1[local]:
   letrec_rel letrec_split x y ∧
   letrec_rel letrec_split a b ⇒
   letrec_rel letrec_split (subst1 s a x) (subst1 s b y)
@@ -1136,7 +1136,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality app_bisimilarity_subst:
+Theorem app_bisimilarity_subst[local]:
   ∀fm1 e fm2.
     fmap_rel (λx y. (x ≃ y) T) fm1 fm2 ∧
     freevars e ⊆ FDOM fm1
@@ -1163,7 +1163,7 @@ Proof
   metis_tac[]
 QED
 
-Triviality beta_equality_Letrec_app_bisimilarity:
+Theorem beta_equality_Letrec_app_bisimilarity[local]:
   closed (Letrec fns e) ⇒ (Letrec fns e ≃ subst_funs fns e) T
 Proof
   rw[app_bisimilarity_eq]
@@ -1629,7 +1629,7 @@ QED
 (************)
 
 
-Triviality beta_equality_app_bisimilarity:
+Theorem beta_equality_app_bisimilarity[local]:
   closed (Let v x e) ⇒ (Let v x e ≃ subst1 v x e) T
 Proof
   rw[app_bisimilarity_eq]
diff --git a/compiler/backend/passes/proofs/pure_letrec_cexpProofScript.sml b/compiler/backend/passes/proofs/pure_letrec_cexpProofScript.sml
index 150be49a..a359ddbc 100644
--- a/compiler/backend/passes/proofs/pure_letrec_cexpProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_letrec_cexpProofScript.sml
@@ -13,20 +13,20 @@ Libs
 
 (********************)
 val _ = temp_delsimps ["nested_rows_def"]
-Triviality letrec_recurse_Lams:
+Theorem letrec_recurse_Lams[local]:
   ∀l f e. letrec_recurse f (Lams l e) = Lams l (letrec_recurse f e)
 Proof
   Induct >> rw[letrec_recurse_def, Lams_def]
 QED
 
-Triviality letrec_recurse_Apps:
+Theorem letrec_recurse_Apps[local]:
   ∀l f e. letrec_recurse f (Apps e l) =
     Apps (letrec_recurse f e) (MAP (letrec_recurse f) l)
 Proof
   Induct >> rw[letrec_recurse_def, Apps_def]
 QED
 
-Triviality letrec_recurse_rows_of:
+Theorem letrec_recurse_rows_of[local]:
   ∀n k l f. letrec_recurse f (rows_of n k l) =
     rows_of n (letrec_recurse f k)
             (MAP (λ(c,vs,e). (c, vs, letrec_recurse f e)) l)
@@ -57,7 +57,7 @@ Proof
       DISJ_IMP_THM, FORALL_AND_THM] >> metis_tac[]
 QED
 
-Triviality letrec_recurse_FOLDR_Let:
+Theorem letrec_recurse_FOLDR_Let[local]:
   (∀vnm e. MEM (vnm,e) binds ⇒ letrec_recurse f e = e) ⇒
   letrec_recurse f (FOLDR (λ(u,e) A. Let (explode u) e A) body binds) =
   FOLDR (λ(u,e) A. Let (explode u) e A) (letrec_recurse f body) binds
@@ -67,7 +67,7 @@ Proof
   metis_tac[]
 QED
 
-Triviality patguards_binds_letrec_recurse_fixpoints:
+Theorem patguards_binds_letrec_recurse_fixpoints[local]:
   ∀eps gd binds vnm e.
     patguards eps = (gd, binds) ∧
     (∀e p. MEM (e,p) eps ⇒ letrec_recurse f e = e) ∧
@@ -86,7 +86,7 @@ Proof
       letrec_recurse_def] >> metis_tac[]
 QED
 
-Triviality letrec_recurse_nested_rows:
+Theorem letrec_recurse_nested_rows[local]:
   letrec_recurse f (nested_rows (Var v) pes) =
   nested_rows (Var v) (MAP (λ(p,e). (p, letrec_recurse f e)) pes)
 Proof
@@ -390,7 +390,7 @@ Proof
       simp[lookup_list_delete, cepat_vars_l_correct])
 QED
 
-Triviality letrec_recurse_IfDisj:
+Theorem letrec_recurse_IfDisj[local]:
   letrec_recurse g (IfDisj n p1 x) =
   IfDisj n p1 (letrec_recurse g x)
 Proof
@@ -555,7 +555,7 @@ QED
 
 (********** Splitting **********)
 
-Triviality exp_of_make_Letrecs_cexp:
+Theorem exp_of_make_Letrecs_cexp[local]:
   ∀fns.
     exp_of (make_Letrecs_cexp fns e) =
       make_Letrecs (MAP (MAP (λ(fn,e). (explode fn,exp_of e))) fns) (exp_of e)
@@ -592,7 +592,7 @@ Proof
   CASE_TAC >> gvs[wf_insert]
 QED
 
-Triviality to_nums_set_eq:
+Theorem to_nums_set_eq[local]:
   set l1 = set l2 ⇒ to_nums l l1 = to_nums l l2
 Proof
   rw[] >> irule $ iffRL spt_eq_thm >> simp[] >>
@@ -604,7 +604,7 @@ Proof
   Cases_on `lookup n (to_nums l l2)` >> gvs[] >> res_tac >> fs[]
 QED
 
-Triviality top_sort_set_eq:
+Theorem top_sort_set_eq[local]:
   ∀l1 l2.
     MAP FST l1 = MAP FST l2 ∧
     LIST_REL (λa b. set a = set b) (MAP SND l1) (MAP SND l2)
@@ -622,7 +622,7 @@ Proof
   first_x_assum drule >> simp[]
 QED
 
-Triviality top_sort_aux_sets:
+Theorem top_sort_aux_sets[local]:
   ∀ns reach acc. ∃res.
     top_sort_aux ns reach acc = res ++ acc ∧
     set (FLAT res) = set ns
@@ -634,7 +634,7 @@ Proof
   gvs[EXTENSION] >> metis_tac[]
 QED
 
-Triviality top_sort_sets:
+Theorem top_sort_sets[local]:
   ∀l. set (FLAT (top_sort l)) = set (MAP FST l)
 Proof
   rw[top_sort_def] >>
diff --git a/compiler/backend/passes/proofs/pure_letrec_lamProofScript.sml b/compiler/backend/passes/proofs/pure_letrec_lamProofScript.sml
index df332b88..4139fa2d 100644
--- a/compiler/backend/passes/proofs/pure_letrec_lamProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_letrec_lamProofScript.sml
@@ -74,13 +74,13 @@ Proof
     )
 QED
 
-Triviality apps_ok_freevars_subst:
+Theorem apps_ok_freevars_subst[local]:
   ∀apps x. apps_ok apps ⇒ freevars (subst apps x) = freevars x
 Proof
   rw[freevars_equiv, apps_ok_freevars_l_subst]
 QED
 
-Triviality lams_ok_imps:
+Theorem lams_ok_imps[local]:
   ∀apps xs ys. lams_ok apps xs ys ⇒
   MAP FST xs = MAP FST ys ∧ LENGTH xs = LENGTH ys ∧ FDOM apps ⊆ set (MAP FST xs)
 Proof
@@ -88,7 +88,7 @@ Proof
   last_x_assum drule >> pairarg_tac >> gvs[] >> pairarg_tac >> gvs[]
 QED
 
-Triviality lams_ok_imp_freevars:
+Theorem lams_ok_imp_freevars[local]:
   ∀apps xs ys.
     lams_ok apps xs ys ∧ apps_ok apps
   ⇒ MAP (λ(fn,e). freevars e) xs = MAP (λ(fn,e). freevars e) ys
@@ -137,7 +137,7 @@ Proof
   irule letrec_lam_subst >> simp[]
 QED
 
-Triviality letrec_rel_lam_subst1:
+Theorem letrec_rel_lam_subst1[local]:
   letrec_rel letrec_lam x y ∧
   letrec_rel letrec_lam a b ⇒
   letrec_rel letrec_lam (subst1 s a x) (subst1 s b y)
diff --git a/compiler/backend/passes/proofs/pure_letrec_spec_cexpProofScript.sml b/compiler/backend/passes/proofs/pure_letrec_spec_cexpProofScript.sml
index cbb4d0bc..5cbf75b6 100644
--- a/compiler/backend/passes/proofs/pure_letrec_spec_cexpProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_letrec_spec_cexpProofScript.sml
@@ -185,28 +185,28 @@ Definition min_app_def[simp]:
 End
 *)
 
-Triviality boundvars_Seq_Fail[simp]:
+Theorem boundvars_Seq_Fail[local,simp]:
   boundvars (if MEM w (FLAT (MAP (FST ∘ SND) e'))
              then Seq Fail x else x) = boundvars x
 Proof
   rw [] \\ fs [boundvars_def]
 QED
 
-Triviality freevars_Seq_Fail[simp]:
+Theorem freevars_Seq_Fail[local,simp]:
   freevars (if MEM w (FLAT (MAP (FST ∘ SND) e'))
              then Seq Fail x else x) = freevars x
 Proof
   rw [] \\ fs [freevars_def]
 QED
 
-Triviality boundvars_lets_for:
+Theorem boundvars_lets_for[local]:
   ∀ts. boundvars (lets_for p_1 w ts p_2) = boundvars p_2 ∪ set (MAP SND ts)
 Proof
   Induct \\ fs [lets_for_def,FORALL_PROD,EXTENSION]
   \\ rw [] \\ eq_tac \\ rw [] \\ fs []
 QED
 
-Triviality freevars_lets_for:
+Theorem freevars_lets_for[local]:
   ∀ts. freevars (lets_for p_1 w ts p_2) =
        (freevars p_2 DIFF set (MAP SND ts)) ∪
        (if NULL ts then {} else {w})
@@ -249,7 +249,7 @@ Proof
   \\ Cases_on ‘MEM x p_1'’ \\ fs [] \\ rw []
 QED
 
-Triviality can_spec_arg_if:
+Theorem can_spec_arg_if[local]:
   can_spec_arg f bs v ts e e1 ⇒
   can_spec_arg f bs v ts (if b then Seq Fail e else e)
                          (if b then Seq Fail e1 else e1)
@@ -257,7 +257,7 @@ Proof
   rw [] \\ rpt (irule can_spec_arg_Prim \\ fs [])
 QED
 
-Triviality map_eq_lemma:
+Theorem map_eq_lemma[local]:
   ∀xs ys.
     MAP (λ(p1,p1',p2). p1') xs = MAP (λ(p1,p1',p2). p1') ys ∧
     MEM (p_1,p_1',p_2) xs ∧ MEM y p_1' ⇒
@@ -477,7 +477,7 @@ Proof
   rw [pure_expTheory.letrecs_distinct_def]
 QED
 
-Triviality UNCURRY_lemma:
+Theorem UNCURRY_lemma[local]:
   UNCURRY f = λ(x,y). f x y
 Proof
   gvs [FUN_EQ_THM]
@@ -674,7 +674,7 @@ Proof
       \\ gvs [pure_expTheory.letrecs_distinct_def])
 QED
 
-Triviality can_spec_arg_map:
+Theorem can_spec_arg_map[local]:
   ∀f vs v ws e1 e2.
     can_spec_arg f vs v ws e1 e2 ⇒
     can_spec_arg f (MAP explode vs) v (MAP explode ws) e1 e2
@@ -684,7 +684,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality delete_with_lemma:
+Theorem delete_with_lemma[local]:
   ∀xs ys.
     delete_with (MAP (K T) xs ++ [F] ++ MAP (K T) ys) (xs ++ [h] ++ ys) = xs ++ ys
 Proof
@@ -692,7 +692,7 @@ Proof
   \\ Induct \\ fs [delete_with_def]
 QED
 
-Triviality MAP_NEQ:
+Theorem MAP_NEQ[local]:
   ∀xs x. ¬MEM x xs ⇒ MAP (λv. x ≠ v) xs = MAP (K T) xs
 Proof
   Induct \\ fs []
@@ -776,7 +776,7 @@ Proof
   \\ rw [] \\ Cases_on ‘h = h'’ \\ gvs [delete_with_def]
 QED
 
-Triviality set_delete_with:
+Theorem set_delete_with[local]:
   ∀args f. set (delete_with f args) ⊆ set args
 Proof
   Induct \\ Cases_on ‘f’ \\ fs [delete_with_def]
@@ -874,7 +874,7 @@ Proof
   \\ drule_all min_call_args_el \\ fs []
 QED
 
-Triviality MEM_all_somes:
+Theorem MEM_all_somes[local]:
   ∀xs x. MEM x (all_somes xs) = MEM (SOME x) xs
 Proof
   Induct \\ fs [all_somes_def]
@@ -915,19 +915,19 @@ Proof
   \\ imp_res_tac MEM_min_call_args
 QED
 
-Triviality all_somes_map_some:
+Theorem all_somes_map_some[local]:
   ∀xs. all_somes (MAP SOME xs) = xs
 Proof
   Induct \\ fs [all_somes_def]
 QED
 
-Triviality set_map_empty:
+Theorem set_map_empty[local]:
   ∀xs. BIGUNION (set (MAP (λx. ∅) xs)) = ∅
 Proof
   fs [EXTENSION,MEM_MAP,PULL_EXISTS] \\ Cases \\ fs [] \\ metis_tac []
 QED
 
-Triviality set_MAP_explode:
+Theorem set_MAP_explode[local]:
   ∀vs. BIGUNION (set (MAP (λx. {explode x}) vs)) = set (MAP explode vs)
 Proof
   Induct \\ fs [] \\ rw [EXTENSION]
diff --git a/compiler/backend/passes/proofs/pure_to_thunkProofScript.sml b/compiler/backend/passes/proofs/pure_to_thunkProofScript.sml
index 5a3a90c9..70256d92 100644
--- a/compiler/backend/passes/proofs/pure_to_thunkProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_to_thunkProofScript.sml
@@ -16,7 +16,7 @@ Libs
   term_tactic monadsyntax dep_rewrite
 
 
-Triviality BIGUNION_set_MAP_SUBSET:
+Theorem BIGUNION_set_MAP_SUBSET[local]:
   ∀ys f t. BIGUNION (set (MAP f ys)) ⊆ t ⇔ EVERY (λy. f y ⊆ t) ys
 Proof
   Induct \\ fs []
@@ -137,7 +137,7 @@ Proof
   \\ Cases \\ simp [thunk_exp_ofTheory.cexp_wf_def]
 QED
 
-Triviality mop_of_mlstring_NONE:
+Theorem mop_of_mlstring_NONE[local]:
   mop_of_mlstring m = NONE ⇒ ~(explode m ∈ monad_cns)
 Proof
   rw [mop_of_mlstring_def]
@@ -145,7 +145,7 @@ Proof
   \\ EVAL_TAC \\ rw []
 QED
 
-Triviality mop_of_mlstring_SOME:
+Theorem mop_of_mlstring_SOME[local]:
   mop_of_mlstring m = SOME x ⇒ explode m ∈ monad_cns
 Proof
   rw [mop_of_mlstring_def]
diff --git a/compiler/backend/passes/proofs/pure_to_thunk_1ProofScript.sml b/compiler/backend/passes/proofs/pure_to_thunk_1ProofScript.sml
index 625fe11f..bcda1ce4 100644
--- a/compiler/backend/passes/proofs/pure_to_thunk_1ProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_to_thunk_1ProofScript.sml
@@ -309,27 +309,27 @@ Proof
   \\ imp_res_tac pure_expTheory.exp_size_lemma \\ fs []
 QED
 
-Triviality LIST_REL_IMP_MAP_FST_EQ:
+Theorem LIST_REL_IMP_MAP_FST_EQ[local]:
   ∀f g. LIST_REL P f g ∧ (∀x y. P x y ⇒ FST x = FST y) ⇒
         MAP FST f = MAP FST g
 Proof
   Induct \\ fs [PULL_EXISTS]
 QED
 
-Triviality IMP_UNION_DIFF_EQ_EMPTY:
+Theorem IMP_UNION_DIFF_EQ_EMPTY[local]:
   x ⊆ z ∧ y ⊆ z ⇒ x ∪ y DIFF z = ∅
 Proof
   fs [SUBSET_DEF,EXTENSION]
   \\ metis_tac []
 QED
 
-Triviality IMP_BIGUNION_SUBSET:
+Theorem IMP_BIGUNION_SUBSET[local]:
   (∀x. x IN s ⇒ x SUBSET z) ⇒ BIGUNION s SUBSET z
 Proof
   fs [SUBSET_DEF,PULL_EXISTS] \\ metis_tac []
 QED
 
-Triviality LIST_REL_ALOOKUP_REVERSE_IMP:
+Theorem LIST_REL_ALOOKUP_REVERSE_IMP[local]:
   ∀f g.
     LIST_REL P f g ∧ MAP FST f = MAP FST g ∧
     ALOOKUP (REVERSE f) n = SOME x ∧
@@ -421,7 +421,7 @@ QED
 Theorem subst_single_def[local] = pure_exp_lemmasTheory.subst1_def;
 Theorem subst1_def[local] = thunkLangTheory.subst1_def;
 
-Triviality subst1_opt_delay_arg:
+Theorem subst1_opt_delay_arg[local]:
   ∀ys idopt n e.
   (∀idx. idopt = SOME idx ⇒ idx < LENGTH ys) ⇒
   MAP (subst1 n e) (opt_delay_arg idopt ys) =
@@ -616,7 +616,7 @@ Proof
   Induct \\ rw [FDIFF_def]
 QED
 
-Triviality subst_opt_delay_arg:
+Theorem subst_opt_delay_arg[local]:
   ∀ys idopt s.
   (∀idx. idopt = SOME idx ⇒ idx < LENGTH ys) ⇒
   MAP (λe. subst s e) (opt_delay_arg idopt ys) =
@@ -2613,7 +2613,7 @@ Proof
   \\ simp [Once tick_rel_cases]
 QED
 
-Triviality eval_simps[simp]:
+Theorem eval_simps[local,simp]:
   eval (Delay e) = INR (Thunk e) ∧
   eval (Lit l) = INR (Atom l) ∧
   eval (Monad mop es) = INR (Monadic mop es) ∧
diff --git a/compiler/backend/passes/proofs/pure_to_thunk_2ProofScript.sml b/compiler/backend/passes/proofs/pure_to_thunk_2ProofScript.sml
index 1f8ee751..377e9101 100644
--- a/compiler/backend/passes/proofs/pure_to_thunk_2ProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_to_thunk_2ProofScript.sml
@@ -194,7 +194,7 @@ Proof
   \\ rpt $ goal_assum drule
 QED
 
-Triviality MEM_EQ_MEM_MAP_explode:
+Theorem MEM_EQ_MEM_MAP_explode[local]:
   ∀h1 f. MEM f h1 ⇔ MEM (explode f) (MAP explode h1)
 Proof
   Induct \\ fs []
@@ -252,7 +252,7 @@ Proof
   \\ rpt (irule_at Any thunk_case_projProofTheory.compile_rel_Var \\ fs [])
 QED
 
-Triviality freevars_Disj':
+Theorem freevars_Disj'[local]:
   ∀xs. f ≠ v ⇒ f ∉ freevars (Disj' (Force (Var v)) xs)
 Proof
   Induct \\ fs [pureLangTheory.Disj_def,FORALL_PROD,Disj'_def] \\ rw []
diff --git a/compiler/backend/passes/proofs/state_app_unitProofScript.sml b/compiler/backend/passes/proofs/state_app_unitProofScript.sml
index eefda208..29ef57e2 100644
--- a/compiler/backend/passes/proofs/state_app_unitProofScript.sml
+++ b/compiler/backend/passes/proofs/state_app_unitProofScript.sml
@@ -92,7 +92,7 @@ End
 Overload rel1 = “state_app_unit_1Proof$compile_rel”
 Overload rel2 = “state_app_unit_2Proof$compile_rel”
 
-Triviality LIST_REL_rel2_rel1:
+Theorem LIST_REL_rel2_rel1[local]:
   ∀xs zs.
     LIST_REL (λx z. cexp1_rel x z ∧ ∃y. rel2 (exp_of x) y ∧ rel1 y (exp_of z)) xs zs ⇒
     ∃ys. LIST_REL rel2 (MAP exp_of xs) ys ∧ LIST_REL rel1 ys (MAP exp_of zs)
@@ -256,7 +256,7 @@ Proof
   \\ PairCases_on ‘x’ \\ fs []
 QED
 
-Triviality cexp1_rel_eq: (* TODO: delete *)
+Theorem cexp1_rel_eq[local]: (* TODO: delete *)
   x = y ⇒ cexp1_rel x y
 Proof
   rw [] \\ fs []
@@ -476,7 +476,7 @@ Inductive cexp_rel:
 
 End
 
-Triviality NRC_refl:
+Theorem NRC_refl[local]:
   NRC cexp1_rel n x x
 Proof
   Induct_on ‘n’ \\ fs [NRC]
@@ -506,7 +506,7 @@ Proof
   \\ fs [LIST_REL_NRC_0,LIST_REL_NRC_SUC,NRC]
 QED
 
-Triviality NRC_Let:
+Theorem NRC_Let[local]:
   ∀k x x1 y y1.
     NRC cexp1_rel k x x1 ∧ NRC cexp1_rel k y y1 ⇒
     NRC cexp1_rel k (Let x_opt x y) (Let x_opt x1 y1)
@@ -516,7 +516,7 @@ Proof
   \\ rpt $ last_x_assum $ irule_at Any
 QED
 
-Triviality NRC_Handle:
+Theorem NRC_Handle[local]:
   ∀k x x1 y y1.
     NRC cexp1_rel k x x1 ∧ NRC cexp1_rel k y y1 ⇒
     NRC cexp1_rel k (Handle x n y) (Handle x1 n y1)
@@ -526,7 +526,7 @@ Proof
   \\ rpt $ last_x_assum $ irule_at Any
 QED
 
-Triviality NRC_HandleApp:
+Theorem NRC_HandleApp[local]:
   ∀k x x1 y y1.
     NRC cexp1_rel k x x1 ∧ NRC cexp1_rel k y y1 ⇒
     NRC cexp1_rel k (HandleApp x y) (HandleApp x1 y1)
@@ -536,7 +536,7 @@ Proof
   \\ rpt $ last_x_assum $ irule_at Any
 QED
 
-Triviality NRC_If:
+Theorem NRC_If[local]:
   ∀k x x1 y y1 z z1.
     NRC cexp1_rel k x x1 ∧ NRC cexp1_rel k y y1 ∧ NRC cexp1_rel k z z1 ⇒
     NRC cexp1_rel k (If x y z) (If x1 y1 z1)
@@ -546,7 +546,7 @@ Proof
   \\ rpt $ last_x_assum $ irule_at Any
 QED
 
-Triviality NRC_Lam:
+Theorem NRC_Lam[local]:
   ∀k z z1.
     NRC cexp1_rel k z z1 ⇒
     NRC cexp1_rel k (Lam y z) (Lam y z1)
@@ -556,7 +556,7 @@ Proof
   \\ rpt $ last_x_assum $ irule_at Any
 QED
 
-Triviality NRC_Raise:
+Theorem NRC_Raise[local]:
   ∀k z z1.
     NRC cexp1_rel k z z1 ⇒
     NRC cexp1_rel k (Raise z) (Raise z1)
@@ -566,7 +566,7 @@ Proof
   \\ rpt $ last_x_assum $ irule_at Any
 QED
 
-Triviality NRC_App:
+Theorem NRC_App[local]:
   ∀k xs ys.
     LIST_REL (NRC cexp1_rel k) xs ys ⇒
     NRC cexp1_rel k (App f xs) (App f ys)
@@ -578,7 +578,7 @@ Proof
   \\ irule cexp1_rel_App \\ fs []
 QED
 
-Triviality NRC_Letrec:
+Theorem NRC_Letrec[local]:
   ∀k xs ys x y.
     MAP FST xs = MAP FST ys ∧
     MAP (FST ∘ SND) xs = MAP (FST ∘ SND) ys ∧
@@ -607,7 +607,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality NRC_Case:
+Theorem NRC_Case[local]:
   ∀k x x1 xs xs1.
     OPTREL (λ(a,x) (b,x1). a = b ∧ NRC cexp1_rel k x x1) x x1 ∧
     MAP FST xs = MAP FST xs1 ∧
@@ -673,7 +673,7 @@ Proof
   \\ first_assum $ irule_at Any \\ fs [NRC_refl]
 QED
 
-Triviality NRC_REFL:
+Theorem NRC_REFL[local]:
   ∀n. R x x ⇒ NRC R n x x
 Proof
   Induct \\ fs [NRC] \\ metis_tac []
diff --git a/compiler/backend/passes/proofs/state_app_unit_1ProofScript.sml b/compiler/backend/passes/proofs/state_app_unit_1ProofScript.sml
index da30e406..ccac33a6 100644
--- a/compiler/backend/passes/proofs/state_app_unit_1ProofScript.sml
+++ b/compiler/backend/passes/proofs/state_app_unit_1ProofScript.sml
@@ -213,7 +213,7 @@ Proof
   \\ irule env_rel_cons \\ fs []
 QED
 
-Triviality FST_INTRO:
+Theorem FST_INTRO[local]:
   (λ(p1,p2). p1) = FST
 Proof
   fs [FUN_EQ_THM,FORALL_PROD]
@@ -446,7 +446,7 @@ Proof
   \\ simp [Once v_rel_cases]
 QED
 
-Triviality LIST_REL_MAP_MAP:
+Theorem LIST_REL_MAP_MAP[local]:
   ∀xs ys.
     LIST_REL R (MAP f xs) (MAP g ys) =
     LIST_REL (λx y. R (f x) (g y)) xs ys
diff --git a/compiler/backend/passes/proofs/state_app_unit_2ProofScript.sml b/compiler/backend/passes/proofs/state_app_unit_2ProofScript.sml
index 093a5db2..72eac682 100644
--- a/compiler/backend/passes/proofs/state_app_unit_2ProofScript.sml
+++ b/compiler/backend/passes/proofs/state_app_unit_2ProofScript.sml
@@ -232,7 +232,7 @@ Proof
   \\ irule env_rel_cons \\ fs []
 QED
 
-Triviality FST_INTRO:
+Theorem FST_INTRO[local]:
   (λ(p1,p2). p1) = FST
 Proof
   fs [FUN_EQ_THM,FORALL_PROD]
@@ -379,7 +379,7 @@ Proof
        \\ gvs []
        \\ Cases_on ‘n' < LENGTH l'’ \\ gvs []
        \\ gvs [Once v_rel_cases,LIST_REL_EL_EQN,state_rel_def])
-    \\ simp [Once v_rel_cases,LIST_REL_EL_EQN,state_rel_def]) 
+    \\ simp [Once v_rel_cases,LIST_REL_EL_EQN,state_rel_def])
   >~ [‘Update’] >-
    (gvs [application_def,step,step_res_rel_cases]
     \\ qpat_x_assum ‘v_rel x h’ mp_tac
@@ -492,7 +492,7 @@ Proof
   \\ rpt $ first_x_assum $ irule_at Any
 QED
 
-Triviality LIST_REL_MAP_MAP:
+Theorem LIST_REL_MAP_MAP[local]:
   ∀xs ys.
     LIST_REL R (MAP f xs) (MAP g ys) =
     LIST_REL (λx y. R (f x) (g y)) xs ys
diff --git a/compiler/backend/passes/proofs/state_caseProofScript.sml b/compiler/backend/passes/proofs/state_caseProofScript.sml
index b3c3fa76..7c9abf01 100644
--- a/compiler/backend/passes/proofs/state_caseProofScript.sml
+++ b/compiler/backend/passes/proofs/state_caseProofScript.sml
@@ -233,7 +233,7 @@ Proof
   rw [env_rel_def] \\ rw [] \\ fs [SUBSET_DEF]
 QED
 
-Triviality FST_INTRO:
+Theorem FST_INTRO[local]:
   (λ(p1,p2). p1) = FST
 Proof
   fs [FUN_EQ_THM,FORALL_PROD]
@@ -485,7 +485,7 @@ Proof
   \\ simp_tac std_ss [GSYM APPEND_ASSOC,APPEND]
 QED
 
-Triviality step_n_lets_for_lemma =
+Theorem step_n_lets_for_lemma[local] =
   step_n_lets_for |> Q.SPECL [‘xs’,‘[]’,‘0’] |> SIMP_RULE std_ss [LENGTH,APPEND]
 
 Theorem env_rel_zip:
diff --git a/compiler/backend/passes/proofs/state_namesProofScript.sml b/compiler/backend/passes/proofs/state_namesProofScript.sml
index b5fc07f4..62c9f2ff 100644
--- a/compiler/backend/passes/proofs/state_namesProofScript.sml
+++ b/compiler/backend/passes/proofs/state_namesProofScript.sml
@@ -11,7 +11,7 @@ Libs
   BasicProvers dep_rewrite
 
 
-Triviality LESS_EQ_list_max:
+Theorem LESS_EQ_list_max[local]:
   ∀xs n. n ≤ list_max xs ⇔ n = 0 ∨ ∃x. MEM x xs ∧ n ≤ x
 Proof
   Induct \\ fs [list_max_def]
@@ -54,7 +54,7 @@ Proof
     \\ metis_tac [LESS_EQ_REFL,PAIR])
 QED
 
-Triviality isStringThere_aux_lemma:
+Theorem isStringThere_aux_lemma[local]:
   ∀xs ts ys.
     LENGTH xs ≤ LENGTH ys ⇒
     (isStringThere_aux (strlit (ts ++ xs)) (strlit (ts ++ ys))
diff --git a/compiler/backend/passes/proofs/state_names_1ProofScript.sml b/compiler/backend/passes/proofs/state_names_1ProofScript.sml
index 9ca10e26..da8b46f4 100644
--- a/compiler/backend/passes/proofs/state_names_1ProofScript.sml
+++ b/compiler/backend/passes/proofs/state_names_1ProofScript.sml
@@ -233,7 +233,7 @@ Proof
   \\ fs [env_rel_def,SUBSET_DEF]
 QED
 
-Triviality FST_INTRO:
+Theorem FST_INTRO[local]:
   (λ(p1,p2). p1) = FST
 Proof
   fs [FUN_EQ_THM,FORALL_PROD]
@@ -497,7 +497,7 @@ Proof
   \\ simp [Once v_rel_cases]
 QED
 
-Triviality LIST_REL_MAP_MAP:
+Theorem LIST_REL_MAP_MAP[local]:
   ∀xs ys.
     LIST_REL R (MAP f xs) (MAP g ys) =
     LIST_REL (λx y. R (f x) (g y)) xs ys
diff --git a/compiler/backend/passes/proofs/state_to_cakeProofScript.sml b/compiler/backend/passes/proofs/state_to_cakeProofScript.sml
index 7ef6e2cf..053e6a25 100644
--- a/compiler/backend/passes/proofs/state_to_cakeProofScript.sml
+++ b/compiler/backend/passes/proofs/state_to_cakeProofScript.sml
@@ -146,7 +146,7 @@ Proof
   TOP_CASE_TAC >> gvs[estep_to_Edone] >> irule_at Any EQ_REFL
 QED
 
-Triviality dstep_ExpVal_Exp:
+Theorem dstep_ExpVal_Exp[local]:
   dstep benv st (ExpVal env (Exp e) k locs p) dk =
   case estep (env,st.refs,Exp e,k) of
   | Estep (env',refs',ev',ec') =>
@@ -834,7 +834,7 @@ Proof
   rw[FUN_EQ_THM, namespaceTheory.nsOptBind_def]
 QED
 
-Triviality cstep_Exn_over_list_to_cont:
+Theorem cstep_Exn_over_list_to_cont[local]:
   ∀es cenv cst cv cenv' env ck'.
   cstep_n (LENGTH es) (Estep (cenv,cst,Exn cv, (list_to_cont env es ++ ck'))) =
         (Estep (cenv,cst,Exn cv,ck'))
@@ -914,7 +914,7 @@ Proof
   rw[var_prefix_def]
 QED
 
-Triviality ALL_DISTINCT_pat_bindings[simp]:
+Theorem ALL_DISTINCT_pat_bindings[local,simp]:
   ALL_DISTINCT (REVERSE (MAP var_prefix vs) ++ [var_prefix v]) ⇔
   ¬MEM v vs ∧ ALL_DISTINCT vs
 Proof
@@ -947,7 +947,7 @@ Proof
   rw[store_lookup_def, store_assign_def, store_v_same_type_def]
 QED
 
-Triviality step_until_halt_no_err_step_n:
+Theorem step_until_halt_no_err_step_n[local]:
   step_until_halt s ≠ Err ⇒ ∀n st k. step_n n s ≠ error st k
 Proof
   PairCases_on `s` >> simp[step_until_halt_def] >>
@@ -957,7 +957,7 @@ Proof
   drule is_halt_imp_eq >> disch_then $ qspec_then `n` assume_tac >> gvs[error_def]
 QED
 
-Triviality ALL_DISTINCT_MAP_FSTs:
+Theorem ALL_DISTINCT_MAP_FSTs[local]:
   ALL_DISTINCT (MAP FST l) ⇒
   ALL_DISTINCT (MAP (λ(x,y,z). x) l)
 Proof
@@ -1709,7 +1709,7 @@ Proof
   simp[MAP_EQ_CONS] >> irule_at Any EQ_REFL
 QED
 
-Triviality implode_v_to_char_list_list_to_v:
+Theorem implode_v_to_char_list_list_to_v[local]:
   ∀il. implode (MAP Int il) =
   v_to_char_list (list_to_v (MAP (λi. Litv (Char (CHR (Num (i % 256))))) il))
 Proof
@@ -3310,7 +3310,7 @@ Proof
   Induct_on `condefs` >> rw[] >> pairarg_tac >> gvs[]
 QED
 
-Triviality build_constrs_MAP[simp]:
+Theorem build_constrs_MAP[local,simp]:
   build_constrs stamp (MAP (λ(cn,tys). cn, MAP f tys) cndefs) =
   build_constrs stamp cndefs
 Proof
@@ -3728,7 +3728,7 @@ QED
 
 (********** Key namespace result **********)
 
-Triviality namespace_ok_append_cn_imps:
+Theorem namespace_ok_append_cn_imps[local]:
   ∀ns ns'. namespace_ok (append_ns (ns0,ns1) (ns'0,ns'1)) ⇒
   (∀cn. MEM cn (MAP FST ns0) ∨ MEM cn (MAP FST $ FLAT $ MAP SND ns1) ⇒
     ¬ MEM cn (MAP FST ns'0) ∧
diff --git a/compiler/backend/passes/proofs/state_unthunkProofScript.sml b/compiler/backend/passes/proofs/state_unthunkProofScript.sml
index f77c8401..a1be0281 100644
--- a/compiler/backend/passes/proofs/state_unthunkProofScript.sml
+++ b/compiler/backend/passes/proofs/state_unthunkProofScript.sml
@@ -360,7 +360,7 @@ Definition pick_opt_def[simp]:
   pick_opt zs (SOME xs) = SOME xs
 End
 
-Triviality cont_rel_nil_cons:
+Theorem cont_rel_nil_cons[local]:
   ~(cont_rel p [] (y::ys)) ∧
   ~(cont_rel p (x::xs) [])
 Proof
@@ -592,7 +592,7 @@ Proof
   \\ fs [thunk_rel_def,dest_anyThunk_def]
 QED
 
-Triviality ALOOKUP_LIST_REL_loc_rel:
+Theorem ALOOKUP_LIST_REL_loc_rel[local]:
   ∀tfns locs x1 x2 x3 n y.
     LIST_REL (loc_rel x1 x2 x3) tfns locs ∧
     ALOOKUP locs n = SOME y ⇒
@@ -604,7 +604,7 @@ Proof
   \\ first_x_assum drule_all \\ fs []
 QED
 
-Triviality LIST_REL_loc_rel_alt_lemma:
+Theorem LIST_REL_loc_rel_alt_lemma[local]:
   ∀f locs f1.
     ALL_DISTINCT (MAP FST f) ∧
     LIST_REL (loc_rel p l (f1 ++ f)) (FILTER ((λx. is_Delay x) ∘ SND) f) locs ∧
@@ -635,10 +635,10 @@ Proof
   \\ last_x_assum $ irule_at Any \\ fs []
 QED
 
-Triviality LIST_REL_loc_rel_alt =
+Theorem LIST_REL_loc_rel_alt[local] =
   Q.SPECL [‘f’,‘locs’,‘[]’] LIST_REL_loc_rel_alt_lemma |> REWRITE_RULE [APPEND];
 
-Triviality LIST_REL_loc_rel:
+Theorem LIST_REL_loc_rel[local]:
   ALL_DISTINCT (MAP FST f) ∧
   LIST_REL (loc_rel p l f) (FILTER ((λx. is_Delay x) ∘ SND) f) locs ∧
   ALOOKUP locs s = SOME v2 ∧
@@ -711,7 +711,7 @@ Proof
   Induct \\ fs [LUPDATE_DEF] \\ rw [] \\ fs [LUPDATE_DEF]
 QED
 
-Triviality IMP_ALOOKUP_FILTER:
+Theorem IMP_ALOOKUP_FILTER[local]:
   ∀xs x y P.
     ALOOKUP xs x = SOME y ∧ P (x,y) ⇒
     ALOOKUP (FILTER P xs) x = SOME y
@@ -719,7 +719,7 @@ Proof
   Induct \\ fs [FORALL_PROD] \\ rw [] \\ gvs []
 QED
 
-Triviality ALOOKUP_LIST_REL:
+Theorem ALOOKUP_LIST_REL[local]:
   ∀tfns n x r sfns.
     ALOOKUP tfns n = SOME x ∧ ALL_DISTINCT (MAP FST sfns) ∧
     MAP FST tfns = MAP FST sfns ∧
@@ -731,7 +731,7 @@ Proof
   \\ Cases_on ‘sfns’ \\ gvs [] \\ PairCases_on ‘h’ \\ gvs []
 QED
 
-Triviality ALOOKUP_LIST_REL_loc_rel:
+Theorem ALOOKUP_LIST_REL_loc_rel[local]:
   ∀tfns locs x1 x2 x3 n x y.
     LIST_REL (loc_rel x1 x2 x3) tfns locs ∧
     ALOOKUP tfns n = SOME x ∧
@@ -997,14 +997,14 @@ Proof
   \\ gvs [ALOOKUP_NONE,EXTENSION]
 QED
 
-Triviality LIST_REL_loc_rel_MAP_FST:
+Theorem LIST_REL_loc_rel_MAP_FST[local]:
   ∀xs ys. LIST_REL (loc_rel p tenv tfns) xs ys ⇒ MAP FST xs = MAP FST ys
 Proof
   Induct \\ Cases_on ‘ys’ \\ fs [] \\ Cases \\ Cases_on ‘h’ \\ fs []
   \\ rw [] \\ fs []
 QED
 
-Triviality ALOOUKP_MAP_Rec:
+Theorem ALOOUKP_MAP_Rec[local]:
   ∀tfns n.
     ALOOKUP (MAP (λ(fn,x). (fn,Recclosure y tenv fn)) tfns) n = SOME tv ⇔
     MEM n (MAP FST tfns) ∧ tv = Recclosure y tenv n
@@ -1012,7 +1012,7 @@ Proof
   Induct \\ fs [FORALL_PROD] \\ rw [] \\ eq_tac \\ rw []
 QED
 
-Triviality LIST_REL_letrec_rel_Lam:
+Theorem LIST_REL_letrec_rel_Lam[local]:
   ∀tfns sfns.
     LIST_REL letrec_rel (MAP SND tfns) (MAP SND sfns) ∧
     MEM k (MAP FST (FILTER (λ(p1,p2). is_Lam p2) sfns)) ∧
@@ -1028,7 +1028,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality LIST_REL_letrec_rel_Delay:
+Theorem LIST_REL_letrec_rel_Delay[local]:
   ∀tfns sfns.
     LIST_REL letrec_rel (MAP SND tfns) (MAP SND sfns) ∧
     ~MEM k (MAP FST (FILTER (λ(p1,p2). is_Lam p2) sfns)) ∧
@@ -1043,7 +1043,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality ALL_DISTINCT_MAP_FILTER:
+Theorem ALL_DISTINCT_MAP_FILTER[local]:
   ∀xs. ALL_DISTINCT (MAP f xs) ⇒ ALL_DISTINCT (MAP f (FILTER p xs))
 Proof
   Induct \\ fs [] \\ rw []
@@ -1051,7 +1051,7 @@ Proof
   \\ gvs [MEM_MAP,MEM_FILTER]
 QED
 
-Triviality LIST_REL_loc_rel_Delay:
+Theorem LIST_REL_loc_rel_Delay[local]:
   ∀tfns locs.
     LIST_REL (loc_rel p tenv xx) (FILTER (λ(p1,p2). is_Delay p2) tfns) locs ∧
     MEM (k,Delay e) tfns ⇒
@@ -1445,7 +1445,7 @@ Proof
   \\ gvs [ALOOKUP_APPEND]
 QED
 
-Triviality step_n_unwind:
+Theorem step_n_unwind[local]:
   step_n (m+1) s = x ∧ n = m + 1 ⇒ step_n n s = x
 Proof
   rw []
@@ -1545,26 +1545,26 @@ Proof
   \\ rw [] \\ eq_tac \\ rw [] \\ fs []
 QED
 
-Triviality EVERY_LAM:
+Theorem EVERY_LAM[local]:
   ∀xs. EVERY (λ(n,x). f n) xs = EVERY f (MAP FST xs)
 Proof
   Induct \\ fs [FORALL_PROD]
 QED
 
-Triviality FST_INTRO:
+Theorem FST_INTRO[local]:
   (λ(p1,p2). p1) = FST
 Proof
   fs [FUN_EQ_THM,FORALL_PROD]
 QED
 
-Triviality LIST_REL_LIST_REL_lemma:
+Theorem LIST_REL_LIST_REL_lemma[local]:
   (∀x y. r1 x y ⇒ r2 x y) ∧ ys1 = ys2 ⇒
   LIST_REL r1 xs ys1 ⇒ LIST_REL r2 xs ys2
 Proof
   metis_tac [LIST_REL_mono]
 QED
 
-Triviality FILTER_ZIP_EQ:
+Theorem FILTER_ZIP_EQ[local]:
   ∀p ss xs ys.
     LENGTH p = LENGTH ss ∧ EVERY (λx. x ≠ NONE) xs ⇒
     FILTER (λx. FST x = NONE) (ZIP (p,ss)) =
@@ -1622,7 +1622,7 @@ Proof
   \\ fs []
 QED
 
-Triviality MAP_FST_make_let_env:
+Theorem MAP_FST_make_let_env[local]:
   ∀delays n env.
     MAP FST (make_let_env delays n env) =
     REVERSE (MAP FST delays) ++ MAP FST env
@@ -1667,7 +1667,7 @@ Proof
   \\ fs [FUN_EQ_THM]
 QED
 
-Triviality IMP_Lam:
+Theorem IMP_Lam[local]:
   ∀tfns sfns.
     MAP FST tfns = MAP FST sfns ∧ MEM (y,Lam v e) sfns ∧
     LIST_REL letrec_rel (MAP SND tfns) (MAP SND sfns) ⇒
@@ -1682,7 +1682,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality EXISTS_ALOOKUP_ALOOKUP:
+Theorem EXISTS_ALOOKUP_ALOOKUP[local]:
   ∀n xs ys.
     MEM n (MAP FST xs) ∧ ALL_DISTINCT (MAP FST ys) ∧ xs = REVERSE ys ⇒
     ∃v. ALOOKUP xs n = SOME v ∧ ALOOKUP ys n = SOME v
@@ -1934,7 +1934,7 @@ Proof
   \\ gvs []
 QED
 
-Triviality LIST_REL_lemma:
+Theorem LIST_REL_lemma[local]:
   ∀xs ys n. LIST_REL R xs ys ∧ ALOOKUP ys n = SOME y ⇒ ∃x. R x (n,y)
 Proof
   Induct_on ‘ys’ \\ gvs [PULL_EXISTS,FORALL_PROD,AllCaseEqs()]
@@ -1953,7 +1953,7 @@ Proof
   \\ gvs [loc_rel_def,dest_anyThunk_def]
 QED
 
-Triviality ALOOKUP_SND:
+Theorem ALOOKUP_SND[local]:
   ∀l f x y. ALOOKUP (FILTER (f o SND) l) x = SOME y ⇒ f y
 Proof
   Induct \\ rw [] \\ gvs []
diff --git a/compiler/backend/passes/proofs/thunk_Let_Delay_VarScript.sml b/compiler/backend/passes/proofs/thunk_Let_Delay_VarScript.sml
index a5bb0e06..e0c5a4be 100644
--- a/compiler/backend/passes/proofs/thunk_Let_Delay_VarScript.sml
+++ b/compiler/backend/passes/proofs/thunk_Let_Delay_VarScript.sml
@@ -1788,7 +1788,7 @@ Proof
       gvs [exp_size_def, boundvars_def])
 QED
 
-Triviality less_1_lemma[simp]:
+Theorem less_1_lemma[local,simp]:
   n < 1 ⇔ n = 0:num
 Proof
   fs []
@@ -1860,7 +1860,7 @@ Proof
       \\ drule_all ALOOKUP_ALL_DISTINCT_MEM \\ gvs []))
 QED
 
-Triviality exp_rel_result_map_Diverge:
+Theorem exp_rel_result_map_Diverge[local]:
   ∀xs ys k.
     LENGTH xs = LENGTH ys ∧
     (∀n. n < LENGTH ys ⇒ exp_rel (EL n xs) (EL n ys)) ∧
diff --git a/compiler/backend/passes/proofs/thunk_case_projProofScript.sml b/compiler/backend/passes/proofs/thunk_case_projProofScript.sml
index 7f866f8e..92f3df21 100644
--- a/compiler/backend/passes/proofs/thunk_case_projProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_case_projProofScript.sml
@@ -163,7 +163,7 @@ Theorem v_rel_def[simp] =
   |> map (SIMP_CONV (srw_ss ()) [Once v_rel_cases])
   |> LIST_CONJ;
 
-Triviality LIST_REL_IMP_MAP_FST_EQ:
+Theorem LIST_REL_IMP_MAP_FST_EQ[local]:
   ∀f g. LIST_REL P f g ∧ (∀x y. P x y ⇒ FST x = FST y) ⇒
         MAP FST f = MAP FST g
 Proof
diff --git a/compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml b/compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml
index d1ec073b..0a520b2a 100644
--- a/compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml
+++ b/compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml
@@ -504,7 +504,7 @@ Theorem v_rel_def =
   |> map (SIMP_CONV (srw_ss()) [Once combine_rel_cases])
   |> LIST_CONJ
 
-Triviality less_1_lemma[simp]:
+Theorem less_1_lemma[local,simp]:
   n < 1 ⇔ n = 0:num
 Proof
   fs []
diff --git a/compiler/backend/passes/proofs/thunk_let_forceProofScript.sml b/compiler/backend/passes/proofs/thunk_let_forceProofScript.sml
index bc7adaea..62730355 100644
--- a/compiler/backend/passes/proofs/thunk_let_forceProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_let_forceProofScript.sml
@@ -167,7 +167,7 @@ Theorem v_rel_def[simp] =
   |> map (SIMP_CONV (srw_ss()) [Once v_rel_cases])
   |> LIST_CONJ;
 
-Triviality LIST_REL_IMP_MAP_FST_EQ:
+Theorem LIST_REL_IMP_MAP_FST_EQ[local]:
   ∀f g. LIST_REL P f g ∧ (∀x y. P x y ⇒ FST x = FST y) ⇒
         MAP FST f = MAP FST g
 Proof
@@ -238,13 +238,13 @@ Definition subst_acc_def:
                | SOME w => (SOME (Val w,y))
 End
 
-Triviality MAP_FST_FILTER_NEQ:
+Theorem MAP_FST_FILTER_NEQ[local]:
   ∀vs. MAP FST (FILTER (λ(n,x). n ≠ w) vs) = FILTER (λx. x ≠ w) (MAP FST vs)
 Proof
   Induct \\ fs [FORALL_PROD] \\ rw []
 QED
 
-Triviality LIST_REL_MAP_SND_FILTER:
+Theorem LIST_REL_MAP_SND_FILTER[local]:
   ∀vs ws.
     LIST_REL P (MAP SND vs) (MAP SND ws) ∧ MAP FST vs = MAP FST ws ⇒
     LIST_REL P (MAP SND (FILTER (λ(n,x). n ≠ w) vs))
@@ -257,7 +257,7 @@ Proof
   \\ rw [] \\ gvs [UNCURRY]
 QED
 
-Triviality LIST_REL_FILTER_ALT:
+Theorem LIST_REL_FILTER_ALT[local]:
   ∀vs ws g.
     LIST_REL P vs ws ∧ MAP FST vs = MAP FST ws ∧
     (∀x y z. g (x,y) = g (x,z)) ⇒
@@ -271,7 +271,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality ALOOKUP_MEM_MAP_FST:
+Theorem ALOOKUP_MEM_MAP_FST[local]:
   ∀xs v x. ALOOKUP xs v = SOME x ⇒ MEM v (MAP FST xs)
 Proof
   Induct \\ fs [FORALL_PROD] \\ rw []
@@ -356,7 +356,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality exp_rel_imp_opt:
+Theorem exp_rel_imp_opt[local]:
   (m1 ≠ NONE ⇒ m2 = m1) ⇒
   exp_rel m1 x y ⇒ exp_rel m2 x y
 Proof
@@ -366,7 +366,7 @@ Proof
   \\ fs []
 QED
 
-Triviality FST_INTRO:
+Theorem FST_INTRO[local]:
   (λ(x,y). x) = FST
 Proof
   fs [FUN_EQ_THM,FORALL_PROD]
@@ -674,7 +674,7 @@ Proof
   \\ fs [freevars_subst]
 QED
 
-Triviality IMP_closed_subst_Rec:
+Theorem IMP_closed_subst_Rec[local]:
   LIST_REL
      (λ(fn,x) (gn,y).
        fn = gn ∧ exp_rel NONE x y ∧ freevars x ⊆ set (MAP FST xs)) xs ys ∧
@@ -2127,7 +2127,7 @@ Definition rel_list_def[simp]:
   rel_list (m::ms) x y = ∃z. exp_rel m x z ∧ rel_list ms z y
 End
 
-Triviality rel_list_append:
+Theorem rel_list_append[local]:
   ∀xs ys x y.
     rel_list (xs ++ ys) x y ⇔ ∃q. rel_list xs x q ∧ rel_list ys q y
 Proof
diff --git a/compiler/backend/passes/proofs/thunk_let_force_1ProofScript.sml b/compiler/backend/passes/proofs/thunk_let_force_1ProofScript.sml
index 96c4fe87..411466b9 100644
--- a/compiler/backend/passes/proofs/thunk_let_force_1ProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_let_force_1ProofScript.sml
@@ -27,7 +27,7 @@ Definition dest_Var_def[simp]:
   dest_Var (Var n:lhs) = n
 End
 
-Triviality MAP_filter_clash_NONE:
+Theorem MAP_filter_clash_NONE[local]:
   ∀m. MAP (filter_clash NONE) m = m
 Proof
   Induct \\ fs [filter_clash_def,name_clash_def]
@@ -326,7 +326,7 @@ Proof
   \\ drule_all e_rel_semantics \\ fs []
 QED
 
-Triviality let_force_Delay:
+Theorem let_force_Delay[local]:
   let_force m e = Delay e' ⇒ ∃e0. e = Delay e0
 Proof
   simp[Once $ DefnBase.one_line_ify NONE let_force_def] >>
diff --git a/compiler/backend/passes/proofs/thunk_to_envProofScript.sml b/compiler/backend/passes/proofs/thunk_to_envProofScript.sml
index 1c46a338..6199e03f 100644
--- a/compiler/backend/passes/proofs/thunk_to_envProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_to_envProofScript.sml
@@ -11,7 +11,7 @@ Libs
   term_tactic monadsyntax
 
 
-Triviality exp_rel_Disj:
+Theorem exp_rel_Disj[local]:
   ∀xs x. exp_rel [] (Disj x xs) (Disj x xs)
 Proof
   Induct \\ fs [Disj_def,FORALL_PROD,envLangTheory.Disj_def] \\ rw []
@@ -20,7 +20,7 @@ Proof
   \\ rpt (irule_at Any exp_rel_Var \\ fs [])
 QED
 
-Triviality op_of_op_to_env[simp]:
+Theorem op_of_op_to_env[local,simp]:
   op_of (op_to_env op) = op_of op
 Proof
   Cases_on `op` >> rw[op_to_env_def, op_of_def]
diff --git a/compiler/backend/passes/proofs/thunk_to_env_1ProofScript.sml b/compiler/backend/passes/proofs/thunk_to_env_1ProofScript.sml
index 8e953de3..509b39ad 100644
--- a/compiler/backend/passes/proofs/thunk_to_env_1ProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_to_env_1ProofScript.sml
@@ -693,7 +693,7 @@ Definition next_rel_def[simp]:
   next_rel (_: (string # string) thunk_semantics$next_res) _ = F
 End
 
-Triviality LIST_REL_ALOOKUP_lemma:
+Theorem LIST_REL_ALOOKUP_lemma[local]:
   ∀f g s.
     LIST_REL (λ(fn,b) (gn,c). fn = gn ∧ exp_rel xs b c) f g ⇒
     ALOOKUP f s = NONE ∧ ALOOKUP g s = NONE ∨
@@ -775,7 +775,7 @@ Proof
   \\ fs [LIST_REL_EL_EQN,MEM_MAP,FORALL_PROD]
 QED
 
-Triviality v_rel_RetVal[simp]:
+Theorem v_rel_RetVal[local,simp]:
   v_rel (Monadic Ret [Lit a]) (RetVal (Atom a))
 Proof
   simp [Once v_rel_cases]
diff --git a/compiler/backend/passes/proofs/thunk_undelay_nextProofScript.sml b/compiler/backend/passes/proofs/thunk_undelay_nextProofScript.sml
index 6d0f107d..766801ff 100644
--- a/compiler/backend/passes/proofs/thunk_undelay_nextProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_undelay_nextProofScript.sml
@@ -751,7 +751,7 @@ Proof
   \\ rgs [Once exp_rel_cases]
 QED
 
-Triviality exp_rel_subst_LIST_REL:
+Theorem exp_rel_subst_LIST_REL[local]:
   exp_rel q q' ∧
   LIST_REL (λ(s,v) (s',v'). s = s' ∧ v_rel v v') r r' ⇒
     ($= +++ v_rel) (eval (subst r q)) (eval (subst r' q'))
@@ -764,7 +764,7 @@ Proof
   \\ rpt (pairarg_tac \\ gvs [])
 QED
 
-Triviality thunk_exists[simp,local]:
+Theorem thunk_exists[simp,local]:
   ∃k. is_anyThunk k
 Proof
   qrefine `Thunk _` \\ simp [is_anyThunk_def, dest_anyThunk_def]
@@ -1264,7 +1264,7 @@ Proof
   \\ Cases_on `next_delayed x v c s` \\ Cases_on `next (ck + x) w d t` \\ gvs []
 QED
 
-Triviality interp_action_return:
+Theorem interp_action_return[local]:
   interp (INR (Monadic Ret [Lit (Str y)]))
     (BC (Lam "v" (Monad Ret [Delay (Var "v")])) cont) st =
   interp (INR (Monadic Ret [Delay $ Value $ Atom $ Str y])) cont st
diff --git a/compiler/backend/passes/proofs/thunk_unthunkProofScript.sml b/compiler/backend/passes/proofs/thunk_unthunkProofScript.sml
index 093c2d39..cf24f327 100644
--- a/compiler/backend/passes/proofs/thunk_unthunkProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_unthunkProofScript.sml
@@ -435,7 +435,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality ALOOKUP_REVERSE_lemma:
+Theorem ALOOKUP_REVERSE_lemma[local]:
   ∀vs ws.
     LIST_REL v_rel (MAP SND vs) (MAP SND ws) ∧
     MAP FST vs = MAP FST ws ⇒
@@ -1195,7 +1195,7 @@ QED
 Overload v_inv_rel = ``λv w. v_inv v ∧ v_rel v w``
 Overload exp_inv_rel = ``λx y. exp_inv x ∧ closed x ∧ exp_rel x y``
 
-Triviality exp_inv_rel_eval:
+Theorem exp_inv_rel_eval[local]:
   exp_inv_rel x y ==>
     ($= +++ v_inv_rel) (eval x) (eval y)
 Proof
@@ -1203,7 +1203,7 @@ Proof
   Cases_on `eval x` >> Cases_on `eval y` >> gvs[]
 QED
 
-Triviality exp_inv_rel_subst:
+Theorem exp_inv_rel_subst[local]:
   ∀vs x ws y.
     LIST_REL v_inv_rel (MAP SND vs) (MAP SND ws) ∧
     MAP FST vs = MAP FST ws ∧
diff --git a/compiler/backend/passes/proofs/thunk_untickProofScript.sml b/compiler/backend/passes/proofs/thunk_untickProofScript.sml
index 8b68504a..eac7b11f 100644
--- a/compiler/backend/passes/proofs/thunk_untickProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_untickProofScript.sml
@@ -173,7 +173,7 @@ Proof
   Cases \\ rw [ok_bind_def] \\ gs [subst_def]
 QED
 
-Triviality LIST_REL_IMP_MAP_FST_EQ:
+Theorem LIST_REL_IMP_MAP_FST_EQ[local]:
   ∀f g. LIST_REL P f g ∧ (∀x y. P x y ⇒ FST x = FST y) ⇒
         MAP FST f = MAP FST g
 Proof
@@ -413,7 +413,7 @@ Proof
   \\ Cases_on `EL n'' f` \\ gvs []
 QED
 
-Triviality exp_rel_result_map_Diverge:
+Theorem exp_rel_result_map_Diverge[local]:
   ∀xs ys k.
     LENGTH xs = LENGTH ys ∧
     (∀n. n < LENGTH ys ⇒ exp_rel (EL n xs) (EL n ys)) ∧
diff --git a/compiler/backend/passes/pure_inline_cexpScript.sml b/compiler/backend/passes/pure_inline_cexpScript.sml
index a5320af5..a9688b74 100644
--- a/compiler/backend/passes/pure_inline_cexpScript.sml
+++ b/compiler/backend/passes/pure_inline_cexpScript.sml
@@ -14,7 +14,7 @@ Libs
 (* heuristic for deciding when to inline *)
 Type heuristic = “:'a cexp -> bool”
 
-Triviality cexp_size_lemma:
+Theorem cexp_size_lemma[local]:
   ∀vbs.
     list_size (cexp_size (K 0)) (MAP SND vbs) ≤
     list_size (pair_size mlstring_size (cexp_size (K 0))) vbs
@@ -54,7 +54,7 @@ Definition heuristic_insert_Rec_def:
       | _ => m
 End
 
-Triviality size_lemma:
+Theorem size_lemma[local]:
   ∀bs.
     list_size (λx. cexp_size (K 0) (SND (SND x))) bs ≤
     list_size (pair_size mlstring_size
@@ -167,7 +167,7 @@ Definition inline_all_def:
     in dead_let inlined_e
 End
 
-Triviality cexp_size_lemma2:
+Theorem cexp_size_lemma2[local]:
   ∀xs e.
     MEM e xs ⇒
     cexp_size (K 0) e ≤ list_size (cexp_size (K 0)) xs
diff --git a/compiler/backend/passes/pure_letrec_spec_cexpScript.sml b/compiler/backend/passes/pure_letrec_spec_cexpScript.sml
index 04d16f4e..a211a780 100644
--- a/compiler/backend/passes/pure_letrec_spec_cexpScript.sml
+++ b/compiler/backend/passes/pure_letrec_spec_cexpScript.sml
@@ -22,7 +22,7 @@ Definition min_call_args_def:
     else NONE::(min_call_args xs ys)
 End
 
-Triviality const_call_args_lemma:
+Theorem const_call_args_lemma[local]:
   ∀bs.
     list_size (λx. cexp_size (K 1) (SND (SND x))) bs
     ≤
diff --git a/compiler/backend/passes/state_app_unitScript.sml b/compiler/backend/passes/state_app_unitScript.sml
index fcc24590..4e5337fd 100644
--- a/compiler/backend/passes/state_app_unitScript.sml
+++ b/compiler/backend/passes/state_app_unitScript.sml
@@ -53,7 +53,7 @@ Termination
   \\ gvs [LENGTH_EQ_NUM_compute,PULL_EXISTS,list_size_def,any_el_def]
 End
 
-Triviality push_app_unit_test:
+Theorem push_app_unit_test[local]:
   push_app_unit 0 (App AppOp [Let NONE (Var w) (Lam NONE (Var v)); Unit]) =
   Let NONE (Var w) (Var v)
 Proof
diff --git a/compiler/backend/passes/state_namesScript.sml b/compiler/backend/passes/state_namesScript.sml
index eb6914a2..1148c63e 100644
--- a/compiler/backend/passes/state_namesScript.sml
+++ b/compiler/backend/passes/state_namesScript.sml
@@ -19,7 +19,7 @@ Definition max_name_def:
     else 0
 End
 
-Triviality max_name_test:
+Theorem max_name_test[local]:
   max_name (strlit "hello") = 0 ∧
   max_name (strlit "ignore") = 1 ∧
   max_name (strlit "ignore'") = 2
diff --git a/compiler/binary/pure_backendProgScript.sml b/compiler/binary/pure_backendProgScript.sml
index becfdeab..928aa74b 100644
--- a/compiler/binary/pure_backendProgScript.sml
+++ b/compiler/binary/pure_backendProgScript.sml
@@ -33,7 +33,7 @@ val r = translate var_setTheory.empty_vars_def;
 
 val res = translate_no_ind pure_namesTheory.extract_names_def;
 
-Triviality extract_names_ind:
+Theorem extract_names_ind[local]:
   extract_names_ind (:α)
 Proof
   once_rewrite_tac [fetch "-" "extract_names_ind_def"]
@@ -74,7 +74,7 @@ val r = translate delay_arg_def;
 val r = translate monad_to_thunk_def;
 val r = translate_no_ind pure_to_thunkTheory.to_thunk_def;
 
-Triviality to_thunk_ind:
+Theorem to_thunk_ind[local]:
   to_thunk_ind (:'a)
 Proof
   once_rewrite_tac [fetch "-" "to_thunk_ind_def"]
diff --git a/compiler/binary/pure_frontendProgScript.sml b/compiler/binary/pure_frontendProgScript.sml
index 14189384..674f66f6 100644
--- a/compiler/binary/pure_frontendProgScript.sml
+++ b/compiler/binary/pure_frontendProgScript.sml
@@ -128,7 +128,7 @@ val r = translate App_Lam_to_Lets_def;
 
 val r = translate_no_ind inline_def;
 
-Triviality inline_ind:
+Theorem inline_ind[local]:
   inline_ind (:'a)
 Proof
   once_rewrite_tac[fetch "-" "inline_ind_def"] >>
diff --git a/compiler/binary/pure_inferProgScript.sml b/compiler/binary/pure_inferProgScript.sml
index 1ac13f5b..1a5e1633 100644
--- a/compiler/binary/pure_inferProgScript.sml
+++ b/compiler/binary/pure_inferProgScript.sml
@@ -144,13 +144,13 @@ val _ = (length (hyp r) = 0) orelse fail (); (* no side conditions *)
 
 val _ = add_preferred_thy "-";
 
-Triviality PRECONDITION_INTRO:
+Theorem PRECONDITION_INTRO[local]:
   (b ==> (x = y)) ==> (x = if PRECONDITION b then y else x)
 Proof
   Cases_on `b` \\ SIMP_TAC std_ss [PRECONDITION_def]
 QED
 
-Triviality EXISTS_eq:
+Theorem EXISTS_eq[local]:
   ∀xs. EXISTS P xs ⇔ MEMBER T (MAP P xs)
 Proof
   fs [GSYM MEMBER_INTRO]
@@ -229,7 +229,7 @@ val r = translate
   |> SPEC_ALL
   |> MATCH_MP PRECONDITION_INTRO)
 
-Triviality pure_oc_side:
+Theorem pure_oc_side[local]:
   pure_oc_side s t v = pure_wfs s
 Proof
   reverse $ Cases_on ‘pure_wfs s’ \\ simp []
@@ -248,7 +248,7 @@ val _ = pure_oc_side |> update_precondition;
 
 val r = translate pure_unificationTheory.pure_ext_s_check;
 
-Triviality pure_ext_s_check_side:
+Theorem pure_ext_s_check_side[local]:
   pure_ext_s_check_side s t v = pure_wfs s
 Proof
   rewrite_tac [fetch "-" "pure_ext_s_check_side_def"]
@@ -256,7 +256,7 @@ QED
 
 val _ = pure_ext_s_check_side |> update_precondition;
 
-Triviality pure_unify_lemma:
+Theorem pure_unify_lemma[local]:
   (pure_unify s t1 t2 =
      if PRECONDITION (pure_wfs s) then
       (case (pure_walk s t1,pure_walk s t2) of
@@ -312,7 +312,7 @@ QED
 
 val r = translate_no_ind pure_unify_lemma;
 
-Triviality pure_unify_ind:
+Theorem pure_unify_ind[local]:
   pure_unify_ind
 Proof
   rewrite_tac [fetch "-" "pure_unify_ind_def"]
@@ -335,7 +335,7 @@ val _ = pure_unify_ind |> update_precondition;
 val pure_unify_ind_lemma =
   pure_unify_ind |> REWRITE_RULE [fetch "-" "pure_unify_ind_def"];
 
-Triviality pure_unify_side:
+Theorem pure_unify_side[local]:
   (∀s t1 t2. pure_unify_side s t1 t2 ⇔ pure_wfs s) ∧
   (∀s ts1 ts2. pure_unifyl_side s ts1 ts2 ⇔ pure_wfs s)
 Proof
@@ -378,7 +378,7 @@ Proof
   \\ simp []
 QED
 
-Triviality pure_walkstar_eta:
+Theorem pure_walkstar_eta[local]:
   MAP (pure_walkstar s) = MAP $ λx. pure_walkstar s x
 Proof
   AP_TERM_TAC \\ fs [FUN_EQ_THM]
@@ -429,7 +429,7 @@ QED
 
 val _ = subst_constraint_side |> update_precondition;
 
-Triviality infer_bind:
+Theorem infer_bind[local]:
   infer_bind (g : ('a,'e) inferM) f = λs.
     case g s of
     | Err e => Err e
@@ -465,7 +465,7 @@ val r = translate pure_inferenceTheory.infer_top_level_def;
 
 val r = translate pure_typingTheory.freetyvars_ok_def;
 
-Triviality type_wf_eq:
+Theorem type_wf_eq[local]:
   type_wf typedefs v ⇔
      case v of
        TypeVar n => T
@@ -493,7 +493,7 @@ Definition every_pair_def:
   (every_pair P ((x,y)::xs) ⇔ P x y ∧ every_pair P xs)
 End
 
-Triviality intro_every_pair:
+Theorem intro_every_pair[local]:
   EVERY P xs ⇔ every_pair (λx y. P (x,y)) xs
 Proof
   Induct_on ‘xs’ \\ fs [FORALL_PROD,every_pair_def]
diff --git a/compiler/binary/pure_parseProgScript.sml b/compiler/binary/pure_parseProgScript.sml
index 08fde859..7b7de5eb 100644
--- a/compiler/binary/pure_parseProgScript.sml
+++ b/compiler/binary/pure_parseProgScript.sml
@@ -109,7 +109,7 @@ val el_side = Q.prove(`
   Induct_on ‘x’ \\ Cases_on ‘l’ \\ simp [Once (fetch"-""el_side_def")])
   |> update_precondition;
 
-Triviality and_to_if:
+Theorem and_to_if[local]:
   (xs ≠ [] ∧ c ⇔ if xs = [] then F else c) ∧
   ((b ⇒ c) ⇔ if b then c else T)
 Proof
@@ -119,7 +119,7 @@ QED
 
 val r = translate (pure_lexer_implTheory.next_sym_alt_def |> RW [and_to_if]);
 
-Triviality read_while_thm':
+Theorem read_while_thm'[local]:
   ∀cs s cs' s'. read_while P cs s = (s', cs') ⇒ STRLEN s' ≥ STRLEN s
 Proof
   Induct >> rw[] >>
@@ -151,7 +151,7 @@ val r = translate purePEGTheory.purePEG_def;
 
 val r = translate (def_of_const ``validAddSym``);
 
-Triviality validaddsym_side_lemma:
+Theorem validaddsym_side_lemma[local]:
   ∀x. validaddsym_side x = T
 Proof
   simp[fetch "-" "validaddsym_side_def"]
@@ -231,7 +231,7 @@ val r = translate (def_of_const “cst_to_ast$mkFunTy”);
 
 val r = translate_no_ind (def_of_const “cst_to_ast$astType”);
 
-Triviality asttype_ind:
+Theorem asttype_ind[local]:
   asttype_ind (:'a)
 Proof
   once_rewrite_tac [fetch "-" "asttype_ind_def"]
@@ -250,7 +250,7 @@ val _ = asttype_ind |> update_precondition;
 
 val res = translate_no_ind cst_to_astTheory.optLAST_def;
 
-Triviality optlast_ind:
+Theorem optlast_ind[local]:
   optlast_ind (:α) (:γ) (:β)
 Proof
   once_rewrite_tac [fetch "-" "optlast_ind_def"]
@@ -283,7 +283,7 @@ val r = translate (def_of_const “cst_to_ast$tok_action”);
 
 val r = translate cst_to_astTheory.handlePrecs_def;
 
-Triviality OPT_MMAP_eq:
+Theorem OPT_MMAP_eq[local]:
   ∀xs f. OPT_MMAP f xs = OPT_MMAP I (MAP f xs)
 Proof
   Induct \\ fs [OPT_MMAP_def]
@@ -303,7 +303,7 @@ val r = translate_no_ind
   (def_of_const “cst_to_ast$astExp”
    |> ONCE_REWRITE_RULE [OPT_MMAP_eq]);
 
-Triviality astexp_ind:
+Theorem astexp_ind[local]:
   astexp_ind (:'a)
 Proof
   once_rewrite_tac [fetch "-" "astexp_ind_def"]
@@ -330,7 +330,7 @@ val r = translate_no_ind
   (def_of_const “ast_to_cexp$translate_type”
    |> ONCE_REWRITE_RULE [OPT_MMAP_eq]);
 
-Triviality translate_type_ind:
+Theorem translate_type_ind[local]:
   translate_type_ind
 Proof
   once_rewrite_tac [fetch "-" "translate_type_ind_def"]
@@ -344,7 +344,7 @@ QED
 
 val _ = translate_type_ind |> update_precondition;
 
-Triviality translate_type_side:
+Theorem translate_type_side[local]:
   ∀x y z. translate_type_side x y z
 Proof
   ho_match_mp_tac (latest_ind ())
@@ -355,7 +355,7 @@ QED
 
 val _ = translate_type_side |> update_precondition;
 
-Triviality FRONT_alt_def:
+Theorem FRONT_alt_def[local]:
   FRONT (h::t) = if NULL t then [] else h::FRONT t
 Proof
   rw[FRONT_DEF] >> gvs[] >> Cases_on `t` >> gvs[]
diff --git a/compiler/parsing/ast_to_cexpScript.sml b/compiler/parsing/ast_to_cexpScript.sml
index f173898a..7ae36f02 100644
--- a/compiler/parsing/ast_to_cexpScript.sml
+++ b/compiler/parsing/ast_to_cexpScript.sml
@@ -674,13 +674,13 @@ Definition monad_cn_mlstrings_def:
     [«Ret»;«Bind»;«Raise»;«Handle»;«Alloc»;«Length»;«Deref»;«Update»;«Act»]
 End
 
-Triviality implodeEQ:
+Theorem implodeEQ[local]:
   y = implode x ⇔ (explode y = x)
 Proof
   rw[EQ_IMP_THM] >> simp[]
 QED
 
-Triviality MEM_monad_cn_mlstrings:
+Theorem MEM_monad_cn_mlstrings[local]:
   MEM x monad_cn_mlstrings ⇔ explode x ∈ monad_cns
 Proof
   rw[monad_cn_mlstrings_def, pure_configTheory.monad_cns_def] >>
diff --git a/compiler/parsing/pure_lexer_implScript.sml b/compiler/parsing/pure_lexer_implScript.sml
index e7e340b6..1a9b7310 100644
--- a/compiler/parsing/pure_lexer_implScript.sml
+++ b/compiler/parsing/pure_lexer_implScript.sml
@@ -293,14 +293,14 @@ Termination
       gs[])
 End
 
-Triviality EVERY_isDigit_imp:
+Theorem EVERY_isDigit_imp[local]:
   EVERY isDigit x ⇒ MAP UNHEX x = MAP unhex_alt x
 Proof
   rw[]>>match_mp_tac LIST_EQ>>
   fs[EL_MAP,EVERY_EL,unhex_alt_def,isDigit_def,isHexDigit_def]
 QED
 
-Triviality toNum_rw:
+Theorem toNum_rw[local]:
   ∀x. EVERY isDigit x ⇒ toNum x = num_from_dec_string_alt x
 Proof
   rw[ASCIInumbersTheory.s2n_def,ASCIInumbersTheory.num_from_dec_string_def,
@@ -310,13 +310,13 @@ Proof
   metis_tac[rich_listTheory.EVERY_REVERSE]
 QED
 
-Triviality EVERY_isHexDigit_imp:
+Theorem EVERY_isHexDigit_imp[local]:
   EVERY isHexDigit x ⇒ MAP UNHEX x = MAP unhex_alt x
 Proof
   rw[]>>match_mp_tac LIST_EQ>>fs[EL_MAP,EVERY_EL,unhex_alt_def]
 QED
 
-Triviality num_from_hex_string_rw:
+Theorem num_from_hex_string_rw[local]:
   ∀x. EVERY isHexDigit x ⇒ num_from_hex_string x = num_from_hex_string_alt x
 Proof
   rw[ASCIInumbersTheory.s2n_def,ASCIInumbersTheory.num_from_hex_string_def,
@@ -326,12 +326,12 @@ Proof
   metis_tac[rich_listTheory.EVERY_REVERSE]
 QED
 
-Triviality EVERY_IMPLODE:
+Theorem EVERY_IMPLODE[local]:
   ∀ls P. EVERY P (IMPLODE ls) ⇔ EVERY P ls
 Proof Induct>>fs[]
 QED
 
-Triviality read_while_P_lem:
+Theorem read_while_P_lem[local]:
   ∀ ls rest P x y.
     EVERY P rest ∧ read_while P ls rest = (x,y) ⇒ EVERY P x
 Proof
diff --git a/compiler/parsing/sexp/pure_printScript.sml b/compiler/parsing/sexp/pure_printScript.sml
index ca7783b8..6327d0aa 100644
--- a/compiler/parsing/sexp/pure_printScript.sml
+++ b/compiler/parsing/sexp/pure_printScript.sml
@@ -71,21 +71,21 @@ Definition str_of_def:
   str_of x = vs2str [sexp_of x] []
 End
 
-Triviality str_of_test1:
+Theorem str_of_test1[local]:
   str_of (Lam () [«x»;«y»] (Prim () (AtomOp Add) [Var () «x»; Var () «y»])) =
     "\n(lam (x y) (+ x y))\n\n"
 Proof
   EVAL_TAC
 QED
 
-Triviality str_of_test2:
+Theorem str_of_test2[local]:
   str_of (Letrec () [(«x»,(Prim () (AtomOp Add) [Var () «x»; Var () «y»]))]
            (Var () «y»)) = "\n(letrec (x (+ x y)) y)\n\n"
 Proof
   EVAL_TAC
 QED
 
-Triviality str_of_test3:
+Theorem str_of_test3[local]:
   str_of (Case () (App () (Var () «f») [Prim () (AtomOp (Lit (Int 7))) []]) «xs»
             [(«nil»,[],Var () «xs»);
              («cons»,[«y»;«ys»],Var () «ys»)] NONE) =
@@ -227,14 +227,14 @@ Definition parse_prog_def:
       Letrec () values main
 End
 
-Triviality parse_cexp_test1:
+Theorem parse_cexp_test1[local]:
   parse_cexp "(+ a b)" =
     Prim () (AtomOp Add) [Var () «a»; Var () «b»]
 Proof
   EVAL_TAC
 QED
 
-Triviality parse_cexp_test2:
+Theorem parse_cexp_test2[local]:
   parse_cexp "(let a (int 6) (+ a b))" =
      Let () «a» (Prim () (AtomOp (Lit (Int 6))) [])
        (Prim () (AtomOp Add) [Var () «a»; Var () «b»])
diff --git a/compiler/proofs/pure_compilerProofScript.sml b/compiler/proofs/pure_compilerProofScript.sml
index 4e442058..e80d838b 100644
--- a/compiler/proofs/pure_compilerProofScript.sml
+++ b/compiler/proofs/pure_compilerProofScript.sml
@@ -82,13 +82,13 @@ Proof
   drule well_typed_program_imps >> gvs[pure_tcexp_lemmasTheory.cexp_wf_tcexp_wf]
 QED
 
-Triviality PAIR_ID:
+Theorem PAIR_ID[local]:
   (λ(p1,p2). (p1,p2)) = I
 Proof
   simp[FUN_EQ_THM] >> PairCases >> simp[]
 QED
 
-Triviality exp_eq_itree_eq:
+Theorem exp_eq_itree_eq[local]:
   e1 ≅ e2 ∧ closed e1 ∧ closed e2 ⇒ itree_of e1 = itree_of e2
 Proof
   rw[] >> dxrule_all $ iffRL pure_exp_relTheory.app_bisimilarity_eq >> strip_tac >>
diff --git a/language/pure_valueScript.sml b/language/pure_valueScript.sml
index b639522f..ef972910 100644
--- a/language/pure_valueScript.sml
+++ b/language/pure_valueScript.sml
@@ -198,7 +198,7 @@ Theorem v_11 = LIST_CONJ [Atom_11, Closure_11, Constructor_11];
  * Prove distinctness for constructors.
  *)
 
-Triviality v_distinct_lemma:
+Theorem v_distinct_lemma[local]:
   ALL_DISTINCT [Atom b; Closure n x; Constructor s t; Error; Diverge]
 Proof
   rw [Atom_def, Closure_def, Constructor_def, Error_def, Diverge_def]
@@ -581,7 +581,7 @@ Definition make_v_rep_def:
       | (Error', _) => (Error', SOME 0))
 End
 
-Triviality v_rep_ok_make_v_rep:
+Theorem v_rep_ok_make_v_rep[local]:
   ∀f. v_rep_ok (make_v_rep f)
 Proof
   rw[v_rep_ok_def, subtrees_def, make_v_rep_def] >>
diff --git a/meta-theory/pure_alpha_equivScript.sml b/meta-theory/pure_alpha_equivScript.sml
index 5d6f29f2..f18c5d3a 100644
--- a/meta-theory/pure_alpha_equivScript.sml
+++ b/meta-theory/pure_alpha_equivScript.sml
@@ -491,7 +491,7 @@ Proof
   rw[MAP_EQ_f] >> PairCases_on `e` >> fs[]
 QED
 
-Triviality subst_funs_eqvt_alt:
+Theorem subst_funs_eqvt_alt[local]:
   ∀ v1 v2 fns e.
     perm_exp v1 v2 (subst_funs fns e) =
     subst_funs (MAP (λ(n,x). (perm1 v1 v2 n, perm_exp v1 v2 x)) fns) (perm_exp v1 v2 e)
@@ -513,7 +513,7 @@ Proof
   ho_match_mp_tac perm_wh_ind \\ rw [perm_wh_def]
 QED
 
-Triviality get_atoms_perm_cancel:
+Theorem get_atoms_perm_cancel[local]:
   ∀v1 v2 l.
     get_atoms (MAP (perm_wh v1 v2) l) = get_atoms l
 Proof
@@ -801,7 +801,7 @@ Inductive exp_alpha:
                (Letrec (funs1 ++ (y,perm_exp x y e)::funs2) e1))
 End
 
-Triviality MAP_PAIR_MAP':
+Theorem MAP_PAIR_MAP'[local]:
   MAP (λ(x,y). h x) (MAP (f ## g) l) = MAP h (MAP f (MAP FST l)) ∧
   MAP (λ(x,y). h y) (MAP (f ## g) l) = MAP h (MAP g (MAP SND l))
 Proof
@@ -904,7 +904,7 @@ Proof
   rw[fmap_rel_def]
 QED
 
-Triviality APPEND_EQ_IMP:
+Theorem APPEND_EQ_IMP[local]:
   ∀(a : 'a list) b c d.
     a = b ∧ c = d ⇒ a ++ c = b ++ d
 Proof
@@ -2811,7 +2811,7 @@ Proof
       rw[])
 QED
 
-Triviality closed_Letrec_perm_lemma:
+Theorem closed_Letrec_perm_lemma[local]:
   x ≠ y ∧
   y ∉ freevars(Letrec (funs1 ++ (x,e)::funs2) e1) ∧
   MEM x (MAP FST funs2) ∧
@@ -2830,7 +2830,7 @@ Proof
   gvs[]
 QED
 
-Triviality closed_Letrec_perm_lemma':
+Theorem closed_Letrec_perm_lemma'[local]:
   MEM x (MAP FST f) ∧
   MEM y (MAP FST f)
   ⇒
@@ -2844,7 +2844,7 @@ Proof
   metis_tac[perm1_def,FST,SND,PAIR]
 QED
 
-Triviality closed_Letrec_perm_lemma'':
+Theorem closed_Letrec_perm_lemma''[local]:
   MEM e1 (MAP SND f) ∧
   MEM e2 (MAP SND f) ∧
   closed (Letrec f e1) ⇒
@@ -2854,7 +2854,7 @@ Proof
   metis_tac[FST,SND,PAIR]
 QED
 
-Triviality closed_Letrec_perm_lemma''':
+Theorem closed_Letrec_perm_lemma'''[local]:
   x ≠ y ∧
   x ∉ (freevars (Letrec (funs1 ++ funs2) e1)) ∧
   ¬MEM x (MAP FST funs1) ∧ ¬MEM x (MAP FST funs2) ∧
@@ -3028,7 +3028,7 @@ Inductive wh_alpha:
     ⇒ wh_alpha (wh_Closure x e1) (wh_Closure y e2))
 End
 
-Triviality wh_alpha_sym_imp:
+Theorem wh_alpha_sym_imp[local]:
   ∀wh1 wh2.
     wh_alpha wh1 wh2
   ⇒ wh_alpha wh2 wh1
@@ -3060,7 +3060,7 @@ Proof
   rw[] >> eq_tac >> rw[wh_alpha_sym_imp]
 QED
 
-Triviality perm_exp_eqvt_alt:
+Theorem perm_exp_eqvt_alt[local]:
   ∀ v1 v2 e.
     IMAGE (perm1 v1 v2) (freevars e) = freevars (perm_exp v1 v2 e)
 Proof
@@ -3068,7 +3068,7 @@ Proof
   simp[freevars_eqvt, MEM_MAP]
 QED
 
-Triviality perm1_MAP_unchanged:
+Theorem perm1_MAP_unchanged[local]:
   ∀x y e.
     ¬ MEM x (freevars_l e) ∧ ¬ MEM y (freevars_l e)
   ⇒ MAP (perm1 x y) (freevars_l e) = freevars_l e
@@ -3076,7 +3076,7 @@ Proof
   rw[LIST_EQ_REWRITE, EL_MAP] >> gvs[MEM_EL, GSYM IMP_DISJ_THM, perm1_def]
 QED
 
-Triviality perm1_swap:
+Theorem perm1_swap[local]:
   ∀x y z a.
     x ≠ z ∧ x ≠ y ⇒
   perm1 x y (perm1 y z a) =
@@ -3094,7 +3094,7 @@ Proof
   >- (Cases_on `a = z` >> gvs[])
 QED
 
-Triviality perm_exp_swap:
+Theorem perm_exp_swap[local]:
   ∀x y e z.
     x ≠ z ∧ x ≠ y ⇒
   perm_exp x y (perm_exp y z e) =
diff --git a/meta-theory/pure_congruenceScript.sml b/meta-theory/pure_congruenceScript.sml
index 184574b3..24ca7dba 100644
--- a/meta-theory/pure_congruenceScript.sml
+++ b/meta-theory/pure_congruenceScript.sml
@@ -134,26 +134,26 @@ Inductive Howe:
   (∀vars x e2.
      R vars (Var x) e2 ⇒
      Howe R vars (Var x) e2)
- 
+
 [Howe2:]
   (∀x e1 e1' e2 vars.
      Howe R (x INSERT vars) e1 e1' ∧
      R vars (Lam x e1') e2 ⇒
      Howe R vars (Lam x e1) e2)
- 
+
 [Howe3:]
   (∀e1 e1' e3 vars.
      Howe R vars e1 e1' ∧
      Howe R vars e2 e2' ∧
      R vars (App e1' e2') e3 ⇒
      Howe R vars (App e1 e2) e3)
- 
+
 [Howe4:]
   (∀es es' e op vars.
     LIST_REL (Howe R vars) es es' ∧
     R vars (Prim op es') e ⇒
     Howe R vars (Prim op es) e)
- 
+
 [Howe5:]
   (∀ves ves' e e' e2.
     Howe R (vars ∪ set (MAP FST ves)) e e' ∧
@@ -733,7 +733,7 @@ Proof
   \\ imp_res_tac Howe_open_similarity_IMP_closed
 QED
 
-Triviality perm_exp_IN_Exps:
+Theorem perm_exp_IN_Exps[local]:
   freevars ce2 ⊆ {y} ⇒ perm_exp x y ce2 ∈ Exps {x}
 Proof
   fs [Exps_def]
@@ -849,7 +849,7 @@ Proof
   >- (gvs[] >> metis_tac[UNION_COMM, UNION_ASSOC, INSERT_SING_UNION])
 QED
 
-Triviality closed_Letrec_funs:
+Theorem closed_Letrec_funs[local]:
   ∀ fs e f.
     closed (Letrec fs e) ∧
     MEM f fs
@@ -2271,7 +2271,7 @@ Proof
   \\ match_mp_tac exp_eq_subst \\ fs []
 QED
 
-Triviality subst_eq_bind:
+Theorem subst_eq_bind[local]:
   (∀n v. FLOOKUP m n = SOME v ⇒ closed v) ⇒
   subst m e = bind m e
 Proof
@@ -2367,7 +2367,7 @@ Proof
   \\ match_mp_tac exp_eq_perm \\ fs [closed_def]
 QED
 
-Triviality Lam_Lam:
+Theorem Lam_Lam[local]:
   (Lam x e1 ≅? Lam y e2) b ⇔
   ∀xv yv. closed xv ∧ closed yv ⇒ (subst1 y yv (Lam x e1) ≅? subst1 x xv (Lam y e2)) b
 Proof
@@ -2386,7 +2386,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality subst_subst_lemma:
+Theorem subst_subst_lemma[local]:
   closed y1 ∧ closed y2 ⇒
   ((subst1 x y1 e1 ≅? subst1 y y2 e2) b ⇔
    ∀xv yv. closed xv ∧ closed yv ⇒
@@ -2788,7 +2788,7 @@ Proof
   \\ qspec_then ‘[a;b;c]’ mp_tac Let_Prim \\ rw []
 QED
 
-Triviality Letrec_Prim_closed:
+Theorem Letrec_Prim_closed[local]:
   ∀l p xs b. EVERY (λfb. freevars (SND fb) ⊆ set (MAP FST l)) l
          /\ EVERY (\e. freevars e ⊆ set (MAP FST l)) xs ==>
     (Letrec l (Prim p xs) ≅? Prim p (MAP (Letrec l) xs)) b
@@ -2914,7 +2914,7 @@ Proof
   \\ Induct \\ Cases_on ‘es’ \\ fs []
 QED
 
-Triviality Apps_Lams_lemma:
+Theorem Apps_Lams_lemma[local]:
   EVERY (λv. closed (f v)) vs ⇒
   eval_wh (Apps (Lams vs e) (MAP f vs)) =
   eval_wh (subst (FEMPTY |++ MAP (λv. (v, f v)) vs) e)
diff --git a/meta-theory/pure_ctxt_equivScript.sml b/meta-theory/pure_ctxt_equivScript.sml
index 3ad3ee19..199d1877 100644
--- a/meta-theory/pure_ctxt_equivScript.sml
+++ b/meta-theory/pure_ctxt_equivScript.sml
@@ -122,7 +122,7 @@ Proof
     )
 QED
 
-Triviality app_bisimilarity_plug:
+Theorem app_bisimilarity_plug[local]:
   ∀c x y. (x ≃ y) T ∧ closed (plug c x) ⇒ (plug c x ≃ plug c y) T
 Proof
   rw[app_bisimilarity_eq]
@@ -199,7 +199,7 @@ Definition wh_to_cons_def:
   wh_to_cons  wh_Error = wh_Err
 End
 
-Triviality app_bisimilarity_wh_to_cons:
+Theorem app_bisimilarity_wh_to_cons[local]:
   ∀x y. (x ≃ y) T ⇒ wh_to_cons (eval_wh x) = wh_to_cons (eval_wh y)
 Proof
   rw[Once app_bisimilarity_iff_alt2] >>
@@ -220,7 +220,7 @@ Definition step_eval_wh_def:
     | NONE => NONE
 End
 
-Triviality step_eval_wh_eq:
+Theorem step_eval_wh_eq[local]:
   ∀l e1 e2. eval_wh e1 = eval_wh e2 ⇒ step_eval_wh l e1 = step_eval_wh l e2
 Proof
   Cases >> rw[step_eval_wh_def] >>
@@ -246,7 +246,7 @@ Proof
   Induct >> rw[BindAllocsC_def, BindAllocs_def, plug_def]
 QED
 
-Triviality freevars_BindAllocs:
+Theorem freevars_BindAllocs[local]:
   ∀n e. freevars (BindAllocs n e) ⊆ freevars e
 Proof
   Induct >> rw[BindAllocs_def] >>
@@ -342,7 +342,7 @@ Proof
     )
 QED
 
-Triviality not_app_bisimilarity_IMP_not_step_eval_wh:
+Theorem not_app_bisimilarity_IMP_not_step_eval_wh[local]:
   ∀e1 e2.
     ¬ (e1 ≃ e2) T ∧ closed e1 ∧ closed e2
   ⇒ ∃l. step_eval_wh l e1 ≠ step_eval_wh l e2
@@ -573,7 +573,7 @@ Proof
   goal_assum drule >> simp[]
 QED
 
-Triviality interp_simps[simp]:
+Theorem interp_simps[local,simp]:
   (∀k st. interp wh_Diverge k st = Div) ∧
   (∀x. interp (wh_Constructor "Ret" [x]) Done [] = Ret Termination) ∧
   (∀k st. interp wh_Error k st = Ret Error)
diff --git a/meta-theory/pure_exp_lemmasScript.sml b/meta-theory/pure_exp_lemmasScript.sml
index b191bb7a..571efd7d 100644
--- a/meta-theory/pure_exp_lemmasScript.sml
+++ b/meta-theory/pure_exp_lemmasScript.sml
@@ -717,13 +717,13 @@ Proof
   gvs[DELETE_DEF, closed_def] >> rw[] >> gvs[SUBSET_DIFF_EMPTY]
 QED
 
-Triviality FDOMSUB_EQ_FDIFF:
+Theorem FDOMSUB_EQ_FDIFF[local]:
   M \\ x = FDIFF M {x}
 Proof
   rw [REWRITE_RULE [pred_setTheory.EXTENSION] fmap_EXT, FDIFF_def, DRESTRICT_DEF, DOMSUB_FAPPLY_NEQ]
 QED
 
-Triviality FDOM_FLOOKUP:
+Theorem FDOM_FLOOKUP[local]:
   x IN FDOM m <=> FLOOKUP m x <> NONE
 Proof
   Cases_on `FLOOKUP m x` \\ fs [FLOOKUP_DEF]
diff --git a/meta-theory/pure_exp_relScript.sml b/meta-theory/pure_exp_relScript.sml
index 294dcae9..becf0068 100644
--- a/meta-theory/pure_exp_relScript.sml
+++ b/meta-theory/pure_exp_relScript.sml
@@ -89,7 +89,7 @@ Definition FF_def:
   FF b s = { (e1, e2) | unfold_rel s (e1, e2) b }
 End
 
-Triviality monotone_similarity:
+Theorem monotone_similarity[local]:
   monotone (FF b)
 Proof
   fs [monotone_def,FF_def,unfold_rel_def] >>
@@ -128,7 +128,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality monotone_bisimilarity:
+Theorem monotone_bisimilarity[local]:
   monotone (λs. { (e1,e2) | (e1,e2) IN FF b s ∧ (e2,e1) IN FF b (opp s) })
 Proof
   fs [monotone_def,FF_def,unfold_rel_def,opp_def] >>
diff --git a/meta-theory/pure_letrec_congScript.sml b/meta-theory/pure_letrec_congScript.sml
index 45fe41b6..23a2acde 100644
--- a/meta-theory/pure_letrec_congScript.sml
+++ b/meta-theory/pure_letrec_congScript.sml
@@ -216,13 +216,13 @@ Proof
     \\ rw [] \\ res_tac \\ fs [])
 QED
 
-Triviality FDOM_UPDATES_EQ:
+Theorem FDOM_UPDATES_EQ[local]:
   ∀b1. FDOM (FEMPTY |++ MAP (λ(g,x). (g,Letrec b2 x)) b1) = set (MAP FST b1)
 Proof
   fs [FDOM_FUPDATE_LIST,MAP_MAP_o,combinTheory.o_DEF,UNCURRY,SF ETA_ss]
 QED
 
-Triviality EVERY_FLOOKUP_closed_lemma:
+Theorem EVERY_FLOOKUP_closed_lemma[local]:
   EVERY (λe. freevars e ⊆ set (MAP FST ys)) (MAP SND ys) ⇒
   (∀n v.
      FLOOKUP (FEMPTY |++ MAP (λ(g,x). (g,Letrec ys x)) ys) n = SOME v ⇒
@@ -263,7 +263,7 @@ Proof
   metis_tac [LIST_REL_MEM]
 QED
 
-Triviality eval_wh_Constructor_NIL_bisim =
+Theorem eval_wh_Constructor_NIL_bisim[local] =
   eval_wh_Constructor_bisim |> Q.GEN ‘xs’ |> Q.SPEC ‘[]’ |> SIMP_RULE (srw_ss()) [];
 
 Theorem eval_forward_letrec_binds:
@@ -763,7 +763,7 @@ Proof
   \\ metis_tac [app_bisimilarity_sym]
 QED
 
-Triviality LIST_REL_IMP_same_keys:
+Theorem LIST_REL_IMP_same_keys[local]:
   ∀binds1 binds2.
     LIST_REL (λ(v1,e1) (v2,e2). v1 = v2) binds1 binds2 ⇒
     MAP FST binds1 = MAP FST binds2
diff --git a/meta-theory/pure_letrec_delargScript.sml b/meta-theory/pure_letrec_delargScript.sml
index 621f7658..c4eb9641 100644
--- a/meta-theory/pure_letrec_delargScript.sml
+++ b/meta-theory/pure_letrec_delargScript.sml
@@ -183,7 +183,7 @@ Proof
   \\ fs [] \\ pop_assum $ irule_at Any
 QED
 
-Triviality LIST_REL_ignore_first:
+Theorem LIST_REL_ignore_first[local]:
   ∀xs ys. LIST_REL (λx y. P x) xs ys ⇔ EVERY P xs ∧ LENGTH xs = LENGTH ys
 Proof
   Induct \\ fs [PULL_EXISTS] \\ rw [] \\ eq_tac \\ rw [] \\ res_tac
@@ -227,7 +227,7 @@ Proof
   >- (irule letrec_delarg_Letrec \\ fs [] \\ simp [Once LIST_REL_SWAP])
 QED
 
-Triviality mk_letrec_neq[simp]:
+Theorem mk_letrec_neq[local,simp]:
   mk_letrec b i x ≠ Lam v t ∧
   mk_letrec b i x ≠ App x1 x2 ∧
   mk_letrec b i x ≠ Prim p ps ∧
@@ -240,7 +240,7 @@ Proof
   \\ fs [Apps_def]
 QED
 
-Triviality EVERY_FLOOKUP_closed_lemma:
+Theorem EVERY_FLOOKUP_closed_lemma[local]:
   EVERY (λe. freevars e ⊆ set (MAP FST ys)) (MAP SND ys) ⇒
   (∀n v.
      FLOOKUP (FEMPTY |++ MAP (λ(g,x). (g,Letrec ys x)) ys) n = SOME v ⇒
@@ -252,7 +252,7 @@ Proof
   \\ res_tac \\ fs []
 QED
 
-Triviality LIST_REL_freevars_lemma_1:
+Theorem LIST_REL_freevars_lemma_1[local]:
   ∀xs ys.
     LIST_REL (λx y. freevars x = freevars y) xs ys ⇒
     MAP freevars xs = MAP freevars ys
@@ -305,7 +305,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality LIST_REL_freevars_lemma:
+Theorem LIST_REL_freevars_lemma[local]:
   ∀xs ys.
     LIST_REL (λx y. letrec_delarg i x y ∧ freevars x = freevars y) xs ys ⇒
     MAP freevars xs = MAP freevars ys
@@ -561,10 +561,10 @@ Proof
   \\ fs [FLOOKUP_DEF]
 QED
 
-Triviality eval_wh_Constructor_NIL_bisim =
+Theorem eval_wh_Constructor_NIL_bisim[local] =
   eval_wh_Constructor_bisim |> Q.GEN ‘xs’ |> Q.SPEC ‘[]’ |> SIMP_RULE (srw_ss()) [];
 
-Triviality LIST_REL_letrec_delarg_closed:
+Theorem LIST_REL_letrec_delarg_closed[local]:
   ∀xs ys. LIST_REL (letrec_delarg i) xs ys ∧ EVERY closed xs ⇒ EVERY closed ys
 Proof
   Induct \\ rw [] \\ fs []
@@ -653,7 +653,7 @@ Definition wh_Closures_def:
   wh_Closures (v::vs) e = wh_Closure v (Lams vs e)
 End
 
-Triviality eval_wh_to_Apps_div:
+Theorem eval_wh_to_Apps_div[local]:
   ∀xs x k.
     eval_wh_to k x = wh_Diverge ⇒
     eval_wh_to k (Apps x xs) = wh_Diverge
@@ -667,7 +667,7 @@ Definition mk_body_def:
     subst1 i.fname (mk_rec b i) (if b then i.rhs_T else i.rhs_F)
 End
 
-Triviality ignore_FDIFF:
+Theorem ignore_FDIFF[local]:
   DISJOINT (FDOM f) m ⇒ FDIFF f m = f
 Proof
   fs [fmap_EXT,FDIFF_def,DRESTRICT_DEF]
@@ -879,14 +879,14 @@ Proof
   \\ imp_res_tac remove_call_arg_dup \\ fs []
 QED
 
-Triviality lemma1:
+Theorem lemma1[local]:
   LENGTH xs2 = LENGTH xs1 ∧ ~MEM k xs1 ⇒
   ALOOKUP (REVERSE (ZIP (xs1,xs2))) k = NONE
 Proof
   fs [ALOOKUP_NONE,MAP_REVERSE,MAP_FST_ZIP]
 QED
 
-Triviality lemma2:
+Theorem lemma2[local]:
   ∀xs1 ys1 vs k'.
     LENGTH xs1 = LENGTH vs ∧
     EVERY closed xs1 ∧ MEM k' vs ∧
@@ -1511,7 +1511,7 @@ Proof
   \\ fs [letrec_delarg_refl,eval_forward_letrec_delarg,eval_forward_letrec_delarg_rev]
 QED
 
-Triviality remove_call_arg_T_with:
+Theorem remove_call_arg_T_with[local]:
   ∀b1 b2 b i R x y.
     remove_call_arg b1 b2 b i R x y ⇒ b ⇒
     remove_call_arg b1 b2 b (i with <|rhs_T := rhs1; rhs_F := rhs2|>) R x y
@@ -1537,7 +1537,7 @@ Proof
   \\ Induct \\ fs [PULL_EXISTS]
 QED
 
-Triviality MAP_FST_EQ_IMP:
+Theorem MAP_FST_EQ_IMP[local]:
   ∀xs ys x y.
     MAP FST xs = MAP FST ys ⇒
     MEM (x,y) xs ⇒ ∃z. MEM (x,z) ys
@@ -1791,7 +1791,7 @@ Proof
   \\ gvs [Abbr‘i2’]
 QED
 
-Triviality letrec_del_arg' =
+Theorem letrec_del_arg'[local] =
   letrec_del_arg
   |> Q.INST [‘i’|->‘<| fname := f;
                        args := vs;
@@ -1806,13 +1806,13 @@ Triviality letrec_del_arg' =
 
 Overload call_with_spec[local] = “pure_letrec_spec$call_with_arg”
 
-Triviality Lams_app_lemma:
+Theorem Lams_app_lemma[local]:
   ∀xs. Lams (xs ++ ys) b = Lams xs (Lams ys b)
 Proof
   Induct \\ fs [Lams_def]
 QED
 
-Triviality Letrec_specialise' =
+Theorem Letrec_specialise'[local] =
   Letrec_specialise
   |> Q.INST [‘i’|->‘<| fname := f;
                        args := vs;
@@ -1838,7 +1838,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality rename_lemma:
+Theorem rename_lemma[local]:
   v ∉ boundvars rhs1 ∧
   w ∉ boundvars rhs1 ∧
   w ∉ freevars rhs1 ∧
@@ -1893,7 +1893,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality invent_name:
+Theorem invent_name[local]:
   FINITE (s:'a set) ∧ ~FINITE (UNIV:'a set) ⇒ ∃k. k ∉ s
 Proof
   rw [] \\ gvs [NOT_IN_FINITE]
@@ -2068,7 +2068,7 @@ Proof
   \\ gvs [EVERY_MEM,MEM_MAP,EXISTS_PROD] \\ metis_tac []
 QED
 
-Triviality map_fst_eq_lemma:
+Theorem map_fst_eq_lemma[local]:
   ∀xs ys.
     MAP FST xs = MAP FST ys ⇒
     ∀x. (∃y. MEM (x,y) xs) ⇔ ∃y. MEM (x,y) ys
@@ -2201,7 +2201,7 @@ Proof
   \\ fs []
 QED
 
-Triviality Letrec_Lam_1 =
+Theorem Letrec_Lam_1[local] =
   pure_demandTheory.Letrec_Lam_weak
   |> Q.SPEC ‘[(f,x)]’ |> SIMP_RULE std_ss [MAP,EVERY_DEF,MEM]
   |> Q.GENL [‘f’,‘x’]
diff --git a/meta-theory/pure_letrec_seqScript.sml b/meta-theory/pure_letrec_seqScript.sml
index 89d89446..6ad1744e 100644
--- a/meta-theory/pure_letrec_seqScript.sml
+++ b/meta-theory/pure_letrec_seqScript.sml
@@ -119,7 +119,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality MAP_FST_mk_bind:
+Theorem MAP_FST_mk_bind[local]:
   MAP FST (MAP mk_bind binds) = MAP FST binds
 Proof
   Induct_on ‘binds’ \\ fs [FORALL_PROD,mk_bind_def]
@@ -149,7 +149,7 @@ Definition obl_syntax_def:
       set (MAP FST (FILTER SND args)) ⊆ freevars body) binds
 End
 
-Triviality IMP_obl_syntax[simp]:
+Theorem IMP_obl_syntax[local,simp]:
   obligation binds ⇒ obl_syntax binds
 Proof
   fs [obligation_def,obl_syntax_def,EVERY_MEM,FORALL_PROD,SF SFY_ss]
@@ -176,7 +176,7 @@ Proof
   metis_tac [freevars_mk_seqs_syntax,IMP_obl_syntax]
 QED
 
-Triviality FDOM_UPDATES_EQ:
+Theorem FDOM_UPDATES_EQ[local]:
   ∀b1. FDOM (FEMPTY |++ MAP (λ(g,x). (g,Letrec b2 x)) b1) = set (MAP FST b1)
 Proof
   fs [FDOM_FUPDATE_LIST,MAP_MAP_o,combinTheory.o_DEF,UNCURRY,SF ETA_ss]
@@ -462,7 +462,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality EVERY_FLOOKUP_closed_lemma:
+Theorem EVERY_FLOOKUP_closed_lemma[local]:
   EVERY (λe. freevars e ⊆ set (MAP FST ys)) (MAP SND ys) ⇒
   (∀n v.
      FLOOKUP (FEMPTY |++ MAP (λ(g,x). (g,Letrec ys x)) ys) n = SOME v ⇒
@@ -494,7 +494,7 @@ Proof
   \\ Induct_on ‘xs’ \\ fs [FORALL_PROD]
 QED
 
-Triviality subst_funs_Seq_Zero:
+Theorem subst_funs_Seq_Zero[local]:
   (∀n v. FLOOKUP (FEMPTY |++ MAP (λ(g,x). (g,Letrec xs x)) xs) n = SOME v ⇒
          closed v) ⇒
   subst_funs xs (Seq Zero x) = Seq Zero (subst_funs xs x)
@@ -561,10 +561,10 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality eval_wh_Constructor_NIL_bisim =
+Theorem eval_wh_Constructor_NIL_bisim[local] =
   eval_wh_Constructor_bisim |> Q.GEN ‘xs’ |> Q.SPEC ‘[]’ |> SIMP_RULE (srw_ss()) [];
 
-Triviality IMP_Seq_Zero:
+Theorem IMP_Seq_Zero[local]:
   closed y ∧ (x ≃ y) F ⇒ (x ≃ Seq Zero y) F
 Proof
   rw []
@@ -625,7 +625,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality freevars_mk_seqs':
+Theorem freevars_mk_seqs'[local]:
   freevars (mk_seqs vs e) =
   set (MAP FST (FILTER SND vs)) UNION freevars e
 Proof
@@ -1386,7 +1386,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality FLOOKUP_FLOOKUP_IMP_LIST_REL:
+Theorem FLOOKUP_FLOOKUP_IMP_LIST_REL[local]:
   EVERY (λb. FST (f b) = FST (g b) ∧ P (SND (f b)) (SND (g b))) binds ⇒
   (∀k v1 v2.
      FLOOKUP (FEMPTY |++ MAP f binds) k = SOME v1 ∧
@@ -1441,7 +1441,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality Seq_Zero:
+Theorem Seq_Zero[local]:
   ∀x y. x ≈ y ⇒ Seq Zero x ≈ y
 Proof
   rw [] \\ irule exp_eq_trans
@@ -1549,7 +1549,7 @@ Proof
       \\ irule_at Any EQ_REFL)
 QED
 
-Triviality FDIFF_LIST_FUPDATE:
+Theorem FDIFF_LIST_FUPDATE[local]:
   FDIFF (FEMPTY |++ ys) P = FEMPTY |++ (FILTER (λ(x,y). ~P x) ys)
 Proof
   fs [fmap_eq_flookup,FLOOKUP_FDIFF,GSYM FILTER_REVERSE,
@@ -1557,7 +1557,7 @@ Proof
   \\ rw [] \\ fs [IN_DEF]
 QED
 
-Triviality subst_mk_seqs:
+Theorem subst_mk_seqs[local]:
   ∀args m.
     DISJOINT (FDOM m) (set (MAP FST args)) ⇒
     subst m (mk_seqs args e) = mk_seqs args (subst m e)
@@ -1587,7 +1587,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality Apps_cong1:
+Theorem Apps_cong1[local]:
   ∀xs f g. f ≈ g ⇒ Apps f xs ≈ Apps g xs
 Proof
   Induct \\ fs [Apps_def]
@@ -1622,7 +1622,7 @@ Proof
   \\ PairCases \\ Cases_on ‘h1’ \\ fs [mk_seqs_def]
 QED
 
-Triviality mk_seqs_cong:
+Theorem mk_seqs_cong[local]:
   ∀args x y. x ≈ y ⇒ mk_seqs args x ≈ mk_seqs args y
 Proof
   Induct
@@ -1725,7 +1725,7 @@ Proof
   \\ fs []
 QED
 
-Triviality ALOOKUP_IMP_FLOOKUP:
+Theorem ALOOKUP_IMP_FLOOKUP[local]:
   ALOOKUP bs f = SOME (args,body) ∧ obl_syntax binds ∧
   set bs ⊆ set binds ⇒
   FLOOKUP (FEMPTY |++
@@ -1760,7 +1760,7 @@ Proof
   \\ qexists_tac ‘f’ \\ fs []
 QED
 
-Triviality mk_seqs_eq_Seqs:
+Theorem mk_seqs_eq_Seqs[local]:
   ∀args e. mk_seqs args e = Seqs (MAP (Var o FST) (FILTER SND args)) e
 Proof
   Induct \\ fs [mk_seqs_def]
diff --git a/meta-theory/pure_letrec_specScript.sml b/meta-theory/pure_letrec_specScript.sml
index 08a6630c..0a639761 100644
--- a/meta-theory/pure_letrec_specScript.sml
+++ b/meta-theory/pure_letrec_specScript.sml
@@ -198,7 +198,7 @@ Proof
   >- (irule letrec_spec_Letrec \\ fs [] \\ simp [Once LIST_REL_SWAP])
 QED
 
-Triviality mk_letrec_neq[simp]:
+Theorem mk_letrec_neq[local,simp]:
   mk_letrec b i x ≠ Lam v t ∧
   mk_letrec b i x ≠ App x1 x2 ∧
   mk_letrec b i x ≠ Prim p ps ∧
@@ -211,7 +211,7 @@ Proof
   \\ fs [Apps_def]
 QED
 
-Triviality EVERY_FLOOKUP_closed_lemma:
+Theorem EVERY_FLOOKUP_closed_lemma[local]:
   EVERY (λe. freevars e ⊆ set (MAP FST ys)) (MAP SND ys) ⇒
   (∀n v.
      FLOOKUP (FEMPTY |++ MAP (λ(g,x). (g,Letrec ys x)) ys) n = SOME v ⇒
@@ -515,10 +515,10 @@ Proof
   \\ fs [FLOOKUP_DEF]
 QED
 
-Triviality eval_wh_Constructor_NIL_bisim =
+Theorem eval_wh_Constructor_NIL_bisim[local] =
   eval_wh_Constructor_bisim |> Q.GEN ‘xs’ |> Q.SPEC ‘[]’ |> SIMP_RULE (srw_ss()) [];
 
-Triviality LIST_REL_letrec_spec_closed:
+Theorem LIST_REL_letrec_spec_closed[local]:
   ∀xs ys. LIST_REL (letrec_spec i) xs ys ∧ EVERY closed xs ⇒ EVERY closed ys
 Proof
   Induct \\ rw [] \\ fs []
@@ -611,7 +611,7 @@ Definition wh_Closures_def:
   wh_Closures (v::vs) e = wh_Closure v (Lams vs e)
 End
 
-Triviality eval_wh_to_Apps_div:
+Theorem eval_wh_to_Apps_div[local]:
   ∀xs x k.
     eval_wh_to k x = wh_Diverge ⇒
     eval_wh_to k (Apps x xs) = wh_Diverge
@@ -625,7 +625,7 @@ Definition mk_body_def:
     subst1 i.fname (mk_rec b i) (if b then subst1 i.arg i.const i.rhs else i.rhs)
 End
 
-Triviality ignore_FDIFF:
+Theorem ignore_FDIFF[local]:
   DISJOINT (FDOM f) m ⇒ FDIFF f m = f
 Proof
   fs [fmap_EXT,FDIFF_def,DRESTRICT_DEF]
@@ -1431,7 +1431,7 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality call_with_arg_T_with:
+Theorem call_with_arg_T_with[local]:
   ∀b i R x y.
     call_with_arg b i R x y ⇒ b ⇒
     call_with_arg b (i with <|const := c; rhs := rhs1|>) R x y
diff --git a/meta-theory/pure_obs_sem_equalScript.sml b/meta-theory/pure_obs_sem_equalScript.sml
index dce70883..e176e6bf 100644
--- a/meta-theory/pure_obs_sem_equalScript.sml
+++ b/meta-theory/pure_obs_sem_equalScript.sml
@@ -14,7 +14,7 @@ Ancestors
 Libs
   term_tactic BasicProvers dep_rewrite intLib
 
-Triviality eval_wh_Cons:
+Theorem eval_wh_Cons[local]:
   wh_Constructor n es = eval_wh x ∧ (x ≃ y) b ⇒
   ∃es1. eval_wh y = wh_Constructor n es1 ∧ LIST_REL (λx y. (x ≃ y) b) es es1
 Proof
diff --git a/misc/quotient_llistScript.sml b/misc/quotient_llistScript.sml
index 0c7c0130..d713bd4d 100644
--- a/misc/quotient_llistScript.sml
+++ b/misc/quotient_llistScript.sml
@@ -5,7 +5,7 @@ Ancestors
 Libs
   quotientLib
 
-Triviality LMAP_id:
+Theorem LMAP_id[local]:
   LMAP (\x. x) = \x. x
 Proof
   irule EQ_EXT >>
@@ -58,7 +58,7 @@ Proof
   \\ Q.ISPECL_THEN [‘z’] strip_assume_tac llist_CASES \\ fs []
 QED
 
-Triviality llist_rel_lemma:
+Theorem llist_rel_lemma[local]:
   ∀R.
     (∀x y. R x y ⇔ R x = R y) ⇒
     ∀z w.
diff --git a/typeclass/compiler/parsing/ast_to_texpScript.sml b/typeclass/compiler/parsing/ast_to_texpScript.sml
index fdf8ec32..6947d77c 100644
--- a/typeclass/compiler/parsing/ast_to_texpScript.sml
+++ b/typeclass/compiler/parsing/ast_to_texpScript.sml
@@ -938,14 +938,14 @@ Termination
   PairCases_on `h` >> gvs[]
 End
 
-Triviality delete_cmp_of:
+Theorem delete_cmp_of[local]:
   cmp_of (delete m k) = cmp_of m
 Proof
   Cases_on `m` >>
   simp[delete_def,cmp_of_def]
 QED
 
-Triviality FDOM_FLOOKUP_unit:
+Theorem FDOM_FLOOKUP_unit[local]:
   FLOOKUP m x = SOME () <=> x IN FDOM m
 Proof
   simp[miscTheory.FDOM_FLOOKUP]
@@ -962,7 +962,7 @@ Proof
   gvs[insert_thm, union_thm]
 QED
 
-Triviality MAP_FST_toAscList_cepat_vars_impl:
+Theorem MAP_FST_toAscList_cepat_vars_impl[local]:
   set (MAP FST (toAscList $ cepat_vars_impl pat)) =
     cepat_vars pat
 Proof
@@ -1062,13 +1062,13 @@ Definition monad_cn_mlstrings_def:
     [«Ret»;«Bind»;«Raise»;«Handle»;«Alloc»;«Length»;«Deref»;«Update»;«Act»]
 End
 
-Triviality implodeEQ:
+Theorem implodeEQ[local]:
   y = implode x ⇔ (explode y = x)
 Proof
   rw[EQ_IMP_THM] >> simp[]
 QED
 
-Triviality MEM_monad_cn_mlstrings:
+Theorem MEM_monad_cn_mlstrings[local]:
   MEM x monad_cn_mlstrings ⇔ explode x ∈ monad_cns
 Proof
   rw[monad_cn_mlstrings_def, pure_configTheory.monad_cns_def] >>
diff --git a/typeclass/typing/pure_tcexp_lemmasScript.sml b/typeclass/typing/pure_tcexp_lemmasScript.sml
index 9cb23137..1922cffa 100644
--- a/typeclass/typing/pure_tcexp_lemmasScript.sml
+++ b/typeclass/typing/pure_tcexp_lemmasScript.sml
@@ -18,7 +18,7 @@ Proof
   metis_tac[]
 QED
 
-Triviality MAPi_ID[simp]:
+Theorem MAPi_ID[local,simp]:
   ∀l. MAPi (λn v. v) l = l
 Proof
   Induct >> rw[combinTheory.o_DEF]
@@ -157,14 +157,14 @@ Proof
   simp[subst_lets_for, combinTheory.o_DEF]
 QED
 
-Triviality patguards_subst_FST:
+Theorem patguards_subst_FST[local]:
   patguards eps = (gd,binds) ⇒
   FST (patguards (MAP (subst f ## I) eps)) = subst f gd
 Proof
   metis_tac[patguards_subst,FST]
 QED
 
-Triviality patguards_subst_SND:
+Theorem patguards_subst_SND[local]:
   patguards eps = (gd,binds) ⇒
   SND (patguards (MAP (subst f ## I) eps)) =
     MAP (I ## subst f) binds
@@ -364,7 +364,7 @@ Proof
   irule exp_eq_Lam_cong >> first_x_assum irule >> simp[]
 QED
 
-Triviality subst1_lets_for_closed:
+Theorem subst1_lets_for_closed[local]:
   ¬ MEM var (MAP SND vs) ∧ closed x
   ⇒ subst1 var x (lets_for cn ar v vs e) =
     subst1 var x (lets_for cn ar v vs (subst1 var x e))
@@ -373,7 +373,7 @@ Proof
   PairCases_on `h` >> gvs[lets_for_def, subst1_def]
 QED
 
-Triviality subst1_lets_for_cexp_closed:
+Theorem subst1_lets_for_cexp_closed[local]:
   ¬ MEM var (MAP SND vs) ∧ closed x
   ⇒ subst1 var x (lets_for cn v vs e) =
     subst1 var x (lets_for cn v vs (subst1 var x e))
@@ -503,7 +503,7 @@ Proof
   once_rewrite_tac[exp_eq_sym] >> irule lets_for_exp_eq_lemma >> simp[]
 QED
 
-Triviality exp_eq_FOLDR_cong_base_case:
+Theorem exp_eq_FOLDR_cong_base_case[local]:
   e ≅ e' ∧ (∀x y y'. y ≅ y' ⇒  f x y ≅ f x y') ⇒
   FOLDR f e l ≅ FOLDR f e' l
 Proof
diff --git a/typeclass/typing/pure_tcexp_typingProofScript.sml b/typeclass/typing/pure_tcexp_typingProofScript.sml
index 82b5b9ec..88a8841c 100644
--- a/typeclass/typing/pure_tcexp_typingProofScript.sml
+++ b/typeclass/typing/pure_tcexp_typingProofScript.sml
@@ -59,7 +59,7 @@ Inductive type_wh:
   (type_ok (SND ns) db t ⇒ type_wh ns db st env wh_Diverge t)
 End
 
-Triviality type_wh_PrimTy_eq_wh_Atom:
+Theorem type_wh_PrimTy_eq_wh_Atom[local]:
   type_wh ns db st env wh (Atom $ PrimTy pt) ∧ pt ≠ Bool ⇒
     wh = wh_Diverge ∨ ∃a. wh = wh_Atom a
 Proof
@@ -69,7 +69,7 @@ Proof
   Cases_on `arg_tys` >> gvs[Functions_def]
 QED
 
-Triviality type_wh_PrimTy_Bool_eq_wh_Constructor:
+Theorem type_wh_PrimTy_Bool_eq_wh_Constructor[local]:
   type_wh ns db st env wh (Atom $ PrimTy Bool) ⇒
     wh = wh_Diverge ∨ wh = wh_Constructor "True" [] ∨
     wh = wh_Constructor "False" []
@@ -81,13 +81,13 @@ Proof
   >- (gvs[get_PrimTys_def, type_atom_op_cases, type_lit_cases])
 QED
 
-Triviality Monad_cons_types:
+Theorem Monad_cons_types[local]:
   Monad t = cons_types (Atom $ CompPrimTy $ M) [t]
 Proof
   simp[cons_types_def]
 QED
 
-Triviality type_wh_Function_eq_wh_Closure:
+Theorem type_wh_Function_eq_wh_Closure[local]:
   type_wh ns db st env wh
     (cons_types (Atom $ CompPrimTy Function) [at; t]) ⇒
     wh = wh_Diverge ∨ ∃x body. wh = wh_Closure x body
@@ -99,14 +99,14 @@ Proof
   gvs[cons_types_def]
 QED
 
-Triviality Array_cons_types:
+Theorem Array_cons_types[local]:
   Cons (Atom (CompPrimTy Array)) t =
   cons_types (Atom $ CompPrimTy Array) [t]
 Proof
   simp[cons_types_def]
 QED
 
-Triviality type_wh_TypeCons_eq_wh_Constructor:
+Theorem type_wh_TypeCons_eq_wh_Constructor[local]:
   type_wh ns db st env wh (tcons_to_type (INL id) ts) ⇒
     wh = wh_Diverge ∨ ∃cname es. wh = wh_Constructor cname es
 Proof
@@ -118,7 +118,7 @@ Proof
   gvs[Functions_cons_types,cons_types_Atom_EQ]
 QED
 
-Triviality type_wh_Array_eq_Loc:
+Theorem type_wh_Array_eq_Loc[local]:
   type_wh ns db st env wh (Cons (Atom $ CompPrimTy Array) t) ⇒
     wh = wh_Diverge ∨ ∃a n. wh = wh_Atom (Loc n) ∧ oEL n st = SOME t
 Proof
@@ -137,7 +137,7 @@ Proof
   Cases_on `arg_tys` >> gvs[Functions_def]
 QED
 
-Triviality type_wh_Tuple_eq_wh_Constructor:
+Theorem type_wh_Tuple_eq_wh_Constructor[local]:
   type_wh ns db st env wh (cons_types (Tup n) ts) ⇒
     wh = wh_Diverge ∨ ∃es. wh = wh_Constructor "" es
 Proof
@@ -149,7 +149,7 @@ Proof
   gvs[Functions_cons_types,cons_types_Atom_EQ]
 QED
 
-Triviality type_wh_Exception_eq_wh_Constructor:
+Theorem type_wh_Exception_eq_wh_Constructor[local]:
   type_wh ns db st env wh (Atom Exception) ⇒
     wh = wh_Diverge ∨ ∃cn es. wh = wh_Constructor cn es
 Proof
@@ -442,7 +442,7 @@ QED
 TODO: relating tcexp_type_cepat with safe_proj_pat?
 *)
 
-Triviality MAPi_ID[simp]:
+Theorem MAPi_ID[local,simp]:
   ∀l. MAPi (λn v. v) l = l
 Proof
   Induct >> rw[combinTheory.o_DEF]
diff --git a/typeclass/typing/pure_tcexp_typingPropsScript.sml b/typeclass/typing/pure_tcexp_typingPropsScript.sml
index 04da3894..86f38cec 100644
--- a/typeclass/typing/pure_tcexp_typingPropsScript.sml
+++ b/typeclass/typing/pure_tcexp_typingPropsScript.sml
@@ -1050,7 +1050,7 @@ Proof
   simp[]
 QED
 
-Triviality cons_types_not_Exception:
+Theorem cons_types_not_Exception[local]:
   cons_types (Atom $ TypeCons c) l ≠ Atom Exception
 Proof
   rw[cons_types_EQ_Atom]
@@ -1093,7 +1093,7 @@ Proof
   )
 QED
 
-Triviality APPEND_ASSOC_four:
+Theorem APPEND_ASSOC_four[local]:
   ks ++ db1 ++ tks ++ db2 = (ks ++ db1) ++ tks ++ db2
 Proof
   metis_tac[APPEND_ASSOC]
@@ -1992,13 +1992,13 @@ Proof
   )
 QED
 
-Triviality MAP_FST_tshift_env:
+Theorem MAP_FST_tshift_env[local]:
   MAP FST (tshift_env n env) = MAP FST env
 Proof
   simp[MAP_MAP_o,combinTheory.o_DEF,FST_THM,LAMBDA_PROD]
 QED
 
-Triviality APPEND_SING_APPEND:
+Theorem APPEND_SING_APPEND[local]:
   l ++ [x] ++ l' = l ++ x::l'
 Proof
   metis_tac[APPEND_ASSOC,APPEND]
diff --git a/typeclass/typing/test_typeclass_typingScript.sml b/typeclass/typing/test_typeclass_typingScript.sml
index 8f4d0901..871e3ea4 100644
--- a/typeclass/typing/test_typeclass_typingScript.sml
+++ b/typeclass/typing/test_typeclass_typingScript.sml
@@ -293,13 +293,13 @@ Definition test_prog_elaborated_def:
   ]
 End
 
-Triviality UNIQUE_MEMBER_SUBSET_SING:
+Theorem UNIQUE_MEMBER_SUBSET_SING[local]:
   (∀x. x ∈ s ⇒ x = y) ⇔ s ⊆ {y}
 Proof
   rw[EQ_IMP_THM,SUBSET_DEF]
 QED
 
-Triviality IN_SINGLETON:
+Theorem IN_SINGLETON[local]:
   x ∈ {x}
 Proof
   irule $ iffRL IN_SING >>
diff --git a/typeclass/typing/typeclass_env_map_implScript.sml b/typeclass/typing/typeclass_env_map_implScript.sml
index 894d0f49..00d6941e 100644
--- a/typeclass/typing/typeclass_env_map_implScript.sml
+++ b/typeclass/typing/typeclass_env_map_implScript.sml
@@ -354,7 +354,7 @@ Proof
   gvs[IN_DEF]
 QED
 
-Triviality GSPEC_super_reachable_or:
+Theorem GSPEC_super_reachable_or[local]:
   {s | super_reachable cl_map c s ∨ c = s} =
     super_reachable cl_map c ∪ {c}
 Proof
@@ -393,13 +393,13 @@ Proof
   metis_tac[super_reachable_FINITE]
 QED
 
-Triviality INTER_PRESERVE_SUBSET:
+Theorem INTER_PRESERVE_SUBSET[local]:
   s ⊆ s' ∧ x ⊆ x' ⇒ (s ∩ x) ⊆ (s' ∩ x')
 Proof
   simp[INTER_DEF,SUBSET_DEF,EXTENSION,IN_DEF]
 QED
 
-Triviality COMPL_SUBSET:
+Theorem COMPL_SUBSET[local]:
   s ⊆ s' ⇒ COMPL s' ⊆ COMPL s
 Proof
   rw[COMPL_DEF,SUBSET_DEF] >>
@@ -784,7 +784,7 @@ Proof
   )
 QED
 
-Triviality PATH_IMP_RTC:
+Theorem PATH_IMP_RTC[local]:
   ∀l x y.
     1 ≤ LENGTH l ∧ EL 0 l = x ∧ EL (LENGTH l - 1) l = y ∧
     (∀n. n < (LENGTH l -1) ⇒ R (EL n l) (EL (SUC n) l)) ⇒
@@ -806,7 +806,7 @@ Proof
   simp[]
 QED
 
-Triviality RTC_PATH:
+Theorem RTC_PATH[local]:
   RTC R x y ⇔ (∃l. 1 ≤ LENGTH l ∧ ALL_DISTINCT l ∧
     EL 0 l = x ∧ EL (LENGTH l - 1) l = y ∧
     ∀n. n < (LENGTH l -1) ⇒ R (EL n l) (EL (SUC n) l))
@@ -836,14 +836,14 @@ Proof
   metis_tac[PATH_IMP_RTC,EL]
 QED
 
-Triviality HD_TL:
+Theorem HD_TL[local]:
   1 < LENGTH l ⇒ HD (TL l) = EL 1 l
 Proof
   Cases_on `l` >>
   simp[]
 QED
 
-Triviality DROP1_EQ_TL:
+Theorem DROP1_EQ_TL[local]:
   DROP 1 l = TL l
 Proof
   Cases_on `l` >>
@@ -1489,7 +1489,7 @@ Proof
   metis_tac[entail_super_TypeVar]
 QED
 
-Triviality entail_wf_lookup_super:
+Theorem entail_wf_lookup_super[local]:
   entail_wf cl_map inst_map ∧
   lookup cl_map c = SOME c' ∧
   MEM s c'.supers ∧
@@ -1542,7 +1542,7 @@ Proof
   metis_tac[super_reachable_RTC_trans]
 QED
 
-Triviality entail_wf_super_reachable_RTC_aux:
+Theorem entail_wf_super_reachable_RTC_aux[local]:
   entail_wf cl_map inst_map ⇒
   ∀p. entail cl_map inst_map ps p ⇒
     ∀c t clinfo s. p = (c,t) ∧
diff --git a/typeclass/typing/typeclass_kindCheckScript.sml b/typeclass/typing/typeclass_kindCheckScript.sml
index 5492902e..a6c5a7c8 100644
--- a/typeclass/typing/typeclass_kindCheckScript.sml
+++ b/typeclass/typing/typeclass_kindCheckScript.sml
@@ -32,7 +32,7 @@ Proof
   simp[kind_arrows_def,Kind_size_def]
 QED
 
-Triviality kindArrow_kind_arrows_NEQ:
+Theorem kindArrow_kind_arrows_NEQ[local]:
   k ≠ kindArrow h (kind_arrows ks k)
 Proof
   `Kind_size k < Kind_size (kindArrow h (kind_arrows ks k))`
@@ -247,7 +247,7 @@ Proof
   gvs[freetyvars_ok_def,miscTheory.LLOOKUP_THM]
 QED
 
-Triviality kind_wf_mono_helper:
+Theorem kind_wf_mono_helper[local]:
   ∀k t.
     kind_wf cdb vdb k t ⇒
   ∀cdb' vdb'.
diff --git a/typeclass/typing/typeclass_texpScript.sml b/typeclass/typing/typeclass_texpScript.sml
index a203893a..4f5457fc 100644
--- a/typeclass/typing/typeclass_texpScript.sml
+++ b/typeclass/typing/typeclass_texpScript.sml
@@ -185,7 +185,7 @@ Termination
   rw[] >> gs[]
 End
 
-Triviality MAX_SET_LE:
+Theorem MAX_SET_LE[local]:
   FINITE s ∧ (∀y. y ∈ s ⇒ y ≤ x) ⇒
   MAX_SET s ≤ x
 Proof
@@ -195,7 +195,7 @@ Proof
   simp[GREATER_EQ]
 QED
 
-Triviality MAX_SET_LT:
+Theorem MAX_SET_LT[local]:
   FINITE s ∧ (∀y. y ∈ s ⇒ y < x) ∧ 0 < x ⇒
   MAX_SET s < x
 Proof
@@ -295,7 +295,7 @@ Proof
     GSYM pure_cexpTheory.cepat_vars_l_correct]
 QED
 
-Triviality texp_wf_strong_helper:
+Theorem texp_wf_strong_helper[local]:
   (∀(e:'a texp). texp_wf_strong e ⇔
     (texp_wf e ∧ texp_Lits_wf e)) ∧
   (∀(es:'a texp list). EVERY texp_wf_strong es ⇔
diff --git a/typeclass/typing/typeclass_typesPropsScript.sml b/typeclass/typing/typeclass_typesPropsScript.sml
index 1d67a7f8..87d9d41a 100644
--- a/typeclass/typing/typeclass_typesPropsScript.sml
+++ b/typeclass/typing/typeclass_typesPropsScript.sml
@@ -67,7 +67,7 @@ Proof
   Cases_on `bs` >> gvs[Functions_def]
 QED
 
-Triviality type_size_Functions:
+Theorem type_size_Functions[local]:
   type_size (Functions [] x) = type_size x ∧
   type_size (Functions (arg::args) x) = type_size arg + type_size
   (Functions args x) + 3 + atom_ty_size (CompPrimTy Function)
@@ -75,7 +75,7 @@ Proof
   rw[Functions_def,type_size_def]
 QED
 
-Triviality self_EQ_Functions_self:
+Theorem self_EQ_Functions_self[local]:
   x = Functions args x ⇒ args = []
 Proof
   `args ≠ [] ⇒ type_size x < type_size (Functions args x)`
diff --git a/typeclass/typing/typeclass_typingProofScript.sml b/typeclass/typing/typeclass_typingProofScript.sml
index a79b20fb..861fa112 100644
--- a/typeclass/typing/typeclass_typingProofScript.sml
+++ b/typeclass/typing/typeclass_typingProofScript.sml
@@ -601,7 +601,7 @@ Proof
   gvs[SmartApp_def,freevars_cexp_def,dest_App_def,SF ETA_ss]
 QED
 
-Triviality LIST_REL_pred_tsubst:
+Theorem LIST_REL_pred_tsubst[local]:
   ∀ps qs.
     LIST_REL (λ(c,t) (c',t'). c = c' ∧ tsubst subs t = t')
       ((cl,t)::ps) ((cl',t')::qs) ⇔
@@ -740,14 +740,14 @@ Proof
   simp[translate_predicates_LIST_REL]
 QED
 
-Triviality ALOOKUP_APPEND_EQ:
+Theorem ALOOKUP_APPEND_EQ[local]:
   ALOOKUP l x = ALOOKUP l' x ⇒
   ALOOKUP (l ++ r) x = ALOOKUP (l' ++ r) x
 Proof
   rw[ALOOKUP_APPEND]
 QED
 
-Triviality INTER_EMPTY_IN_NOTIN:
+Theorem INTER_EMPTY_IN_NOTIN[local]:
   (a ∩ b = EMPTY) ⇔ (∀x. x ∈ a ⇒ x ∉ b)
 Proof
   simp[IN_DEF,INTER_DEF,EXTENSION,IMP_DISJ_THM]
@@ -1250,7 +1250,7 @@ Proof
   )
 QED
 
-Triviality CONS_APPEND_APPEND:
+Theorem CONS_APPEND_APPEND[local]:
   x::(l ++ m ++ r) = x::l ++ m ++ r
 Proof
   simp[]
@@ -1283,13 +1283,13 @@ Proof
   metis_tac[]
 QED
 
-Triviality FST_3:
+Theorem FST_3[local]:
   (λ(p1,p1',p2). p1) = FST
 Proof
   simp[GSYM LAMBDA_PROD,GSYM pure_miscTheory.FST_THM]
 QED
 
-Triviality FST_o_FST:
+Theorem FST_o_FST[local]:
   (λ((p1,p2),p2'). p1) = (FST o FST)
 Proof
   simp[combinTheory.o_DEF,FST,LAMBDA_PROD]
@@ -1390,7 +1390,7 @@ Proof
   >- metis_tac[tcexp_exhaustive_cepat_List]
 QED
 
-Triviality MAP_PROD_EQ_MAP_FST:
+Theorem MAP_PROD_EQ_MAP_FST[local]:
   MAP (λ(ks,t). (ks, f ks t)) l = MAP ($, h) l' ⇔
   (l' = MAP (λ(ks,t). f ks t) l ∧ EVERY ($= h o FST) l)
 Proof
@@ -1422,14 +1422,14 @@ Proof
   >- metis_tac[tcexp_exhaustive_cepat_List]
 QED
 
-Triviality DISJOINT_NOT_IN_R:
+Theorem DISJOINT_NOT_IN_R[local]:
   DISJOINT a b ⇔ (∀x. x ∈ a ⇒ x ∉ b)
 Proof
   rw[DISJOINT_DEF,EXTENSION] >>
   metis_tac[]
 QED
 
-Triviality DISJOINT_NOT_IN_L:
+Theorem DISJOINT_NOT_IN_L[local]:
   DISJOINT a b ⇔ (∀x. x ∈ b ⇒ x ∉ a)
 Proof
   rw[DISJOINT_DEF,EXTENSION] >>
@@ -2359,7 +2359,7 @@ Proof
   )
 QED
 
-Triviality ALL_DISTINCT_APPEND_DISJOINT:
+Theorem ALL_DISTINCT_APPEND_DISJOINT[local]:
   ALL_DISTINCT (a ++ b) ⇔
     ALL_DISTINCT a ∧ ALL_DISTINCT b ∧
     DISJOINT (set a) (set b)
@@ -2512,7 +2512,7 @@ Proof
   simp[]
 QED
 
-Triviality LENGTH_SUM_1:
+Theorem LENGTH_SUM_1[local]:
   (∀x. MEM x xs ⇒ f x = 1) ⇒
   SUM (MAP f xs) = LENGTH xs
 Proof
@@ -2731,7 +2731,7 @@ Proof
   )
 QED
 
-Triviality translate_methods_aux_lem:
+Theorem translate_methods_aux_lem[local]:
   ∀n.
   LENGTH l ≤ len ⇒
   translate_methods_aux cons len n l =
@@ -2756,13 +2756,13 @@ Proof
   rw[LIST_EQ_REWRITE]
 QED
 
-Triviality Functions_CONS_alt:
+Theorem Functions_CONS_alt[local]:
   Functions (at::ats) t = Functions [at] (Functions ats t)
 Proof
   simp[Functions_def]
 QED
 
-Triviality Cons_eq_cons_types:
+Theorem Cons_eq_cons_types[local]:
   Cons t t' = cons_types t [t']
 Proof
   simp[cons_types_def]
@@ -2995,7 +2995,7 @@ Proof
   simp[kind_ok,LLOOKUP_THM,specialises_def,subst_db_def]
 QED
 
-Triviality class_map_super_accessors_entailment_kind_ok_aux:
+Theorem class_map_super_accessors_entailment_kind_ok_aux[local]:
   ∀cl_map' c ent rest.
   ALL_DISTINCT (MAP FST cl_map) ∧
   class_map_kind_ok tds cl_map ∧
@@ -3253,7 +3253,7 @@ Proof
   )
 QED
 
-Triviality ALL_DISTINCT_method_names_EL_LT_IMP_class_EQ:
+Theorem ALL_DISTINCT_method_names_EL_LT_IMP_class_EQ[local]:
   ALL_DISTINCT (method_names cl_map) ∧
   i < j ∧ j < LENGTH cl_map ∧
   EL i cl_map = (clname,cl) ∧
@@ -3423,7 +3423,7 @@ Proof
   simp[]
 QED
 
-Triviality SmartLam_EQ_LENGHT_LT_IMP:
+Theorem SmartLam_EQ_LENGHT_LT_IMP[local]:
   SmartLam () vs e = SmartLam () vs' e' ∧
   LENGTH vs < LENGTH vs' ⇒
   ∃us. vs' = vs ++ us ∧
@@ -3461,14 +3461,14 @@ Proof
   gvs[]
 QED
 
-Triviality NOT_EMPTY_IMP_LENGTH_SUC:
+Theorem NOT_EMPTY_IMP_LENGTH_SUC[local]:
   l ≠ [] ⇒ ∃n. LENGTH l = SUC n
 Proof
   Cases_on `l` >>
   simp[]
 QED
 
-Triviality SmartLam_EQ_LENGTH_EQ_IMP:
+Theorem SmartLam_EQ_LENGTH_EQ_IMP[local]:
   SmartLam () vs e = SmartLam () vs' e' ∧
   LENGTH vs = LENGTH vs' ⇒
   vs = vs' ∧ e = e'
@@ -4396,7 +4396,7 @@ Proof
   rw[] >> simp[]
 QED
 
-Triviality type_tcexp_env_extensional_weak:
+Theorem type_tcexp_env_extensional_weak[local]:
   ALOOKUP env = ALOOKUP env' ∧
   type_tcexp ns db st env e t ⇒
   type_tcexp ns db st env' e t
@@ -4406,7 +4406,7 @@ Proof
   simp[]
 QED
 
-Triviality type_tcexp_env_shift_extensional_weak_LIST_REL:
+Theorem type_tcexp_env_shift_extensional_weak_LIST_REL[local]:
   ALOOKUP new_env = ALOOKUP env' ∧
   LIST_REL
     (λ(fn,body) (vars,scheme).
@@ -4430,7 +4430,7 @@ Proof
   simp[ELIM_UNCURRY,SRULE[ELIM_UNCURRY] ALOOKUP_MAP_2]
 QED
 
-Triviality type_tcexp_weaken_env_shift_LIST_REL:
+Theorem type_tcexp_weaken_env_shift_LIST_REL[local]:
   LIST_REL
     (λ(p1,p2) (p1',p2').
        type_tcexp trans_ns p1' (MAP (tshift (LENGTH p1')) st)
diff --git a/typeclass/typing/typeclass_typingPropsScript.sml b/typeclass/typing/typeclass_typingPropsScript.sml
index 35e2d161..bcebc294 100644
--- a/typeclass/typing/typeclass_typingPropsScript.sml
+++ b/typeclass/typing/typeclass_typingPropsScript.sml
@@ -399,7 +399,7 @@ Proof
   gvs[LIST_REL_EL_EQN,kind_ok,kind_arrows_kindType_EQ]
 QED
 
-Triviality LIST_REL3_IMP_helper:
+Theorem LIST_REL3_IMP_helper[local]:
   ∀xs ys zs.
   LIST_REL3 (λx y z. P x y z ⇒ Q x y z) xs ys zs ⇒
   LIST_REL3 P xs ys zs ⇒
diff --git a/typeclass/typing/typeclass_typingScript.sml b/typeclass/typing/typeclass_typingScript.sml
index d90923da..4561ca17 100644
--- a/typeclass/typing/typeclass_typingScript.sml
+++ b/typeclass/typing/typeclass_typingScript.sml
@@ -1015,7 +1015,7 @@ End
 (* Prove that if we can type_elaborate, then we can do dictionary
 * construction on the output *)
 
-Triviality INFINITE_mlstring:
+Theorem INFINITE_mlstring[local]:
   INFINITE 𝕌(:mlstring)
 Proof
   strip_assume_tac mlstringTheory.explode_BIJ >>
@@ -1024,7 +1024,7 @@ Proof
   simp[INFINITE_LIST_UNIV]
 QED
 
-Triviality DISTINCT_SUBSET:
+Theorem DISTINCT_SUBSET[local]:
   s ∩ u = {} ∧ v ⊆ u ⇒ s ∩ v = {}
 Proof
   rw[] >>
@@ -1037,7 +1037,7 @@ Proof
   simp[]
 QED
 
-Triviality INFINITE_INTER_FINITE_EMPTY:
+Theorem INFINITE_INTER_FINITE_EMPTY[local]:
   ∀s. FINITE s ⇒ INFINITE (u:'a set) ⇒
     ∃v. INFINITE v ∧ v ⊆ u ∧ v ∩ s = ∅
 Proof
@@ -1071,7 +1071,7 @@ Proof
   simp[]
 QED
 
-Triviality INFINITE_TAKE_N:
+Theorem INFINITE_TAKE_N[local]:
   INFINITE v ⇒ ∃s. s ⊆ v ∧ FINITE s ∧ CARD s = n
 Proof
   Induct_on `n` >>
@@ -1083,7 +1083,7 @@ Proof
   simp[]
 QED
 
-Triviality EXISTS_fresh_vars_list:
+Theorem EXISTS_fresh_vars_list[local]:
   FINITE s ⇒
   ∃vs. LENGTH (vs:mlstring list) = n ∧ set vs ∩ s = {} ∧ ALL_DISTINCT vs
 Proof
@@ -1102,7 +1102,7 @@ Proof
   simp[]
 QED
 
-Triviality DISTINCT_FRANGE:
+Theorem DISTINCT_FRANGE[local]:
   set (MAP FST l) ∩ FDOM m = {} ∧ ALL_DISTINCT (MAP FST l) ⇒
     FRANGE m ∪ set (MAP SND l) = FRANGE (m |++ l)
 Proof
@@ -1138,7 +1138,7 @@ Proof
     pred_setTheory.INSERT_INTER]
 QED
 
-Triviality DISTINCT_FRANGE_ZIP:
+Theorem DISTINCT_FRANGE_ZIP[local]:
   LENGTH vs = LENGTH ps ∧
   set vs ∩ FDOM m = {} ∧ ALL_DISTINCT vs ⇒
     FRANGE m ∪ set ps = FRANGE (m |++ ZIP (vs,ps))
diff --git a/typeclass/typing/typeclass_unificationScript.sml b/typeclass/typing/typeclass_unificationScript.sml
index 31a1d196..23db0548 100644
--- a/typeclass/typing/typeclass_unificationScript.sml
+++ b/typeclass/typing/typeclass_unificationScript.sml
@@ -23,19 +23,19 @@ Definition decode_utype_def[nocompute]:
   decode_utype (Var n) = iCVar n
 End
 
-Triviality I_o_f:
+Theorem I_o_f[local]:
   ∀m. I o_f m = m
 Proof
   rw[GSYM fmap_EQ_THM]
 QED
 
-Triviality option_map_case:
+Theorem option_map_case[local]:
   ∀f opt. OPTION_MAP f opt = case opt of NONE => NONE | SOME a => SOME $ f a
 Proof
   gen_tac >> Cases >> simp[]
 QED
 
-Triviality option_bind_case:
+Theorem option_bind_case[local]:
   ∀x f. OPTION_BIND x f = case x of NONE => NONE | SOME y => f y
 Proof
   Cases >> simp[]
@@ -331,7 +331,7 @@ Proof
   )
 QED
 
-Triviality pure_unify_ind_lemma:
+Theorem pure_unify_ind_lemma[local]:
   ∀P.
     (∀us ut1 ut2 s t1 t2.
        us = encode_itype o_f s ∧
@@ -428,7 +428,7 @@ Definition pure_walkstar_def[nocompute]:
     decode_utype $ walkstar (encode_itype o_f s) (encode_itype t)
 End
 
-Triviality pure_walkstar_ind_lemma:
+Theorem pure_walkstar_ind_lemma[local]:
  ∀s. pure_wfs s ⇒
   ∀P.
     (∀t.
diff --git a/typing/pure_inferenceProofScript.sml b/typing/pure_inferenceProofScript.sml
index c76c79f7..90dabe2d 100644
--- a/typing/pure_inferenceProofScript.sml
+++ b/typing/pure_inferenceProofScript.sml
@@ -905,7 +905,7 @@ Proof
   first_x_assum drule >> simp[]
 QED
 
-Triviality new_vars_SUBSET:
+Theorem new_vars_SUBSET[local]:
   BIGUNION (FRANGE as) ⊆ BIGUNION (FRANGE as') ∧ cs ⊆ cs' ∧
   pure_vars it ⊆ pure_vars it' ∧
   v ∈ new_vars as cs it ⇒
@@ -914,7 +914,7 @@ Proof
   rw[new_vars_def] >> gvs[SUBSET_DEF] >> metis_tac[]
 QED
 
-Triviality new_vars_SUBSET_minfer:
+Theorem new_vars_SUBSET_minfer[local]:
   BIGUNION (FRANGE as) ⊆ BIGUNION (FRANGE as') ∧ cs ⊆ cs' ∧
   pure_vars it ⊆ new_vars as cs Exception ⇒
   ∀n. n ∈ new_vars as cs it ⇒ n ∈ new_vars as' cs' it'
@@ -922,7 +922,7 @@ Proof
   rw[new_vars_def] >> gvs[SUBSET_DEF, pure_vars] >> metis_tac[]
 QED
 
-Triviality pure_vars_csubst_EMPTY_suff:
+Theorem pure_vars_csubst_EMPTY_suff[local]:
   (∀it. it ∈ FRANGE s ⇒ pure_vars it = {}) ∧
   pure_vars t ⊆ FDOM s ⇒
   pure_vars (csubst s t) = {}
@@ -932,7 +932,7 @@ Proof
   simp[IMAGE_EQ_SING, SUBSET_DIFF_EMPTY]
 QED
 
-Triviality freedbvars_isubst_EMPTY_suff:
+Theorem freedbvars_isubst_EMPTY_suff[local]:
   ∀it its.
     freedbvars it ⊆ count (LENGTH its) ∧
     EVERY ( λit. freedbvars it = {}) its
@@ -943,7 +943,7 @@ Proof
   gvs[EVERY_EL]
 QED
 
-Triviality shift_shift_let_lemma:
+Theorem shift_shift_let_lemma[local]:
   ∀it t sub vs1 vs2.
     type_of (csubst (ishift vs1 o_f sub) it) = SOME t ∧
     freedbvars it ⊆ count vs1 ⇒
@@ -966,7 +966,7 @@ Proof
   simp[tshift_tshift] >> simp[GSYM tshift_tshift] >> simp[GSYM shift_db_shift_db]
 QED
 
-Triviality subset_union:
+Theorem subset_union[local]:
   a ⊆ c ⇒ a ⊆ b ∪ c
 Proof
   rw[SUBSET_DEF]
@@ -3615,7 +3615,7 @@ QED
 
 (******************** Constraint solving ********************)
 
-Triviality constraints_ok_subst_constraint:
+Theorem constraints_ok_subst_constraint[local]:
   constraints_ok ns (set (MAP to_mconstraint cs)) ∧
   pure_wfs sub ∧ (∀it. it ∈ FRANGE sub ⇒ itype_ok ns 0 it) ⇒
   constraints_ok ns (set (MAP to_mconstraint (MAP (subst_constraint sub) cs)))
@@ -3629,7 +3629,7 @@ Proof
   rpt $ irule_at Any itype_ok_pure_walkstar >> gvs[itype_ok_def]
 QED
 
-Triviality isubst_irrelevance:
+Theorem isubst_irrelevance[local]:
   pure_vars (isubst its it) ⊆ s ⇒
   isubst (MAP
     (λt. if pure_vars t ⊆ s then t else any) its) it =
@@ -3641,7 +3641,7 @@ Proof
   gvs[BIGUNION_SUBSET, MEM_MAP, PULL_EXISTS]
 QED
 
-Triviality pure_unify_FEMPTY:
+Theorem pure_unify_FEMPTY[local]:
   pure_unify FEMPTY t1 t2 = SOME s ⇒
     pure_wfs s ∧
     pure_walkstar s t1 = pure_walkstar s t2 ∧
@@ -3652,7 +3652,7 @@ Proof
   gvs[pure_uP, pure_allvars]
 QED
 
-Triviality subst_constraint_DISJOINT_FDOM:
+Theorem subst_constraint_DISJOINT_FDOM[local]:
   ∀s c. pure_wfs s ⇒
     DISJOINT (FDOM s) (mactivevars (to_mconstraint (subst_constraint s c)))
 Proof
@@ -3667,7 +3667,7 @@ Proof
   metis_tac[DISJOINT_ALT, pure_walkstar_vars_notin]
 QED
 
-Triviality mactivevars_subst_constraint:
+Theorem mactivevars_subst_constraint[local]:
   pure_wfs s ⇒
   mactivevars (to_mconstraint (subst_constraint s c)) ⊆
   mactivevars (to_mconstraint c) ∪ pure_substvars s
@@ -3697,7 +3697,7 @@ Proof
     )
 QED
 
-Triviality msubst_vars_FUNION:
+Theorem msubst_vars_FUNION[local]:
   ∀t s.
     pure_wfs s ∧ pure_wfs t ∧
     DISJOINT (FDOM t) (pure_substvars s)
@@ -3716,7 +3716,7 @@ Proof
     )
 QED
 
-Triviality pure_substvars_FUNION:
+Theorem pure_substvars_FUNION[local]:
   DISJOINT (FDOM s1) (FDOM s2) ⇒
   pure_substvars (FUNION s1 s2) = pure_substvars s1 ∪ pure_substvars s2
 Proof
@@ -3724,7 +3724,7 @@ Proof
   simp[AC UNION_ASSOC UNION_COMM]
 QED
 
-Triviality satisfies_FUNION:
+Theorem satisfies_FUNION[local]:
   ∀c. DISJOINT (FDOM t) (pure_substvars s) ∧ pure_wfs s ∧ pure_wfs t ∧
     satisfies tds s (to_mconstraint (subst_constraint t c)) ⇒
     satisfies tds (FUNION t s) (to_mconstraint c)
@@ -3740,7 +3740,7 @@ Proof
     )
 QED
 
-Triviality constraint_vars_subst_constraint_SUBSET:
+Theorem constraint_vars_subst_constraint_SUBSET[local]:
   pure_substvars s ⊆ X ∧ pure_wfs s ∧
   constraint_vars (to_mconstraint c) ⊆ X
   ⇒ constraint_vars (to_mconstraint (subst_constraint s c)) ⊆ X
diff --git a/typing/pure_inferencePropsScript.sml b/typing/pure_inferencePropsScript.sml
index e62af583..6fdb1b4c 100644
--- a/typing/pure_inferencePropsScript.sml
+++ b/typing/pure_inferencePropsScript.sml
@@ -1209,7 +1209,7 @@ Proof
   DEP_REWRITE_TAC[lookup_insert] >> simp[]
 QED
 
-Triviality pure_vars_pure_apply_subst_DBVar_o_f[simp]:
+Theorem pure_vars_pure_apply_subst_DBVar_o_f[local,simp]:
   ∀t s.
     pure_vars (pure_apply_subst (DBVar o_f s) t) =
     pure_vars t DIFF FDOM s
diff --git a/typing/pure_inferenceScript.sml b/typing/pure_inferenceScript.sml
index c84d2684..a16ce7eb 100644
--- a/typing/pure_inferenceScript.sml
+++ b/typing/pure_inferenceScript.sml
@@ -977,7 +977,7 @@ Definition reserved_cn_mlstrings_def:
      «Ret»;«Bind»;«Raise»;«Handle»;«Alloc»;«Length»;«Deref»;«Update»;«Act»]
 End
 
-Triviality type_wf_TypeCons_impl_lemma:
+Theorem type_wf_TypeCons_impl_lemma[local]:
   (∃ar cdefs.
     oEL id tdefs = SOME (ar, cdefs) ∧
     LENGTH tyargs = ar)
diff --git a/typing/pure_inference_modelScript.sml b/typing/pure_inference_modelScript.sml
index 02255b91..2642a4ad 100644
--- a/typing/pure_inference_modelScript.sml
+++ b/typing/pure_inference_modelScript.sml
@@ -463,7 +463,7 @@ End
 
 (******************** Lemmas ********************)
 
-Triviality maunion_comm:
+Theorem maunion_comm[local]:
   ∀x y. maunion x y = maunion y x
 Proof
   rw[maunion_def] >>
@@ -519,7 +519,7 @@ Proof
   simp[miscTheory.toAList_domain]
 QED
 
-Triviality domain_list_insert_alt:
+Theorem domain_list_insert_alt[local]:
   domain (list_insert xs t) = set xs ∪ domain t
 Proof
   rw[EXTENSION, domain_list_insert]
@@ -559,7 +559,7 @@ Proof
   gvs[FLOOKUP_DEF] >> metis_tac[]
 QED
 
-Triviality infer_bind_alt_def:
+Theorem infer_bind_alt_def[local]:
   ∀g f.
     infer_bind g f = λs. case g s of Err e => Err e | OK ((a,b,c),s') => f (a,b,c) s'
 Proof
@@ -636,7 +636,7 @@ val _ = simpLib.register_frag inferM_ss;
 
 val inferM_rws = SF inferM_ss;
 
-Triviality infer_ignore_bind_simps[simp]:
+Theorem infer_ignore_bind_simps[local,simp]:
   (do _ <- ( λs. Err e) ; foo od = \s. Err e) ∧
   (do _ <- ( λs. OK ((),s)) ; foo od = foo)
 Proof
diff --git a/typing/pure_tcexp_lemmasScript.sml b/typing/pure_tcexp_lemmasScript.sml
index f140ccc5..625e1472 100644
--- a/typing/pure_tcexp_lemmasScript.sml
+++ b/typing/pure_tcexp_lemmasScript.sml
@@ -18,7 +18,7 @@ Proof
   metis_tac[]
 QED
 
-Triviality MAPi_ID[simp]:
+Theorem MAPi_ID[local,simp]:
   ∀l. MAPi (λn v. v) l = l
 Proof
   Induct >> rw[combinTheory.o_DEF]
@@ -237,7 +237,7 @@ Proof
   irule exp_eq_Lam_cong >> first_x_assum irule >> simp[]
 QED
 
-Triviality subst1_lets_for_closed:
+Theorem subst1_lets_for_closed[local]:
   ¬ MEM var (MAP SND vs) ∧ closed x
   ⇒ subst1 var x (lets_for cn ar v vs e) =
     subst1 var x (lets_for cn ar v vs (subst1 var x e))
@@ -246,7 +246,7 @@ Proof
   PairCases_on `h` >> gvs[lets_for_def, subst1_def]
 QED
 
-Triviality subst1_lets_for_cexp_closed:
+Theorem subst1_lets_for_cexp_closed[local]:
   ¬ MEM var (MAP SND vs) ∧ closed x
   ⇒ subst1 var x (lets_for cn v vs e) =
     subst1 var x (lets_for cn v vs (subst1 var x e))
diff --git a/typing/pure_typingProofScript.sml b/typing/pure_typingProofScript.sml
index f84592dc..1b1a689f 100644
--- a/typing/pure_typingProofScript.sml
+++ b/typing/pure_typingProofScript.sml
@@ -53,7 +53,7 @@ Inductive type_wh:
   (type_ok (SND ns) db t ⇒ type_wh ns db st env wh_Diverge t)
 End
 
-Triviality type_wh_PrimTy_eq_wh_Atom:
+Theorem type_wh_PrimTy_eq_wh_Atom[local]:
   type_wh ns db st env wh (PrimTy pt) ∧ pt ≠ Bool ⇒
     wh = wh_Diverge ∨ ∃a. wh = wh_Atom a
 Proof
@@ -61,7 +61,7 @@ Proof
   Cases_on `arg_tys` >> gvs[Functions_def]
 QED
 
-Triviality type_wh_PrimTy_Bool_eq_wh_Constructor:
+Theorem type_wh_PrimTy_Bool_eq_wh_Constructor[local]:
   type_wh ns db st env wh (PrimTy Bool) ⇒
     wh = wh_Diverge ∨ wh = wh_Constructor "True" [] ∨
     wh = wh_Constructor "False" []
@@ -71,14 +71,14 @@ Proof
   >- (gvs[get_PrimTys_def, type_atom_op_cases, type_lit_cases])
 QED
 
-Triviality type_wh_Function_eq_wh_Closure:
+Theorem type_wh_Function_eq_wh_Closure[local]:
   type_wh ns db st env wh (Function ft rt) ⇒
     wh = wh_Diverge ∨ ∃x body. wh = wh_Closure x body
 Proof
   rw[type_wh_cases] >> gvs[Once type_tcexp_cases]
 QED
 
-Triviality type_wh_TypeCons_eq_wh_Constructor:
+Theorem type_wh_TypeCons_eq_wh_Constructor[local]:
   type_wh ns db st env wh (TypeCons id ts) ⇒
     wh = wh_Diverge ∨ ∃cname es. wh = wh_Constructor cname es
 Proof
@@ -86,7 +86,7 @@ Proof
   Cases_on `arg_tys` >> gvs[Functions_def]
 QED
 
-Triviality type_wh_Array_eq_Loc:
+Theorem type_wh_Array_eq_Loc[local]:
   type_wh ns db st env wh (Array t) ⇒
     wh = wh_Diverge ∨ ∃a n. wh = wh_Atom (Loc n) ∧ oEL n st = SOME t
 Proof
@@ -94,7 +94,7 @@ Proof
   Cases_on `arg_tys` >> gvs[Functions_def]
 QED
 
-Triviality type_wh_Tuple_eq_wh_Constructor:
+Theorem type_wh_Tuple_eq_wh_Constructor[local]:
   type_wh ns db st env wh (Tuple ts) ⇒
     wh = wh_Diverge ∨ ∃es. wh = wh_Constructor "" es
 Proof
@@ -103,7 +103,7 @@ Proof
   Cases_on `arg_tys` >> gvs[Functions_def]
 QED
 
-Triviality type_wh_Exception_eq_wh_Constructor:
+Theorem type_wh_Exception_eq_wh_Constructor[local]:
   type_wh ns db st env wh Exception ⇒
     wh = wh_Diverge ∨ ∃cn es. wh = wh_Constructor cn es
 Proof
@@ -334,7 +334,7 @@ Proof
 QED
 
 
-Triviality MAPi_ID[simp]:
+Theorem MAPi_ID[local,simp]:
   ∀l. MAPi (λn v. v) l = l
 Proof
   Induct >> rw[combinTheory.o_DEF]
diff --git a/typing/pure_unificationScript.sml b/typing/pure_unificationScript.sml
index 4c0f606d..d9daed3d 100644
--- a/typing/pure_unificationScript.sml
+++ b/typing/pure_unificationScript.sml
@@ -59,19 +59,19 @@ Definition decode_utype_def[nocompute]:
   decode_utypes _ = NONE
 End
 
-Triviality I_o_f:
+Theorem I_o_f[local]:
   ∀m. I o_f m = m
 Proof
   rw[GSYM fmap_EQ_THM]
 QED
 
-Triviality option_map_case:
+Theorem option_map_case[local]:
   ∀f opt. OPTION_MAP f opt = case opt of NONE => NONE | SOME a => SOME $ f a
 Proof
   gen_tac >> Cases >> simp[]
 QED
 
-Triviality option_bind_case:
+Theorem option_bind_case[local]:
   ∀x f. OPTION_BIND x f = case x of NONE => NONE | SOME y => f y
 Proof
   Cases >> simp[]