diff --git a/examples/logic/folcompactness/folLangScript.sml b/examples/logic/folcompactness/folLangScript.sml
new file mode 100644
index 0000000000..05deabab68
--- /dev/null
+++ b/examples/logic/folcompactness/folLangScript.sml
@@ -0,0 +1,409 @@
+open HolKernel Parse boolLib bossLib;
+
+open pred_setTheory listTheory
+
+val _ = new_theory "folLang";
+
+val MAP_CONG' = REWRITE_RULE [GSYM AND_IMP_INTRO] MAP_CONG
+
+
+Definition LIST_UNION_def[simp]:
+  (LIST_UNION [] = ∅) ∧
+  (LIST_UNION (h::t) = h ∪ LIST_UNION t)
+End
+
+Theorem IN_LIST_UNION[simp]:
+  x ∈ LIST_UNION l ⇔ ∃s. MEM s l ∧ x ∈ s
+Proof
+  Induct_on ‘l’ >> simp[] >> metis_tac[]
+QED
+
+Theorem FINITE_LIST_UNION[simp]:
+  FINITE (LIST_UNION sets) ⇔ ∀s. MEM s sets ⇒ FINITE s
+Proof
+  Induct_on ‘sets’ >> simp[] >> metis_tac[]
+QED
+
+val _ = Datatype‘
+  term = V num | Fn num (term list)
+’;
+
+val term_size_def = DB.fetch "-" "term_size_def"
+val _ = export_rewrites ["term_size_def"]
+
+Theorem term_size_lemma[simp]:
+  ∀x l a. MEM a l ⇒ term_size a < 1 + (x + term1_size l)
+Proof
+  rpt gen_tac >> Induct_on ‘l’ >> simp[] >> rpt strip_tac >> simp[] >>
+  res_tac >> simp[]
+QED
+
+Theorem term_induct:
+  ∀P. (∀v. P (V v)) ∧ (∀n ts. (∀t. MEM t ts ⇒ P t) ⇒ P (Fn n ts)) ⇒
+      ∀t. P t
+Proof
+  rpt strip_tac >>
+  qspecl_then [‘P’, ‘λts. ∀t. MEM t ts ⇒ P t’]
+    (assume_tac o SIMP_RULE bool_ss [])
+    (TypeBase.induction_of “:term”) >> rfs[] >>
+  fs[DISJ_IMP_THM, FORALL_AND_THM]
+QED
+
+Definition tswap_def[simp]:
+  (tswap x y (V v) = if v = x then V y else if v = y then V x else V v) ∧
+  (tswap x y (Fn f ts) = Fn f (MAP (tswap x y) ts))
+Termination
+  WF_REL_TAC ‘measure (term_size o SND o SND)’ >> simp[]
+End
+
+Definition FVT_def[simp]:
+  (FVT (V v) = {v}) ∧
+  (FVT (Fn s ts) = LIST_UNION (MAP FVT ts))
+Termination
+  WF_REL_TAC ‘measure term_size’ >> simp[]
+End
+
+Theorem FVT_FINITE[simp]:
+  ∀t. FINITE (FVT t)
+Proof
+  ho_match_mp_tac term_induct >> simp[MEM_MAP, PULL_EXISTS]
+QED
+
+Theorem tswap_inv[simp]:
+  ∀t. tswap x y (tswap x y t) = t
+Proof
+  ho_match_mp_tac term_induct >> rw[] >> simp[MAP_MAP_o, Cong MAP_CONG']
+QED
+
+Theorem tswap_id[simp]:
+  ∀t. tswap x x t = t
+Proof
+  ho_match_mp_tac term_induct >> rw[] >> simp[MAP_MAP_o, Cong MAP_CONG']
+QED
+
+Theorem tswap_supp_id[simp]:
+  ∀t. x ∉ FVT t ∧ y ∉ FVT t ⇒ (tswap x y t = t)
+Proof
+  ho_match_mp_tac term_induct >> rw[] >> fs[MAP_MAP_o, MEM_MAP] >>
+  simp[LIST_EQ_REWRITE, EL_MAP] >> rw[] >> first_x_assum irule >>
+  metis_tac[MEM_EL]
+QED
+
+Definition termsubst_def[simp]:
+  (termsubst v (V x) = v x) ∧
+  (termsubst v (Fn f l) = Fn f (MAP (termsubst v) l))
+Termination
+  WF_REL_TAC ‘measure (term_size o SND)’ >> simp[]
+End
+
+Theorem termsubst_termsubst:
+  ∀t i j. termsubst j (termsubst i t) = termsubst (termsubst j o i) t
+Proof
+  ho_match_mp_tac term_induct >>
+  simp[MAP_MAP_o, combinTheory.o_ABS_R, Cong MAP_CONG']
+QED
+
+Theorem termsubst_triv[simp]:
+  ∀t. termsubst V t = t
+Proof
+  ho_match_mp_tac term_induct >> simp[Cong MAP_CONG']
+QED
+
+Theorem termsubst_valuation:
+  ∀t v1 v2. (∀x. x ∈ FVT t ⇒ (v1 x = v2 x)) ⇒ (termsubst v1 t = termsubst v2 t)
+Proof
+  ho_match_mp_tac term_induct >> simp[MEM_MAP, PULL_EXISTS] >> rpt strip_tac >>
+  irule MAP_CONG' >> simp[] >> rpt strip_tac >> first_x_assum irule >>
+  metis_tac[]
+QED
+
+Theorem termsubst_fvt:
+  ∀t i. FVT (termsubst i t) = { x | ∃y. y ∈ FVT t ∧ x ∈ FVT (i y) }
+Proof
+  ho_match_mp_tac term_induct >>
+  simp[MAP_MAP_o, combinTheory.o_ABS_R, MEM_MAP, PULL_EXISTS] >> rpt strip_tac>>
+  simp[Once EXTENSION,MEM_MAP,PULL_EXISTS] >> csimp[] >> metis_tac[]
+QED
+
+Theorem freshsubst_tswap:
+  ∀t. y ∉ FVT t ⇒ (termsubst V⦇ x ↦ V y ⦈ t = tswap x y t)
+Proof
+  ho_match_mp_tac term_induct >> simp[MEM_MAP,combinTheory.APPLY_UPDATE_THM] >>
+  rpt strip_tac >- (COND_CASES_TAC >> fs[]) >>
+  irule MAP_CONG' >> simp[] >> metis_tac[]
+QED
+
+val _ = Datatype‘
+  form = False
+       | Pred num (term list)
+       | IMP form form
+       | FALL num form
+’;
+
+Definition Not_def:
+  Not f = IMP f False
+End
+
+Definition True_def:
+  True = Not False
+End
+
+Definition Or_def:
+  Or p q = IMP (IMP p q) q
+End
+
+Definition And_def:
+  And p q = Not (Or (Not p) (Not q))
+End
+
+Definition Iff_def:
+  Iff p q = And (IMP p q) (IMP q p)
+End
+
+Definition Exists_def:
+  Exists x p = Not (FALL x (Not p))
+End
+
+Definition term_functions_def[simp]:
+  (term_functions (V v) = ∅) ∧
+  (term_functions (Fn f args) =
+     (f, LENGTH args) INSERT LIST_UNION (MAP term_functions args))
+Termination
+  WF_REL_TAC ‘measure term_size’ >> simp[]
+End
+
+Definition form_functions_def[simp]:
+  (form_functions False = ∅) ∧
+  (form_functions (Pred n ts) = LIST_UNION (MAP term_functions ts)) ∧
+  (form_functions (IMP f1 f2) = form_functions f1 ∪ form_functions f2) ∧
+  (form_functions (FALL x f) = form_functions f)
+End
+
+Definition form_predicates[simp]:
+  (form_predicates False = ∅) ∧
+  (form_predicates (Pred n ts) = {(n,LENGTH ts)}) ∧
+  (form_predicates (IMP f1 f2) = form_predicates f1 ∪ form_predicates f2) ∧
+  (form_predicates (FALL x f) = form_predicates f)
+End
+
+Theorem form_functions_Exists[simp]:
+  form_functions (Exists x p) = form_functions p
+Proof
+  simp[Exists_def, Not_def]
+QED
+
+Definition functions_def:
+  functions fms = BIGUNION{form_functions f | f ∈ fms}
+End
+
+Definition predicates_def:
+  predicates fms = BIGUNION {form_predicates f | f ∈ fms}
+End
+
+Definition language_def:
+  language fms = (functions fms, predicates fms)
+End
+
+Theorem functions_SING[simp]:
+  functions {f} = form_functions f
+Proof
+  simp[functions_def, Once EXTENSION]
+QED
+
+Theorem language_SING:
+  language {p} = (form_functions p, form_predicates p)
+Proof
+  simp[functions_def, language_def, predicates_def] >> simp[Once EXTENSION]
+QED
+
+Definition FV_def[simp]:
+  (FV False = ∅) ∧
+  (FV (Pred _ ts) = LIST_UNION (MAP FVT ts)) ∧
+  (FV (IMP f1 f2) = FV f1 ∪ FV f2) ∧
+  (FV (FALL x f) = FV f DELETE x)
+End
+
+Theorem FV_extras[simp]:
+  (FV True = ∅) ∧
+  (FV (Not p) = FV p) ∧
+  (FV (And p q) = FV p ∪ FV q) ∧
+  (FV (Or p q) = FV p ∪ FV q) ∧
+  (FV (Iff p q) = FV p ∪ FV q) ∧
+  (FV (Exists x p) = FV p DELETE x)
+Proof
+  simp[Exists_def, And_def, Or_def, Iff_def, True_def, Not_def] >>
+  simp[EXTENSION] >> metis_tac[]
+QED
+
+
+Definition BV_def[simp]:
+  (BV False = ∅) ∧
+  (BV (Pred _ _) = ∅) ∧
+  (BV (IMP f1 f2) = BV f1 ∪ BV f2) ∧
+  (BV (FALL x f) = x INSERT BV f)
+End
+
+Theorem FV_FINITE[simp]:
+  ∀f. FINITE (FV f)
+Proof
+  Induct >> simp[MEM_MAP,PULL_EXISTS]
+QED
+
+Theorem BV_FINITE[simp]:
+  ∀f. FINITE (BV f)
+Proof
+  Induct >> simp[]
+QED
+
+Definition VARIANT_def :
+  VARIANT s = MAX_SET s + 1
+End
+
+Theorem VARIANT_FINITE:
+  ∀s. FINITE s ⇒ VARIANT s ∉ s
+Proof
+  simp[VARIANT_def] >> rpt strip_tac >> drule_all in_max_set >> simp[]
+QED
+
+Theorem VARIANT_THM[simp]:
+  VARIANT (FV t) ∉ FV t
+Proof
+  simp[VARIANT_FINITE]
+QED
+
+Definition formsubst_def[simp]:
+  (formsubst v False = False) ∧
+  (formsubst v (Pred p l) = Pred p (MAP (termsubst v) l)) ∧
+  (formsubst v (IMP f1 f2) = IMP (formsubst v f1) (formsubst v f2)) ∧
+  (formsubst v (FALL u f) =
+     let v' = v⦇ u ↦ V u ⦈ ;
+         z  = if ∃y. y ∈ FV (FALL u f) ∧ u ∈ FVT (v' y) then
+                VARIANT (FV (formsubst v' f))
+              else u
+     in
+       FALL z (formsubst v⦇ u ↦ V z ⦈ f))
+End
+
+Theorem formsubst_triv[simp]:
+  formsubst V p = p
+Proof
+  Induct_on ‘p’ >> simp[Cong MAP_CONG', combinTheory.APPLY_UPDATE_ID]
+QED
+
+Theorem formsubst_valuation:
+  ∀v1 v2. (∀x. x ∈ FV p ⇒ (v1 x = v2 x)) ⇒ (formsubst v1 p = formsubst v2 p)
+Proof
+  Induct_on ‘p’ >> simp[MEM_MAP, PULL_EXISTS, Cong MAP_CONG']
+  >- (rw[] >> irule MAP_CONG' >> simp[] >> metis_tac[termsubst_valuation]) >>
+  csimp[combinTheory.UPDATE_APPLY] >> rpt gen_tac >> strip_tac >>
+  reverse COND_CASES_TAC >> simp[]
+  >- (first_x_assum irule >> simp[combinTheory.APPLY_UPDATE_THM]) >>
+  rename [‘VARIANT (FV (formsubst v1⦇ k ↦ V k⦈ form))’] >>
+  ‘formsubst v1⦇k ↦ V k⦈ form = formsubst v2⦇k ↦ V k⦈ form’
+    by (first_x_assum irule >> simp[combinTheory.APPLY_UPDATE_THM]) >>
+  simp[] >>
+  first_x_assum irule >> simp[combinTheory.APPLY_UPDATE_THM]
+QED
+
+Theorem formsubst_FV :
+  ∀i. FV (formsubst i p) = { x | ∃y. y ∈ FV p ∧ x ∈ FVT (i y) }
+Proof
+  Induct_on ‘p’ >>
+  simp[MEM_MAP, PULL_EXISTS, MAP_MAP_o, Cong MAP_CONG', termsubst_fvt]
+  >- (simp[Once EXTENSION, MEM_MAP, PULL_EXISTS] >> metis_tac[])
+  >- (simp[Once EXTENSION] >> metis_tac[]) >>
+  csimp[combinTheory.UPDATE_APPLY] >> rpt gen_tac >>
+  reverse COND_CASES_TAC
+  >- (simp[Once EXTENSION] >> fs[] >>
+      simp[combinTheory.APPLY_UPDATE_THM] >> qx_gen_tac ‘u’ >> eq_tac >>
+      simp[PULL_EXISTS] >> qx_gen_tac ‘v’ >- (rw[] >> metis_tac[]) >>
+      metis_tac[]) >>
+  simp[Once EXTENSION, EQ_IMP_THM, PULL_EXISTS, FORALL_AND_THM] >>
+  qmatch_goalsub_abbrev_tac ‘i ⦇ n ↦ V var⦈’ >> rw[]
+  >- (rename [‘x ∈ FVT (i ⦇ n ↦ V var ⦈ y)’] >>
+      ‘y ≠ n’ by (strip_tac >> fs[combinTheory.UPDATE_APPLY]) >>
+      fs[combinTheory.UPDATE_APPLY] >> metis_tac[]) >>
+  asm_simp_tac (srw_ss() ++ boolSimps.CONJ_ss ++ boolSimps.COND_elim_ss)
+               [combinTheory.APPLY_UPDATE_THM] >>
+  simp[GSYM PULL_EXISTS] >> conj_tac >- metis_tac[] >>
+  simp[Abbr‘var’] >>
+  last_assum (fn th => REWRITE_TAC [GSYM th]) >>
+  qmatch_abbrev_tac‘x <> VARIANT (FV f)’ >>
+  ‘x ∈ FV f’ suffices_by metis_tac[VARIANT_THM] >>
+  simp[Abbr‘f’] >> metis_tac[combinTheory.APPLY_UPDATE_THM]
+QED
+
+Theorem VARIANT_NOTIN_SUBSET:
+  FINITE s ∧ t ⊆ s ⇒ VARIANT s ∉ t
+Proof
+  simp[VARIANT_def] >> strip_tac >> DEEP_INTRO_TAC MAX_SET_ELIM >> simp[] >>
+  rw[] >> fs[] >> metis_tac [DECIDE “~(x + 1 ≤ x)”, SUBSET_DEF]
+QED
+
+Theorem formsubst_rename:
+  FV (formsubst V⦇ x ↦ V y⦈ p) DELETE y = (FV p DELETE x) DELETE y
+Proof
+  simp_tac (srw_ss() ++ boolSimps.COND_elim_ss ++ boolSimps.CONJ_ss)
+    [formsubst_FV, EXTENSION, combinTheory.APPLY_UPDATE_THM] >>
+  metis_tac[]
+QED
+
+Theorem term_functions_termsubst:
+  ∀t i. term_functions (termsubst i t) =
+        term_functions t ∪ { x | ∃y. y ∈ FVT t ∧ x ∈ term_functions (i y) }
+Proof
+  ho_match_mp_tac term_induct >>
+  simp[MAP_MAP_o, combinTheory.o_ABS_R, MEM_MAP, PULL_EXISTS, Cong MAP_CONG'] >>
+  rpt strip_tac >> simp[Once EXTENSION] >> simp[MEM_MAP, PULL_EXISTS] >>
+  metis_tac[]
+QED
+
+Theorem form_functions_formsubst:
+  ∀i. form_functions (formsubst i p) =
+      form_functions p ∪ { x | ∃y. y ∈ FV p ∧ x ∈ term_functions (i y) }
+Proof
+  Induct_on ‘p’ >>
+  simp[MAP_MAP_o, combinTheory.o_ABS_R, Cong MAP_CONG',
+       term_functions_termsubst, MEM_MAP, PULL_EXISTS]
+  >- (simp[Once EXTENSION,MEM_MAP, PULL_EXISTS] >> metis_tac[])
+  >- (simp[Once EXTENSION] >> metis_tac[])
+  >- (csimp[combinTheory.APPLY_UPDATE_THM] >>
+      simp_tac (srw_ss() ++ boolSimps.COND_elim_ss ++ boolSimps.CONJ_ss) [] >>
+      simp[Once EXTENSION] >> metis_tac[])
+QED
+
+
+Theorem form_functions_formsubst1[simp]:
+  x ∈ FV p ⇒
+  (form_functions (formsubst V⦇ x ↦ t ⦈ p) =
+   form_functions p ∪ term_functions t)
+Proof
+  simp_tac(srw_ss() ++ boolSimps.CONJ_ss ++ boolSimps.COND_elim_ss)
+    [combinTheory.APPLY_UPDATE_THM,form_functions_formsubst,
+     term_functions_termsubst]
+QED
+
+Theorem form_predicates_formsubst[simp]:
+  ∀i. form_predicates (formsubst i p) = form_predicates p
+Proof   Induct_on ‘p’ >> simp[]
+QED
+
+Theorem formsubst_14b[simp]:
+  x ∉ FV p ⇒ (formsubst V⦇ x ↦ t ⦈ p = p)
+Proof
+  strip_tac >>
+  ‘formsubst V⦇x ↦ t⦈ p = formsubst V p’ suffices_by simp[] >>
+  irule formsubst_valuation >>
+  asm_simp_tac(srw_ss() ++ boolSimps.COND_elim_ss ++ boolSimps.CONJ_ss)
+    [combinTheory.APPLY_UPDATE_THM]
+QED
+
+Theorem formsubst_language_rename:
+  language {formsubst V⦇ x ↦ V y ⦈ p} = language {p}
+Proof
+  simp[language_SING] >> Cases_on ‘x ∈ FV p’ >> simp[]
+QED
+
+(* TODO: show formulas are countable set *)
+
+val _ = export_theory();
diff --git a/examples/logic/folcompactness/folModelsScript.sml b/examples/logic/folcompactness/folModelsScript.sml
new file mode 100644
index 0000000000..77f91028b6
--- /dev/null
+++ b/examples/logic/folcompactness/folModelsScript.sml
@@ -0,0 +1,269 @@
+open HolKernel Parse boolLib bossLib;
+
+open listTheory pred_setTheory
+open folLangTheory
+
+val _ = new_theory "folModels";
+
+val MAP_CONG' = REWRITE_RULE [GSYM AND_IMP_INTRO] MAP_CONG
+
+val _ = Datatype‘
+  model = <| Dom : α set ; Fun : num -> α list -> α ;
+             Pred : num -> α list -> bool |>
+’;
+
+Definition valuation_def:
+  valuation M v ⇔ ∀n. v n ∈ M.Dom
+End
+
+Theorem upd_valuation[simp]:
+  valuation M v ∧ a ∈ M.Dom ⇒ valuation M v⦇x ↦ a⦈
+Proof
+  simp[valuation_def, combinTheory.APPLY_UPDATE_THM] >> rw[] >> rw[]
+QED
+
+Definition termval_def[simp]:
+  (termval M v (V x) = v x) ∧
+  (termval M v (Fn f l) = M.Fun f (MAP (termval M v) l))
+Termination
+  WF_REL_TAC ‘measure (term_size o SND o SND)’ >> simp[]
+End
+
+Definition holds_def:
+  (holds M v False ⇔ F) ∧
+  (holds M v (Pred a l) ⇔ M.Pred a (MAP (termval M v) l)) ∧
+  (holds M v (IMP f1 f2) ⇔ (holds M v f1 ⇒ holds M v f2)) ∧
+  (holds M v (FALL x f) ⇔ ∀a. a ∈ M.Dom ⇒ holds M v⦇x ↦ a⦈ f)
+End
+
+Definition hold_def:
+  hold M v fms ⇔ ∀p. p ∈ fms ⇒ holds M v p
+End
+
+Definition satisfies_def:
+  (satisfies) M fms ⇔ ∀v p. valuation M v ∧ p ∈ fms ⇒ holds M v p
+End
+
+val _ = set_fixity "satisfies" (Infix(NONASSOC, 450))
+
+Theorem satisfies_SING[simp]:
+  M satisfies {p} ⇔ ∀v. valuation M v ⇒ holds M v p
+Proof
+  simp[satisfies_def]
+QED
+
+Theorem HOLDS[simp]:
+  (holds M v False ⇔ F) ∧
+  (holds M v True ⇔ T) ∧
+  (holds M v (Pred a l) ⇔ M.Pred a (MAP (termval M v) l)) ∧
+  (holds M v (Not p) ⇔ ~holds M v p) ∧
+  (holds M v (Or p q) ⇔ holds M v p ∨ holds M v q) ∧
+  (holds M v (And p q) ⇔ holds M v p ∧ holds M v q) ∧
+  (holds M v (Iff p q) ⇔ (holds M v p ⇔ holds M v q)) ∧
+  (holds M v (IMP p q) ⇔ (holds M v p ⇒ holds M v q)) ∧
+  (holds M v (FALL x p) ⇔ ∀a. a ∈ M.Dom ⇒ holds M v⦇x ↦ a⦈ p) ∧
+  (holds M v (Exists x p) ⇔ ∃a. a ∈ M.Dom ∧ holds M v⦇x ↦ a⦈ p)
+Proof
+  simp[holds_def, True_def, Not_def, Exists_def, Or_def, And_def, Iff_def] >>
+  metis_tac[]
+QED
+
+Theorem termval_valuation:
+  ∀t M v1 v2.
+     (∀x. x ∈ FVT t ⇒ (v1 x = v2 x)) ⇒
+     (termval M v1 t = termval M v2 t)
+Proof
+  ho_match_mp_tac term_induct >> simp[MEM_MAP, PULL_EXISTS] >>
+  rpt strip_tac >> AP_TERM_TAC >>
+  irule MAP_CONG >> simp[] >> rpt strip_tac >> first_x_assum irule >>
+  metis_tac[]
+QED
+
+Theorem holds_valuation:
+  ∀M p v1 v2.
+     (∀x. x ∈ FV p ⇒ (v1 x = v2 x)) ⇒
+     (holds M v1 p ⇔ holds M v2 p)
+Proof
+  Induct_on ‘p’ >> simp[MEM_MAP, PULL_EXISTS]
+  >- (rpt strip_tac >> AP_TERM_TAC >> irule MAP_CONG >> simp[] >>
+      rpt strip_tac >> irule termval_valuation >> metis_tac[])
+  >- metis_tac[]
+  >- (rpt strip_tac >> AP_TERM_TAC >> ABS_TAC >> AP_TERM_TAC >>
+      first_x_assum irule >> rpt strip_tac >>
+      rename [‘var ∈ FV fm’, ‘_ ⦇ u ↦ a ⦈’] >>
+      Cases_on ‘var = u’ >> simp[combinTheory.UPDATE_APPLY])
+QED
+
+Definition satisfiable_def:
+  satisfiable (:α) fms ⇔ ∃M:α model. M.Dom ≠ ∅ ∧ M satisfies fms
+End
+
+Definition valid_def:
+  valid (:α) fms ⇔ ∀M:α model. M satisfies fms
+End
+
+Definition entails_def:
+  entails (:α) Γ p ⇔
+    ∀M:α model v. hold M v Γ ⇒ holds M v p
+End
+
+Definition equivalent_def:
+  equivalent (:α) p q ⇔
+    ∀M:α model v. holds M v p ⇔ holds M v q
+End
+
+Definition interpretation_def:
+  interpretation (fns,preds) M ⇔
+    ∀f l. (f, LENGTH l) ∈ fns ∧ (∀x. MEM x l ⇒ x ∈ M.Dom) ⇒
+          M.Fun f l ∈ M.Dom
+End
+
+Theorem interpretation_termval:
+  ∀t M v. interpretation (term_functions t,preds) M ∧ valuation M v ⇒
+          termval M v t ∈ M.Dom
+Proof
+  simp[interpretation_def] >> ho_match_mp_tac term_induct >> rpt strip_tac
+  >- fs[valuation_def] >>
+  fs[MEM_MAP, PULL_EXISTS] >>
+  first_assum irule >> simp[MEM_MAP, PULL_EXISTS] >>
+  rpt strip_tac >> first_x_assum irule >> simp[] >> rpt strip_tac >>
+  last_x_assum irule >> simp[] >> metis_tac[]
+QED
+
+Theorem interpretation_sublang:
+  fns2 ⊆ fns1 ∧ interpretation (fns1,preds) M ⇒ interpretation (fns2,preds) M
+Proof
+  simp[SUBSET_DEF, interpretation_def]
+QED
+
+Theorem termsubst_termval:
+  (M.Fun = Fn) ⇒ ∀t v. termsubst v t = termval M v t
+Proof
+  strip_tac >> ho_match_mp_tac term_induct >> simp[Cong MAP_CONG']
+QED
+
+Theorem termval_triv:
+  (M.Fun = Fn) ⇒ ∀t. termval M V t = t
+Proof
+  strip_tac >> ho_match_mp_tac term_induct >> simp[Cong MAP_CONG']
+QED
+
+Theorem termval_termsubst:
+  ∀t v i. termval M v (termsubst i t) = termval M (termval M v o i) t
+Proof
+  ho_match_mp_tac term_induct >>
+  simp[MAP_MAP_o, combinTheory.o_ABS_R, Cong MAP_CONG']
+QED
+
+Theorem holds_formsubst :
+  ∀v i. holds M v (formsubst i p) ⇔ holds M (termval M v o i) p
+Proof
+  Induct_on ‘p’ >> simp[MAP_MAP_o, termval_termsubst, Cong MAP_CONG'] >>
+  rpt gen_tac >>
+  ho_match_mp_tac
+    (METIS_PROVE [] “
+       (∀a. P a ⇒ (Q a ⇔ R a)) ⇒ ((∀a. P a ⇒ Q a) ⇔ (∀a. P a ⇒ R a))
+     ”) >>
+  qx_gen_tac ‘a’ >> strip_tac >> csimp[combinTheory.UPDATE_APPLY] >>
+  reverse COND_CASES_TAC >> simp[]
+  >- (irule holds_valuation >> rw[] >>
+      simp[combinTheory.APPLY_UPDATE_THM] >> rw[combinTheory.UPDATE_APPLY] >>
+      irule termval_valuation >> metis_tac[combinTheory.APPLY_UPDATE_THM]) >>
+  fs[] >> Q.MATCH_GOALSUB_ABBREV_TAC ‘VARIANT (FV f)’ >>
+  irule holds_valuation >> qx_gen_tac ‘u’ >> strip_tac >> simp[] >>
+  rw[combinTheory.APPLY_UPDATE_THM] >>
+  irule termval_valuation >> qx_gen_tac ‘uu’ >> strip_tac >>
+  rw[combinTheory.APPLY_UPDATE_THM] >>
+  rename [‘VARIANT (FV f) ∈ FVT (i u)’] >>
+  ‘FVT (i u) ⊆ FV f’ suffices_by metis_tac[FV_FINITE, VARIANT_NOTIN_SUBSET] >>
+  simp[formsubst_FV, Abbr‘f’, SUBSET_DEF] >>
+  metis_tac[combinTheory.APPLY_UPDATE_THM]
+QED
+
+Theorem holds_formsubst1:
+  holds M σ (formsubst V⦇ x ↦ t ⦈ p) ⇔ holds M σ⦇ x ↦ termval M σ t⦈ p
+Proof
+  simp[holds_formsubst] >> irule holds_valuation >>
+  rw[combinTheory.APPLY_UPDATE_THM]
+QED
+
+Theorem holds_rename:
+  holds M σ (formsubst V⦇ x ↦ V y ⦈ p) ⇔ holds M σ⦇ x ↦ σ y ⦈ p
+Proof
+  simp[holds_formsubst1]
+QED
+
+Theorem holds_alpha_forall:
+  y ∉ FV (FALL x p) ⇒
+  (holds M v (FALL y (formsubst V⦇ x ↦ V y⦈ p)) ⇔
+   holds M v (FALL x p))
+Proof
+  simp[combinTheory.APPLY_UPDATE_ID, DISJ_IMP_THM, holds_formsubst1,
+       combinTheory.UPDATE_APPLY, combinTheory.UPDATE_EQ] >> strip_tac >>
+  AP_TERM_TAC >> ABS_TAC >> AP_TERM_TAC >>
+  irule holds_valuation >> rpt strip_tac >>
+  rw[combinTheory.APPLY_UPDATE_THM] >> fs[]
+QED
+
+Theorem holds_alpha_exists:
+  y ∉ FV (Exists x p) ⇒
+  (holds M v (Exists y (formsubst V⦇ x ↦ V y⦈ p)) ⇔
+   holds M v (Exists x p))
+Proof
+  simp[combinTheory.APPLY_UPDATE_ID, DISJ_IMP_THM, holds_formsubst1,
+       combinTheory.UPDATE_APPLY, combinTheory.UPDATE_EQ] >> strip_tac >>
+  AP_TERM_TAC >> ABS_TAC >> AP_TERM_TAC >>
+  irule holds_valuation >> rpt strip_tac >>
+  rw[combinTheory.APPLY_UPDATE_THM] >> fs[]
+QED
+
+Theorem termval_functions:
+  ∀t. (∀f zs. (f,LENGTH zs) ∈ term_functions t ⇒ (M.Fun f zs = M'.Fun f zs)) ⇒
+      ∀v. termval M v t = termval M' v t
+Proof
+  ho_match_mp_tac term_induct >>
+  simp[MEM_MAP, PULL_EXISTS, DISJ_IMP_THM, FORALL_AND_THM] >> rw[] >>
+  AP_TERM_TAC >> irule MAP_CONG' >> rw[] >>
+  first_x_assum irule >> metis_tac[]
+QED
+
+Theorem holds_functions:
+  (M2.Dom = M1.Dom) ∧ (∀P zs. M2.Pred P zs ⇔ M1.Pred P zs) ∧
+  (∀f zs. (f,LENGTH zs) ∈ form_functions p ⇒ (M2.Fun f zs = M1.Fun f zs))
+ ⇒
+  ∀v. holds M2 v p ⇔ holds M1 v p
+Proof
+  Induct_on ‘p’ >> simp[MEM_MAP,PULL_EXISTS] >> rw[] >> AP_TERM_TAC >>
+  irule MAP_CONG' >> rw[] >> metis_tac[termval_functions]
+QED
+
+Theorem holds_predicates:
+  (M2.Dom = M1.Dom) ∧ (∀f zs. M2.Fun f zs = M1.Fun f zs) ∧
+  (∀P zs. (P,LENGTH zs) ∈ form_predicates p ⇒ (M2.Pred P zs ⇔ M1.Pred P zs))
+⇒
+  ∀v. holds M2 v p ⇔ holds M1 v p
+Proof
+  Induct_on ‘p’ >> rw[] >> AP_TERM_TAC >> irule MAP_CONG' >> rw[] >>
+  irule termval_functions >> simp[]
+QED
+
+Theorem holds_uclose:
+  (∀v. valuation M v ⇒ holds M v (FALL x p)) ⇔
+  (M.Dom = ∅) ∨ ∀v. valuation M v ⇒ holds M v p
+Proof
+  simp[] >> Cases_on ‘M.Dom = ∅’ >> simp[] >>
+  metis_tac[combinTheory.APPLY_UPDATE_ID, upd_valuation, valuation_def]
+QED
+
+(* ultimate objective:
+Theorem compactness:
+  (∀t. FINITE t ∧ t ⊆ s ⇒
+       ∃M. interpretation (language s) M ∧ M.Dom ≠ ∅ ∧ M satisfies t)
+⇒
+  ∃C. interpretation (language s) C ∧ C.Dom ≠ ∅ ∧ C satisfies s
+Proof
+  cheat
+QED
+*)
+
+val _ = export_theory();
diff --git a/examples/logic/folcompactness/folPrenexScript.sml b/examples/logic/folcompactness/folPrenexScript.sml
new file mode 100644
index 0000000000..8ec60bfd48
--- /dev/null
+++ b/examples/logic/folcompactness/folPrenexScript.sml
@@ -0,0 +1,509 @@
+open HolKernel Parse boolLib bossLib;
+
+open pred_setTheory listTheory
+open boolSimps combinTheory
+open folLangTheory folModelsTheory
+
+val _ = new_theory "folPrenex";
+
+Definition qfree_def:
+  (qfree False ⇔ T) ∧
+  (qfree (Pred _ _) ⇔ T) ∧
+  (qfree (IMP f1 f2) ⇔ qfree f1 ∧ qfree f2) ∧
+  (qfree (FALL _ _) ⇔ F)
+End
+
+Theorem QFREE[simp]:
+  (qfree False ⇔ T) ∧
+  (qfree True ⇔ T) ∧
+  (qfree (Pred n ts) ⇔ T) ∧
+  (qfree (Not p) ⇔ qfree p) ∧
+  (qfree (Or p q) ⇔ qfree p ∧ qfree q) ∧
+  (qfree (And p q) ⇔ qfree p ∧ qfree q) ∧
+  (qfree (Iff p q) ⇔ qfree p ∧ qfree q) ∧
+  (qfree (IMP p q) ⇔ qfree p ∧ qfree q) ∧
+  (qfree (FALL n p) ⇔ F) ∧
+  (qfree (Exists n p) ⇔ F)
+Proof
+  simp[qfree_def, Exists_def, And_def, Or_def, True_def, Not_def, Iff_def] >>
+  metis_tac[]
+QED
+
+Theorem qfree_formsubst[simp]:
+  qfree (formsubst i p) ⇔ qfree p
+Proof
+  Induct_on ‘p’ >> simp[]
+QED
+
+Theorem qfree_bv_empty:
+  qfree p ⇔ (BV p = ∅)
+Proof
+  Induct_on ‘p’ >> simp[]
+QED
+
+val (prenex_rules, prenex_ind, prenex_cases) = Hol_reln‘
+  (∀p. qfree p ⇒ prenex p) ∧
+  (∀x p. prenex p ⇒ prenex (FALL x p)) ∧
+  (∀x p. prenex p ⇒ prenex (Exists x p))
+’;
+
+val (universal_rules, universal_ind, universal_cases) = Hol_reln‘
+  (∀p. qfree p ⇒ universal p) ∧
+  (∀x p. universal p ⇒ universal (FALL x p))
+’;
+
+Theorem prenex_INDUCT_NOT:
+  ∀P. (∀p. qfree p ⇒ P p) ∧
+      (∀x p. P p ⇒ P (FALL x p)) ∧
+      (∀p. P p ⇒ P (Not p))
+    ⇒
+      ∀p. prenex p ⇒ P p
+Proof
+  ntac 2 strip_tac >> Induct_on ‘prenex’ >> simp[Exists_def]
+QED
+
+Theorem Exists_eqns[simp]:
+  Exists x p ≠ Or q r ∧
+  Exists x p ≠ Iff q r ∧
+  Exists x p ≠ And q r ∧
+  Exists x p ≠ FALL y q ∧
+  Exists x p ≠ Pred n ts ∧
+  ((Exists x p = IMP q r) ⇔ (q = FALL x (IMP p False)) ∧ (r = False)) ∧
+  ((Exists x p = Exists y q) ⇔ (x = y) ∧ (p = q))
+Proof
+  simp[And_def, Or_def, Iff_def, Exists_def, Not_def] >> simp[EQ_SYM_EQ]
+QED
+
+Theorem PRENEX[simp]:
+  (prenex False ⇔ T) ∧
+  (prenex True ⇔ T) ∧
+  (prenex (Pred n ts) ⇔ T) ∧
+  (prenex (Not p) ⇔ qfree p ∨ ∃x q. (Not p = Exists x q) ∧ prenex q) ∧
+  (prenex (Or p q) ⇔ qfree p ∧ qfree q) ∧
+  (prenex (And p q) ⇔ qfree p ∧ qfree q) ∧
+  (prenex (IMP p q) ⇔ qfree p ∧ qfree q ∨
+                      ∃x r. (IMP p q = Exists x r) ∧ prenex r) ∧
+  (prenex (Iff p q) ⇔ qfree p ∧ qfree q) ∧
+  (prenex (FALL x p) ⇔ prenex p) ∧
+  (prenex (Exists x p) ⇔ prenex p)
+Proof
+  rpt conj_tac >>
+  simp[SimpLHS, Once prenex_cases] >>
+  simp[And_def, Or_def, Iff_def, Not_def]
+QED
+
+Theorem formsubst_EQ[simp]:
+  (∀i p. (formsubst i p = False) ⇔ (p = False)) ∧
+  (∀i p. (False = formsubst i p) ⇔ (p = False)) ∧
+  (∀i p n ts. (formsubst i p = Pred n ts) ⇔ ∃ts0. (p = Pred n ts0) ∧
+                                       (ts = MAP (termsubst i) ts0)) ∧
+  (∀i p q r. (formsubst i p = IMP q r) ⇔
+             ∃q0 r0. (p = IMP q0 r0) ∧ (q = formsubst i q0) ∧
+                     (r = formsubst i r0)) ∧
+  (∀i p q. (formsubst i p = Not q) ⇔ ∃q0. (p = Not q0) ∧ (q = formsubst i q0))
+Proof
+  csimp[Not_def] >> rw[] >> Cases_on ‘p’ >> simp[EQ_SYM_EQ]
+QED
+
+Theorem formsubst_Not[simp]:
+  formsubst i (Not p) = Not (formsubst i p)
+Proof
+  rw[Not_def]
+QED
+
+Theorem Not_11[simp]:
+  (Not p = Not q) ⇔ (p = q)
+Proof
+  rw[Not_def]
+QED
+
+Theorem formsubst_EQ_FALL:
+  (∃x q. formsubst i p = FALL x q) ⇔ (∃x q. p = FALL x q)
+Proof
+  Cases_on ‘p’ >> simp[]
+QED
+
+Theorem formsubst_EQ_Exists:
+  (∃x q. formsubst i p = Exists x q) ⇔ (∃x q. p = Exists x q)
+Proof
+  Cases_on ‘p’ >> simp[] >>
+  rename [‘subf2 = False’, ‘formsubst i subf1 = FALL _ _’] >>
+  Cases_on ‘subf2 = False’ >> simp[] >>
+  Cases_on ‘subf1’ >> simp[]
+QED
+
+Theorem prenex_formsubst[simp]:
+  prenex (formsubst i p) ⇔ prenex p
+Proof
+  ‘(∀p. prenex p ⇒ ∀i. prenex (formsubst i p)) ∧
+   (∀p. prenex p ⇒ ∀i q. (p = formsubst i q) ⇒ prenex q)’
+    suffices_by metis_tac[] >>
+  conj_tac >> Induct_on ‘prenex’ >> simp[] >> rw[]
+  >- metis_tac[qfree_formsubst, prenex_rules]
+  >- simp[Exists_def]
+  >- metis_tac[qfree_formsubst, prenex_rules]
+  >- (rename [‘FALL n p = formsubst i q’] >>
+      ‘∃m r. q = FALL m r’ by metis_tac[formsubst_EQ_FALL] >> rw[] >> fs[] >>
+      metis_tac[])
+  >- (rename [‘Exists n p = formsubst i q’] >>
+      ‘∃m r. q = Exists m r’ by metis_tac[formsubst_EQ_Exists] >> rw[] >>
+      fs[Exists_def] >> metis_tac[])
+QED
+
+Definition size_def:
+  (size False = 1) ∧
+  (size (Pred _ _) = 1) ∧
+  (size (IMP q r) = 1 + size q + size r) ∧
+  (size (FALL _ q) = 1 + size q)
+End
+
+Theorem SIZE[simp]:
+  (size False = 1) ∧
+  (size True = 3) ∧
+  (size (Pred n ts) = 1) ∧
+  (size (Not p) = 2 + size p) ∧
+  (size (Or p q) = size p + 2 * size q + 2) ∧
+  (size (And p q) = size p + 2 * size q + 10) ∧
+  (size (Iff p q) = 3 * size p + 3 * size q + 13) ∧
+  (size (IMP p q) = size p + size q + 1) ∧
+  (size (FALL x p) = 1 + size p) ∧
+  (size (Exists x p) = 5 + size p)
+Proof
+  simp[And_def, Or_def, Iff_def, size_def, Exists_def, Not_def, True_def]
+QED
+
+Theorem size_formsubst[simp]:
+  ∀i. size (formsubst i p) = size p
+Proof
+  Induct_on ‘p’ >> simp[]
+QED
+
+Definition PPAT_def:
+  PPAT A B C p =
+    case some (x,q). p = Exists x q of
+        SOME (x,q) => B x q
+      | NONE =>
+        case p of
+            FALL x q => A x q
+          | _ => C p
+End
+
+Theorem PPAT[simp]:
+  (PPAT A B C (FALL x p) = A x p) ∧
+  (PPAT A B C (Exists x p) = B x p) ∧
+  ((!x q. p ≠ FALL x q) ∧ (∀x q. p ≠ Exists x q) ⇒ (PPAT A B C p = C p))
+Proof
+  simp[PPAT_def, pairTheory.ELIM_UNCURRY]>>
+  ‘∀a b. (λy. (a:num = FST y) ∧ (b:form = SND y)) = (λp. p = (a,b))’
+     by simp[FUN_EQ_THM, pairTheory.FORALL_PROD, EQ_SYM_EQ] >>
+  simp[] >>
+  Cases_on ‘p’ >> simp[Exists_def]
+QED
+
+Theorem PPAT_CONG[defncong]:
+  ∀A1 A2 B1 B2 C1 C2 q q'.
+    (∀x p. size p < size q ⇒ (A1 x p = A2 x p)) ∧
+    (∀x p. size p < size q ⇒ (B1 x p = B2 x p)) ∧ (∀p. C1 p = C2 p) ∧
+    (q = q') ⇒
+    (PPAT A1 B1 C1 q = PPAT A2 B2 C2 q')
+Proof
+  rw[] >>
+  Cases_on ‘∃n p0. q = Exists n p0’ >> fs[] >>
+  Cases_on ‘q’ >> simp[]
+QED
+
+Definition prenexR_def:
+  prenexR p q =
+    PPAT
+      (λx q0. let y = VARIANT (FV p ∪ FV(FALL x q0))
+              in
+                FALL y (prenexR p (formsubst V⦇x ↦ V y⦈ q0)))
+      (λx q0. let y = VARIANT (FV p ∪ FV(Exists x q0))
+              in
+                Exists y (prenexR p (formsubst V⦇x ↦ V y⦈ q0)))
+      (λq. IMP p q)
+      q
+Termination
+  WF_REL_TAC ‘measure (size o SND)’ >> simp[]
+End
+
+Theorem prenexR_thm[simp]:
+  (prenexR p (FALL x q) = let y = VARIANT (FV p ∪ FV (FALL x q))
+                          in
+                            FALL y (prenexR p (formsubst V⦇x ↦ V y⦈ q))) ∧
+  (prenexR p (Exists x q) = let y = VARIANT (FV p ∪ FV(Exists x q))
+                            in
+                              Exists y (prenexR p (formsubst V⦇x ↦ V y⦈ q))) ∧
+  (qfree q ⇒ (prenexR p q = IMP p q))
+Proof
+  rpt conj_tac >> simp[SimpLHS, Once prenexR_def] >> simp[] >> strip_tac >>
+  ‘(∀x r. q ≠ FALL x r) ∧ (∀x r. q ≠ Exists x r)’
+     by (rpt strip_tac >> fs[]) >>
+  simp[]
+QED
+
+Definition prenexL_def:
+  prenexL p q =
+    PPAT (λx p0. let y = VARIANT (FV (FALL x p0) ∪ FV q)
+                 in
+                   Exists y (prenexL (formsubst V⦇x ↦ V y⦈ p0) q))
+         (λx p0. let y = VARIANT (FV (Exists x p0) ∪ FV q)
+                 in
+                   FALL y (prenexL (formsubst V⦇x ↦ V y⦈ p0) q))
+         (λp. prenexR p q) p
+Termination
+  WF_REL_TAC ‘measure (size o FST)’ >> simp[]
+End
+
+Theorem prenexL_thm[simp]:
+  (prenexL (FALL x p) q = let y = VARIANT (FV (FALL x p) ∪ FV q)
+                          in
+                            Exists y (prenexL (formsubst V⦇x ↦ V y⦈ p) q)) ∧
+  (prenexL (Exists x p) q = let y = VARIANT (FV (Exists x p) ∪ FV q)
+                            in
+                              FALL y (prenexL (formsubst V⦇x ↦ V y⦈ p) q)) ∧
+  (qfree p ⇒ (prenexL p q = prenexR p q))
+Proof
+  rpt conj_tac >> simp[Once prenexL_def, SimpLHS] >> simp[] >> strip_tac >>
+  ‘(∀x r. p ≠ FALL x r) ∧ (∀x r. p ≠ Exists x r)’
+     by (rpt strip_tac >> fs[]) >>
+  simp[]
+QED
+
+Definition Prenex_def[simp]:
+  (Prenex False = False) ∧
+  (Prenex (Pred n ts) = Pred n ts) ∧
+  (Prenex (IMP f1 f2) = prenexL (Prenex f1) (Prenex f2)) ∧
+  (Prenex (FALL x f) = FALL x (Prenex f))
+End
+
+Theorem prenexR_language[simp]:
+  ∀p. language {prenexR p q} = language {IMP p q}
+Proof
+  completeInduct_on ‘size q’ >> fs[PULL_FORALL, language_SING] >> rpt gen_tac >>
+  disch_then SUBST_ALL_TAC >>
+  Cases_on ‘∃x q0. q = Exists x q0’ >> fs[]
+  >- (simp[Exists_def, Not_def, form_functions_formsubst] >>
+      simp_tac (srw_ss() ++ COND_elim_ss) [combinTheory.APPLY_UPDATE_THM]) >>
+  Cases_on ‘∃x q0. q = FALL x q0’ >> fs[]
+  >- simp_tac (srw_ss() ++ COND_elim_ss)
+       [form_functions_formsubst,combinTheory.APPLY_UPDATE_THM] >>
+  conj_tac >> simp[Once prenexR_def]
+QED
+
+Theorem prenexL_language[simp]:
+  ∀q. language {prenexL p q} = language {IMP p q}
+Proof
+  completeInduct_on ‘size p’ >> fs[PULL_FORALL] >> rpt gen_tac >>
+  disch_then SUBST_ALL_TAC >>
+  Cases_on ‘∃x p0. p = Exists x p0’ >> fs[] >> fs[]
+  >- (fs[Exists_def, Not_def, form_functions_formsubst, language_SING] >>
+      simp_tac (srw_ss() ++ COND_elim_ss) [combinTheory.APPLY_UPDATE_THM]) >>
+  Cases_on ‘∃x p0. p = FALL x p0’ >> fs[]
+  >- full_simp_tac (srw_ss() ++ COND_elim_ss)
+       [language_SING,form_functions_formsubst,APPLY_UPDATE_THM,Exists_def,
+        Not_def] >>
+  simp[Once prenexL_def]
+QED
+
+Theorem prenex_lemma_forall:
+  P ∧ (FV f1 = FV f2) ∧ (language {f1} = language {f2}) ∧
+  (∀M:α model v. M.Dom ≠ ∅ ⇒ (holds M v f1 ⇔ holds M v f2)) ⇒
+  P ∧ (FV (FALL z f1) = FV (FALL z f2)) ∧
+  (language {FALL z f1} = language {FALL z f2}) ∧
+  ∀M:α model v. M.Dom ≠ ∅ ⇒ (holds M v (FALL z f1) ⇔ holds M v (FALL z f2))
+Proof
+  rw[language_SING]
+QED
+
+Theorem prenex_lemma_exists:
+  P ∧ (FV f1 = FV f2) ∧ (language {f1} = language {f2}) ∧
+  (∀M:α model v. M.Dom ≠ ∅ ⇒ (holds M v f1 ⇔ holds M v f2)) ⇒
+  P ∧ (FV (Exists z f1) = FV (Exists z f2)) ∧
+  (language {Exists z f1} = language {Exists z f2}) ∧
+  ∀M:α model v. M.Dom ≠ ∅ ⇒ (holds M v (Exists z f1) ⇔ holds M v (Exists z f2))
+Proof
+  rw[language_SING, Exists_def, Not_def]
+QED
+
+Theorem prenex_rename1[simp]:
+  ∀f x y. prenex (formsubst V⦇x ↦ V y⦈ f) ⇔ prenex f
+Proof
+  completeInduct_on ‘size f’ >> fs[PULL_FORALL]
+QED
+
+Theorem tfresh_rename_inverts:
+  ∀t x y. y ∉ FVT t ⇒ (termsubst V⦇y ↦ V x⦈ (termsubst V⦇x ↦ V y⦈ t) = t)
+Proof
+  ho_match_mp_tac term_induct >> simp[] >> rw[MEM_MAP, MAP_MAP_o]
+  >- rw[combinTheory.APPLY_UPDATE_THM] >>
+  irule EQ_TRANS >> qexists_tac ‘MAP I ts’ >> reverse conj_tac
+  >- simp[] >>
+  irule listTheory.MAP_CONG >> simp[] >> qx_gen_tac ‘t0’ >> strip_tac >>
+  first_x_assum irule >> metis_tac[]
+QED
+
+Theorem holds_nonFV:
+  v ∉ FV f ⇒ (holds M i⦇ v ↦ t ⦈ f ⇔ holds M i f)
+Proof
+  strip_tac >> irule holds_valuation >>
+  simp[combinTheory.APPLY_UPDATE_THM] >> rw[] >> fs[]
+QED
+
+Theorem prenexR_FV[simp]:
+  FV (prenexR p q) = FV p ∪ FV q
+Proof
+  completeInduct_on ‘size q’ >> fs[PULL_FORALL] >> rw[] >>
+  Cases_on ‘∃v q0. q = Exists v q0’ >> fs[]
+  >- (simp_tac (srw_ss() ++ COND_elim_ss)
+       [EXTENSION, formsubst_FV, termsubst_fvt, APPLY_UPDATE_THM] >>
+      qmatch_goalsub_abbrev_tac ‘VARIANT s’ >>
+      qabbrev_tac ‘vv = VARIANT s’ >>
+      ‘vv ∉ s’ by simp[Abbr‘vv’, Abbr‘s’, VARIANT_FINITE] >>
+      Q.UNABBREV_TAC ‘s’ >> fs[] >> gen_tac >>
+      eq_tac >> rw[] >> simp[] >> fs[] >> metis_tac[]) >>
+  Cases_on ‘∃v q0. q = FALL v q0’ >> fs[]
+  >- (simp_tac (srw_ss() ++ COND_elim_ss)
+       [EXTENSION, formsubst_FV, termsubst_fvt, APPLY_UPDATE_THM] >>
+      qmatch_goalsub_abbrev_tac ‘VARIANT s’ >>
+      qabbrev_tac ‘vv = VARIANT s’ >>
+      ‘vv ∉ s’ by simp[Abbr‘vv’, Abbr‘s’, VARIANT_FINITE] >>
+      Q.UNABBREV_TAC ‘s’ >> fs[] >> gen_tac >>
+      eq_tac >> rw[] >> simp[] >> fs[] >> metis_tac[]) >>
+  simp[prenexR_def]
+QED
+
+Theorem prenexR_prenex:
+  qfree p ∧ prenex q ⇒ prenex (prenexR p q)
+Proof
+  completeInduct_on ‘size q’ >> fs[PULL_FORALL] >> gen_tac >>
+  disch_then SUBST_ALL_TAC >>
+  simp[Once prenex_cases, SimpLHS] >> dsimp[]
+QED
+
+Theorem prenexR_holds:
+  ∀M v. M.Dom ≠ ∅ ⇒ (holds M v (prenexR p q) ⇔ holds M v (IMP p q))
+Proof
+  completeInduct_on ‘size q’ >> fs[PULL_FORALL] >> rw[] >>
+  Cases_on ‘∃v q0. q = Exists v q0’ >> fs[] >> fs[]
+  >- (qmatch_goalsub_abbrev_tac ‘VARIANT ss’ >>
+      ‘VARIANT ss ∉ ss’ by simp[VARIANT_FINITE, Abbr‘ss’] >>
+      qabbrev_tac ‘vv = VARIANT ss’ >>
+      rename [‘holds M vln⦇ vv ↦ _ ⦈ f1’, ‘formsubst _ f2’] >>
+      ‘vv ∉ FV f1’ by fs[Abbr‘ss’] >>
+      ‘∀t. holds M vln⦇vv ↦ t⦈ f1 ⇔ holds M vln f1’
+          by (gen_tac >> irule holds_valuation >>
+              metis_tac[combinTheory.APPLY_UPDATE_THM]) >>
+      simp[] >> Cases_on ‘holds M vln f1’ >> simp[]
+      >- (AP_TERM_TAC >> ABS_TAC >>
+          rename [‘d ∈ M.Dom’] >> Cases_on ‘d ∈ M.Dom’ >>
+          simp[holds_formsubst] >> irule holds_valuation >>
+          rw[combinTheory.APPLY_UPDATE_THM] >> fs[Abbr‘ss’] >> metis_tac[]) >>
+      metis_tac[MEMBER_NOT_EMPTY]) >>
+  Cases_on ‘∃v q0. q = FALL v q0’ >> fs[] >> fs[]
+  >- (qmatch_goalsub_abbrev_tac ‘VARIANT ss’ >>
+      ‘VARIANT ss ∉ ss’ by simp[VARIANT_FINITE, Abbr‘ss’] >>
+      qabbrev_tac ‘vv = VARIANT ss’ >>
+      rename [‘holds M vln⦇ vv ↦ _ ⦈ f1’, ‘formsubst V⦇v₀ ↦ V vv⦈ f2’] >>
+      ‘vv ∉ FV f1’ by fs[Abbr‘ss’] >>
+      ‘∀d. holds M vln⦇vv ↦ d⦈ f1 ⇔ holds M vln f1’
+        by (gen_tac >> irule holds_valuation >> simp[APPLY_UPDATE_THM] >>
+            metis_tac[]) >>
+      simp[] >> Cases_on ‘holds M vln f1’ >> simp[holds_formsubst] >>
+      AP_TERM_TAC >> ABS_TAC >> rename [‘d ∈ M.Dom’] >> Cases_on ‘d ∈ M.Dom’ >>
+      simp[] >> irule holds_valuation >> simp[APPLY_UPDATE_THM] >>
+      rw[APPLY_UPDATE_THM] >> fs[Abbr‘ss’] >> metis_tac[]) >>
+  simp[Once prenexR_def]
+QED
+
+Theorem prenexL_FV[simp]:
+  FV (prenexL p q) = FV p ∪ FV q
+Proof
+  completeInduct_on ‘size p’ >> fs[PULL_FORALL] >> rw[] >>
+  Cases_on ‘∃v p1. p = Exists v p1’ >> fs[]
+  >- (qmatch_goalsub_abbrev_tac ‘VARIANT ss’ >>
+      ‘VARIANT ss ∉ ss’ by fs[Abbr‘ss’, VARIANT_FINITE] >>
+      simp[formsubst_FV, combinTheory.APPLY_UPDATE_THM] >>
+      simp[EXTENSION] >> qx_gen_tac ‘n’ >> eq_tac >>
+      asm_simp_tac(srw_ss() ++ COND_elim_ss) [] >> rw[]
+      >- simp[Abbr‘ss’]
+      >- simp[Abbr‘ss’]
+      >- (dsimp[] >> fs[Abbr‘ss’])
+      >- metis_tac[]) >>
+  Cases_on ‘∃v p1. p = FALL v p1’ >> fs[]
+  >- (qmatch_goalsub_abbrev_tac ‘VARIANT ss’ >>
+      ‘VARIANT ss ∉ ss’ by fs[Abbr‘ss’, VARIANT_FINITE] >>
+      simp[formsubst_FV, combinTheory.APPLY_UPDATE_THM] >>
+      simp[EXTENSION] >> qx_gen_tac ‘n’ >> eq_tac >>
+      asm_simp_tac(srw_ss() ++ COND_elim_ss) [] >> rw[]
+      >- simp[Abbr‘ss’]
+      >- simp[Abbr‘ss’]
+      >- (dsimp[] >> fs[Abbr‘ss’])
+      >- metis_tac[]) >>
+  simp[prenexL_def]
+QED
+
+Theorem prenexL_prenex[simp]:
+  prenex p ∧ prenex q ⇒ prenex (prenexL p q)
+Proof
+  completeInduct_on ‘size p’ >> fs[PULL_FORALL] >> rw[] >>
+  Cases_on ‘∃v p0. p = Exists v p0’ >> fs[] >>
+  Cases_on ‘∃v p0. p = FALL v p0’ >> fs[] >> fs[] >>
+  simp[prenexL_def] >>
+  ‘qfree p’ suffices_by metis_tac[prenexR_prenex] >>
+  Q.UNDISCH_THEN ‘prenex p’ mp_tac >> simp[Once prenex_cases]
+QED
+
+Theorem prenexL_holds[simp]:
+   ∀M vln. M.Dom ≠ ∅ ⇒ (holds M vln (prenexL p q) ⇔ holds M vln (IMP p q))
+Proof
+  completeInduct_on ‘size p’ >> fs[PULL_FORALL] >> rw[] >>
+  Cases_on ‘∃v p0. p = Exists v p0’ >> fs[]
+  >- (qmatch_goalsub_abbrev_tac ‘VARIANT ss’ >>
+      ‘VARIANT ss ∉ ss’ by simp[VARIANT_FINITE, Abbr‘ss’] >>
+      ‘∀d. holds M vln⦇ VARIANT ss ↦ d⦈ q ⇔ holds M vln q’
+        by (gen_tac >> irule holds_valuation >> rw[APPLY_UPDATE_THM] >>
+            fs[Abbr‘ss’]) >> simp[PULL_EXISTS] >>
+      AP_TERM_TAC >> ABS_TAC >> rename [‘d ∈ M.Dom’] >> Cases_on ‘d ∈ M.Dom’ >>
+      simp[] >> AP_THM_TAC >> AP_TERM_TAC >>
+      simp[holds_formsubst] >> irule holds_valuation >> rw[APPLY_UPDATE_THM] >>
+      fs[Abbr‘ss’] >> metis_tac[]) >>
+  Cases_on ‘∃v p0. p = FALL v p0’ >> fs[]
+  >- (qmatch_goalsub_abbrev_tac ‘VARIANT ss’ >>
+      ‘VARIANT ss ∉ ss’ by simp[VARIANT_FINITE, Abbr‘ss’] >>
+      simp[GSYM LEFT_EXISTS_IMP_THM] >>
+      ‘∀d. holds M vln⦇ VARIANT ss ↦ d ⦈ q ⇔ holds M vln q’
+        by (gen_tac >> irule holds_nonFV >> fs[Abbr‘ss’]) >>
+      simp[] >> Cases_on ‘holds M vln q’ >> simp[]
+      >- metis_tac[MEMBER_NOT_EMPTY] >>
+      AP_TERM_TAC >> ABS_TAC >> rename [‘d ∈ M.Dom’] >> Cases_on ‘d ∈ M.Dom’ >>
+      simp[] >> simp[holds_formsubst] >> irule holds_valuation >>
+      rw[APPLY_UPDATE_THM] >> fs[Abbr‘ss’] >> metis_tac[]) >>
+  simp[Once prenexL_def, prenexR_holds]
+QED
+
+Theorem prenex_Prenex[simp]:
+  prenex (Prenex f)
+Proof
+  Induct_on ‘f’ >> simp[]
+QED
+
+Theorem FV_Prenex[simp]:
+  FV (Prenex f) = FV f
+Proof
+  Induct_on ‘f’ >> simp[]
+QED
+
+Theorem holds_Prenex[simp]:
+  ∀vln. M.Dom ≠ ∅ ⇒ (holds M vln (Prenex f) ⇔ holds M vln f)
+Proof
+  Induct_on ‘f’ >> simp[prenexL_holds]
+QED
+
+Theorem language_Prenex[simp]:
+  language {Prenex f} = language {f}
+Proof
+  Induct_on ‘f’ >> simp[] >> fs[language_SING]
+QED
+
+val _ = export_theory();
diff --git a/examples/logic/folcompactness/folSkolemScript.sml b/examples/logic/folcompactness/folSkolemScript.sml
new file mode 100644
index 0000000000..8852ae13a6
--- /dev/null
+++ b/examples/logic/folcompactness/folSkolemScript.sml
@@ -0,0 +1,265 @@
+open HolKernel Parse boolLib bossLib;
+
+open boolSimps pred_setTheory listTheory
+open folPrenexTheory folModelsTheory folLangTheory
+
+val _ = new_theory "folSkolem";
+
+Theorem holds_exists_lemma:
+  ∀p t x M v preds.
+     interpretation (term_functions t, preds) M ∧
+     valuation M v ∧
+     holds M v (formsubst V⦇x ↦ t⦈ p)
+    ⇒
+     holds M v (Exists x p)
+Proof
+  rw[holds_formsubst1] >> metis_tac[interpretation_termval]
+QED
+
+Definition Skolem1_def:
+  Skolem1 f x p =
+    formsubst V⦇ x ↦ Fn f (MAP V (SET_TO_LIST (FV (Exists x p))))⦈ p
+End
+
+Theorem FV_Skolem1[simp]:
+  FV (Skolem1 f x p) = FV (Exists x p)
+Proof
+  simp[Skolem1_def, formsubst_FV, combinTheory.APPLY_UPDATE_THM, EXTENSION,
+       EQ_IMP_THM, FORALL_AND_THM, PULL_EXISTS] >>
+  simp_tac (srw_ss() ++ COND_elim_ss ++ DNF_ss) [EXISTS_OR_THM, MEM_MAP]
+QED
+
+Theorem size_Skolem1[simp]:
+  size (Skolem1 f x p) < size (Exists x p)
+Proof
+  simp[Skolem1_def]
+QED
+
+Theorem prenex_Skolem1[simp]:
+  prenex (Skolem1 f x p) ⇔ prenex p
+Proof
+  simp[Skolem1_def]
+QED
+
+Theorem form_predicates_Skolem1[simp]:
+  form_predicates (Skolem1 f x p) = form_predicates p
+Proof
+  simp[Skolem1_def]
+QED
+
+Theorem LIST_UNION_MAP_KEMPTY[simp]:
+  LIST_UNION (MAP (λa. ∅) l) = ∅ ∧
+  LIST_UNION (MAP (K ∅) l) = ∅
+Proof
+  Induct_on ‘l’ >> simp[]
+QED
+
+Theorem form_functions_Skolem1[simp]:
+  form_functions (Skolem1 f x p) ⊆
+    (f, CARD (FV (Exists x p))) INSERT form_functions p ∧
+  form_functions p ⊆ form_functions (Skolem1 f x p)
+Proof
+  simp[Skolem1_def] >> Cases_on ‘x ∈ FV p’
+  >- (simp[form_functions_formsubst1, MAP_MAP_o, combinTheory.o_ABS_L,
+           SET_TO_LIST_CARD] >>
+      simp[SUBSET_DEF]) >>
+  simp[SUBSET_DEF]
+QED
+
+Theorem Skolem1_ID[simp]:
+  x ∉ FV p ⇒ Skolem1 f x p = p
+Proof
+  simp[Skolem1_def]
+QED
+
+Theorem holds_exists_holds_skolem1:
+  (f,CARD (FV (Exists x p))) ∉ form_functions (Exists x p)
+ ⇒
+  ∀M. interpretation (language {p}) M ∧ M.Dom ≠ ∅ ∧
+      (∀v. valuation M v ⇒ holds M v (Exists x p))
+   ⇒
+      ∃M'. M'.Dom = M.Dom ∧ M'.Pred = M.Pred ∧
+           (∀g zs. g ≠ f ∨ LENGTH zs ≠ CARD (FV (Exists x p)) ⇒
+                   M'.Fun g zs = M.Fun g zs) ∧
+           interpretation (language {Skolem1 f x p}) M' ∧
+           ∀v. valuation M' v ⇒ holds M' v (Skolem1 f x p)
+Proof
+  reverse (Cases_on ‘x ∈ FV p’)
+  >- (simp[holds_nonFV] >> metis_tac[]) >>
+  qabbrev_tac ‘FF = FV (Exists x p)’ >> simp[Skolem1_def] >>
+  qabbrev_tac ‘ft = Fn f (MAP V (SET_TO_LIST FF))’ >> rw[] >>
+  qexists_tac ‘<|
+    Dom := M.Dom ; Pred := M.Pred ;
+    Fun := M.Fun ⦇ f ↦
+                   λargs. if LENGTH args = CARD FF then
+                             @a. a ∈ M.Dom ∧
+                                 holds M (FOLDR (λ(k,v) f. f ⦇ k ↦ v ⦈)
+                                             (λz. @c. c ∈ M.Dom)
+                                             (ZIP(SET_TO_LIST FF, args)))
+                                         ⦇ x ↦ a ⦈
+                                         p
+                          else M.Fun f args ⦈
+  |>’ >> simp[] >> rw[]
+  >- simp[combinTheory.APPLY_UPDATE_THM]
+  >- rw[combinTheory.APPLY_UPDATE_THM]
+  >- (fs[interpretation_def, language_def] >>
+      rw[combinTheory.APPLY_UPDATE_THM]
+      >- (rename [‘(f,LENGTH l) ∈ form_functions p’] >> metis_tac[])
+      >- (rename [‘(f,LENGTH l) ∈ term_functions ft’] >>
+          ‘FINITE FF’ by simp[Abbr‘FF’]>>
+          reverse (fs[Abbr‘ft’, MAP_MAP_o, MEM_MAP, SET_TO_LIST_CARD])
+          >- (rw[] >> fs[]) >>
+          SELECT_ELIM_TAC >> simp[] >>
+          first_x_assum irule >> simp[valuation_def] >>
+          ‘∀(vars:num list) (vals:α list) n.
+             (∀v. MEM v vals ⇒ v ∈ M.Dom) ∧ LENGTH vars = LENGTH vals ⇒
+             FOLDR (λ(k,v) f. f ⦇k ↦ v⦈) (λz. @c. c ∈ M.Dom)
+                   (ZIP (vars, vals)) n ∈ M.Dom’
+            suffices_by metis_tac[SET_TO_LIST_CARD] >>
+          Induct >> simp[]
+          >- (SELECT_ELIM_TAC >> fs[EXTENSION] >> metis_tac[]) >>
+          Cases_on ‘vals’ >>
+          simp[DISJ_IMP_THM, FORALL_AND_THM, combinTheory.APPLY_UPDATE_THM] >>
+          rw[])
+      >- (rename [‘f ≠ g’, ‘(g,LENGTH l) ∈ form_functions p’] >> metis_tac[]) >>
+      rename [‘f ≠ g’, ‘(g,LENGTH l) ∈ term_functions ft’] >>
+      fs[Abbr‘ft’, MEM_MAP, SET_TO_LIST_CARD] >> rw[] >> fs[]) >>
+  qmatch_abbrev_tac ‘holds <| Dom := M.Dom; Fun := CF; Pred := M.Pred |> _ _’ >>
+  simp[holds_formsubst1, Abbr‘ft’, MAP_MAP_o, combinTheory.o_ABS_L] >>
+  irule (holds_functions
+           |> CONV_RULE (RAND_CONV (REWRITE_CONV [EQ_IMP_THM]))
+           |> UNDISCH |> Q.SPEC ‘v’ |> CONJUNCT2 |> Q.GEN ‘v’ |> DISCH_ALL) >>
+  qexists_tac ‘M’ >> simp[] >> conj_tac
+  >- (rw[Abbr‘CF’, combinTheory.APPLY_UPDATE_THM] >> metis_tac[]) >>
+  ‘FINITE FF’ by simp[Abbr‘FF’] >>
+  simp[Abbr‘CF’, SET_TO_LIST_CARD, combinTheory.APPLY_UPDATE_THM] >>
+  SELECT_ELIM_TAC >> conj_tac
+  >- (first_x_assum irule >> fs[valuation_def] >>
+      ‘∀l. (∀n. v n ∈ M.Dom) ⇒
+           ∀n. FOLDR (λ(k,v) f. f ⦇ k ↦ v ⦈) (λz. @c. c ∈ M.Dom)
+                     (ZIP (l,MAP (λa. v a) l)) n ∈ M.Dom’
+        suffices_by metis_tac[] >> Induct >> simp[]
+      >- (SELECT_ELIM_TAC >> fs[EXTENSION] >>metis_tac[]) >>
+      rfs[combinTheory.APPLY_UPDATE_THM] >> rw[]) >>
+  qx_gen_tac ‘a’ >>
+  qmatch_abbrev_tac ‘a ∈ M.Dom ∧ holds M vv⦇ x ↦ a ⦈ p ⇒ holds M v⦇ x ↦ a ⦈ p’>>
+  fs[valuation_def] >> strip_tac >>
+  ‘∀var. var ∈ FV p ⇒ vv⦇ x ↦ a ⦈ var = v⦇ x ↦ a ⦈ var’
+    suffices_by metis_tac[holds_valuation] >>
+  rw[combinTheory.APPLY_UPDATE_THM] >> simp[Abbr‘vv’] >>
+  ‘∀vars (var:num).
+     MEM var vars ∧ ALL_DISTINCT vars ⇒
+     FOLDR (λ(k,v) f. f ⦇ k ↦ v ⦈) (λz. @c. c ∈ M.Dom)
+           (ZIP (vars,MAP (λa. v a) vars)) var = v var’
+    suffices_by (disch_then irule >> simp[] >> simp[Abbr‘FF’]) >>
+  Induct >> simp[] >> rw[combinTheory.APPLY_UPDATE_THM]
+QED
+
+Theorem Skolem1_holds_Exists_holds:
+  (f,CARD (FV (Exists x p))) ∉ form_functions (Exists x p) ⇒
+  ∀N. interpretation (language {Skolem1 f x p}) N ∧ N.Dom ≠ ∅
+     ⇒
+      ∀v. valuation N v ∧ holds N v (Skolem1 f x p) ⇒ holds N v (Exists x p)
+Proof
+  reverse (Cases_on ‘x ∈ FV p’)
+  >- (simp[holds_nonFV, EXTENSION] >> metis_tac[]) >>
+  qabbrev_tac ‘FF = FV (Exists x p)’ >> simp[Skolem1_def] >>
+  qabbrev_tac ‘ft = Fn f (MAP V (SET_TO_LIST FF))’ >>
+  ‘FINITE FF’ by simp[Abbr‘FF’] >>
+  simp[holds_formsubst1] >> rw[] >>
+  ‘termval N v ft ∈ N.Dom’ suffices_by metis_tac[] >>
+  simp[Abbr‘ft’, MAP_MAP_o, combinTheory.o_ABS_L] >>
+  rfs[interpretation_def, language_def, form_functions_formsubst1,
+      MEM_MAP, MAP_MAP_o, PULL_EXISTS, DISJ_IMP_THM, FORALL_AND_THM,
+      RIGHT_AND_OVER_OR] >>
+  first_x_assum
+    (fn th => irule th >>
+              fs[MEM_MAP, PULL_EXISTS, SET_TO_LIST_CARD, valuation_def] >>
+              NO_TAC)
+QED
+
+(* ------------------------------------------------------------------------- *)
+(* Multiple Skolemization of a prenex formula.                               *)
+(* ------------------------------------------------------------------------- *)
+
+Definition Skolems_def:
+  Skolems J r k =
+    PPAT (λx q. FALL x (Skolems J q k))
+         (λx q. Skolems J (Skolem1 (J *, k) x q) (k + 1))
+         (λp. p) r
+Termination
+  WF_REL_TAC ‘measure (λ(a,b,c). size b)’ >> simp[] >>
+  simp[Skolem1_def]
+End
+
+Theorem prenex_Skolems_universal[simp]:
+  ∀J p k. prenex p ⇒ universal (Skolems J p k)
+Proof
+  ho_match_mp_tac Skolems_ind >> rw[] >>
+  Cases_on ‘∃x p0. p = Exists x p0’ >> fs[]
+  >- (simp[Once Skolems_def] >> first_x_assum irule >> fs[]) >>
+  Cases_on ‘∃x p0. p = FALL x p0’ >> fs[]
+  >- (simp[Once Skolems_def] >> fs[universal_rules]) >>
+  simp[Once Skolems_def] >>
+  simp[Once universal_cases] >> metis_tac[prenex_cases]
+QED
+
+Theorem FV_Skolems[simp]:
+  ∀J p k. FV (Skolems J p k) = FV p
+Proof
+  ho_match_mp_tac Skolems_ind >> rw[] >>
+  Cases_on ‘∃x p0. p = Exists x p0’ >> fs[] >- simp[Once Skolems_def] >>
+  Cases_on ‘∃x p0. p = FALL x p0’ >> fs[] >- simp[Once Skolems_def] >>
+  simp[Once Skolems_def]
+QED
+
+Theorem form_predicates_Skolems[simp]:
+  ∀J p k. form_predicates (Skolems J p k) = form_predicates p
+Proof
+  ho_match_mp_tac Skolems_ind >> rw[] >>
+  Cases_on ‘∃x p0. p = Exists x p0’ >> fs[]
+  >- (simp[Once Skolems_def] >> simp[Exists_def, Not_def]) >>
+  Cases_on ‘∃x p0. p = FALL x p0’ >> fs[] >- simp[Once Skolems_def] >>
+  simp[Once Skolems_def]
+QED
+
+Theorem form_functions_Skolems_up:
+  ∀J p k.
+    form_functions (Skolems J p k) ⊆
+      {(J ⊗ l, m) | l, m | k ≤ l} ∪ form_functions p
+Proof
+  ho_match_mp_tac Skolems_ind >> rw[] >>
+  Cases_on ‘∃x p0. p = Exists x p0’ >> fs[]
+  >- (simp[Once Skolems_def] >> fs[] >>
+      first_x_assum (qspecl_then [‘p0’, ‘x’] mp_tac) >> simp[] >>
+      simp[SUBSET_DEF] >> rw[] >> first_x_assum drule >> rw[] >>
+      mp_tac (form_functions_Skolem1 |> CONJUNCT1 |> GEN_ALL) >>
+      REWRITE_TAC[SUBSET_DEF] >> rw[] >>
+      pop_assum (drule_then strip_assume_tac) >> rw[]) >>
+  Cases_on ‘∃x p0. p = FALL x p0’ >> fs[] >- simp[Once Skolems_def] >>
+  simp[Once Skolems_def]
+QED
+
+Theorem form_functions_Skolems_down:
+  ∀J p k.
+    form_functions p ⊆ form_functions (Skolems J p k)
+Proof
+  ho_match_mp_tac Skolems_ind >> rw[] >>
+  Cases_on ‘∃x p0. p = Exists x p0’ >> fs[]
+  >- (simp[Once Skolems_def] >> fs[] >>
+      first_x_assum (qspecl_then [‘p0’, ‘x’] mp_tac) >> simp[] >>
+      simp[SUBSET_DEF] >> rw[] >> first_x_assum irule >> rw[] >>
+      metis_tac[SUBSET_DEF, form_functions_Skolem1]) >>
+  Cases_on ‘∃x p0. p = FALL x p0’ >> fs[] >- simp[Once Skolems_def] >>
+  simp[Once Skolems_def]
+QED
+
+
+
+
+
+
+
+
+
+val _ = export_theory();