diff --git a/thys/Q0_Soundness/HOLZF_Set_Theory.thy b/thys/Q0_Soundness/HOLZF_Set_Theory.thy
new file mode 100644
--- /dev/null
+++ b/thys/Q0_Soundness/HOLZF_Set_Theory.thy
@@ -0,0 +1,8 @@
+section \<open>Isabelle/HOLZF lives up to CakeML's set theory specification\<close>
+
+theory HOLZF_Set_Theory imports "HOL-ZF.MainZF" Set_Theory begin
+
+interpretation set_theory Elem Sep Power Sum Upair
+  using Ext Sep Power subset_def Sum Upair by unfold_locales auto
+
+end
diff --git a/thys/Q0_Soundness/Q0.thy b/thys/Q0_Soundness/Q0.thy
new file mode 100644
--- /dev/null
+++ b/thys/Q0_Soundness/Q0.thy
@@ -0,0 +1,2414 @@
+section \<open>Q0 abbreviations\<close>
+
+theory Q0
+  imports Set_Theory 
+  abbrevs "App" = "\<^bold>\<cdot>"
+    and "Abs" = "\<^bold>[\<^bold>\<lambda>_:_. _\<^bold>]"
+    and "Eql" = "\<^bold>[_ \<^bold>=_\<^bold>= _\<^bold>]"
+    and "Con" = "\<^bold>\<and>"
+    and "Forall" = "\<^bold>[\<^bold>\<forall>_:_. _\<^bold>]"
+    and "Imp" = "\<^bold>\<longrightarrow>"
+    and "Fun" = "\<^bold>\<Leftarrow>"
+begin
+
+lemma arg_cong3: "a = b \<Longrightarrow> c = d \<Longrightarrow> e = f \<Longrightarrow> h a c e = h b d f"
+  by auto
+
+
+section \<open>Syntax and typing\<close>
+
+datatype type_sym =
+  Ind | 
+  Tv |
+  Fun type_sym type_sym (infixl "\<^bold>\<Leftarrow>" 80)
+
+type_synonym var_sym = string
+type_synonym cst_sym = string
+
+datatype trm =
+  Var var_sym type_sym |
+  Cst cst_sym type_sym |
+  App trm trm (infixl "\<^bold>\<cdot>" 80) |
+  Abs var_sym type_sym trm ("\<^bold>[\<^bold>\<lambda>_:_. _\<^bold>]" [80,80,80])
+
+fun vars :: "trm \<Rightarrow> (var_sym * type_sym) set" where
+  "vars (Var x \<alpha>) = {(x,\<alpha>)}"
+| "vars (Cst _ _) = {}"
+| "vars (A \<^bold>\<cdot> B) = vars A \<union> vars B"
+| "vars (\<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>]) = {(x,\<alpha>)} \<union> vars A"
+
+fun frees :: "trm \<Rightarrow> (var_sym * type_sym) set" where
+  "frees (Var x \<alpha>) = {(x,\<alpha>)}"
+| "frees (Cst _ _) = {}"
+| "frees (A \<^bold>\<cdot> B) = frees A \<union> frees B"
+| "frees (\<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>]) = frees A - {(x,\<alpha>)}"
+
+lemma frees_subset_vars:
+  "frees A \<subseteq> vars A"
+  by (induction A) auto
+
+inductive wff :: "type_sym \<Rightarrow> trm \<Rightarrow> bool" where
+  wff_Var: "wff \<alpha> (Var _ \<alpha>)"
+| wff_Cst: "wff \<alpha> (Cst _ \<alpha>)"
+| wff_App: "wff (\<alpha> \<^bold>\<Leftarrow> \<beta>) A \<Longrightarrow> wff \<beta> B \<Longrightarrow> wff \<alpha> (A \<^bold>\<cdot> B)"
+| wff_Abs: "wff \<alpha> A \<Longrightarrow> wff (\<alpha> \<^bold>\<Leftarrow> \<beta>) \<^bold>[\<^bold>\<lambda>x:\<beta>. A\<^bold>]"
+
+fun type_of :: "trm \<Rightarrow> type_sym" where
+  "type_of (Var x \<alpha>) = \<alpha>"
+| "type_of (Cst c \<alpha>) = \<alpha>"
+| "type_of (A \<^bold>\<cdot> B) =
+     (case type_of A of \<beta> \<^bold>\<Leftarrow> \<alpha> \<Rightarrow> \<beta>)"
+| "type_of \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>] = (type_of A) \<^bold>\<Leftarrow> \<alpha>"
+
+lemma type_of[simp]:
+  "wff \<alpha> A \<Longrightarrow> type_of A = \<alpha>"
+  by (induction rule: wff.induct) auto
+
+lemma wff_Var'[simp, code]: 
+  "wff \<beta> (Var x \<alpha>) \<longleftrightarrow> \<beta> = \<alpha>"
+  using wff.cases wff_Var by auto
+
+lemma wff_Cst'[simp, code]:
+  "wff \<beta> (Cst c \<alpha>) \<longleftrightarrow> \<beta> = \<alpha>"
+  using wff.cases wff_Cst by auto
+
+lemma wff_App'[simp]:
+  "wff \<alpha> (A \<^bold>\<cdot> B) \<longleftrightarrow> (\<exists>\<beta>. wff (\<alpha> \<^bold>\<Leftarrow> \<beta>) A \<and> wff \<beta> B)"
+proof
+  assume "wff \<alpha> (A \<^bold>\<cdot> B)"
+  then show "\<exists>\<beta>. wff (\<alpha> \<^bold>\<Leftarrow> \<beta>) A \<and> wff \<beta> B" 
+    using wff.cases by fastforce
+next
+  assume "\<exists>\<beta>. wff (\<alpha> \<^bold>\<Leftarrow> \<beta>) A \<and> wff \<beta> B"
+  then show "wff \<alpha> (A \<^bold>\<cdot> B)"
+    using wff_App by auto
+qed
+
+lemma wff_Abs'[simp]:
+  "wff \<gamma> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>]) \<longleftrightarrow> (\<exists>\<beta>. wff \<beta> A \<and> \<gamma> = \<beta> \<^bold>\<Leftarrow> \<alpha>)"
+proof
+  assume "wff \<gamma> \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>]"
+  then show "\<exists>\<beta>. wff \<beta> A \<and> \<gamma> = \<beta> \<^bold>\<Leftarrow> \<alpha>" 
+    using wff.cases by blast
+next
+  assume "\<exists>\<beta>. wff \<beta> A \<and> \<gamma> = \<beta> \<^bold>\<Leftarrow> \<alpha>"
+  then show "wff \<gamma> \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>]" 
+    using wff_Abs by auto     
+qed
+
+lemma wff_Abs_type_of[code]:
+  "wff \<gamma> \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>] \<longleftrightarrow> (wff (type_of A) A \<and> \<gamma> = (type_of A) \<^bold>\<Leftarrow> \<alpha>)"
+proof
+  assume "wff \<gamma> \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>]"
+  then show "wff (type_of A) A \<and> \<gamma> = (type_of A) \<^bold>\<Leftarrow> \<alpha>" 
+    using wff.cases by auto
+next
+  assume "wff (type_of A) A \<and> \<gamma> = (type_of A) \<^bold>\<Leftarrow> \<alpha>"
+  then show "wff \<gamma> \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>]" 
+    using wff_Abs by auto
+qed
+
+lemma wff_App_type_of[code]:
+  "wff \<gamma> ((A \<^bold>\<cdot> B)) \<longleftrightarrow> (wff (type_of A) A \<and> wff (type_of B) B \<and> type_of A = \<gamma> \<^bold>\<Leftarrow> (type_of B))"
+proof
+  assume "wff \<gamma> (A \<^bold>\<cdot> B)"
+  then show "wff (type_of A) A \<and> wff (type_of B) B \<and> type_of A = \<gamma> \<^bold>\<Leftarrow> (type_of B)" 
+    by auto
+next
+  assume "wff (type_of A) A \<and> wff (type_of B) B \<and> type_of A = \<gamma> \<^bold>\<Leftarrow> (type_of B)"
+  then show "wff \<gamma> (A \<^bold>\<cdot> B)"
+    by (metis wff_App')
+qed
+
+lemma unique_type:
+  "wff \<beta> A \<Longrightarrow> wff \<alpha> A \<Longrightarrow> \<alpha> = \<beta>"
+proof (induction arbitrary: \<alpha> rule: wff.induct)
+  case (wff_Var \<alpha>' y)
+  then show ?case
+    by simp
+next
+  case (wff_Cst \<alpha>' c)
+  then show ?case
+    by simp 
+next
+  case (wff_App \<alpha>' \<beta> A B)
+  then show ?case
+    using wff_App' by blast
+next
+  case (wff_Abs \<beta> A \<alpha> x)
+  then show ?case
+    using wff_Abs_type_of by blast
+qed
+
+
+section \<open>Replacement\<close>
+
+inductive replacement :: "trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> bool" where
+  replace: "replacement A B A B"
+| replace_App_left: "replacement A B C E \<Longrightarrow> replacement A B (C \<^bold>\<cdot> D) (E \<^bold>\<cdot> D)"
+| replace_App_right: "replacement A B D E \<Longrightarrow> replacement A B (C \<^bold>\<cdot> D) (C \<^bold>\<cdot> E)"
+| replace_Abs: "replacement A B C D \<Longrightarrow> replacement A B \<^bold>[\<^bold>\<lambda>x:\<alpha>. C\<^bold>] \<^bold>[\<^bold>\<lambda>x:\<alpha>. D\<^bold>]"
+
+lemma replacement_preserves_type:
+  assumes "replacement A B C D"
+  assumes "wff \<alpha> A"
+  assumes "wff \<alpha> B"
+  assumes "wff \<beta> C"
+  shows "wff \<beta> D"
+  using assms
+proof (induction arbitrary: \<alpha> \<beta> rule: replacement.induct)
+  case (replace A B)
+  then show ?case
+    using unique_type by auto
+next
+  case (replace_App_left A B C E D)
+  then have "\<exists>\<beta>'. wff (\<beta> \<^bold>\<Leftarrow> \<beta>') C"
+    by auto
+  then obtain \<beta>' where wff_C: "wff (\<beta> \<^bold>\<Leftarrow> \<beta>') C"
+    by auto
+  then have e: "wff (\<beta> \<^bold>\<Leftarrow> \<beta>') E"
+    using replace_App_left by auto
+  define \<alpha>' where "\<alpha>' = \<beta> \<^bold>\<Leftarrow> \<beta>'"
+  have "wff \<beta>' D"
+    using wff_C unique_type replace_App_left.prems(3) by auto
+  then have "wff \<beta> (E \<^bold>\<cdot> D)"
+    using e by auto
+  then show ?case
+    by auto
+next
+  case (replace_App_right A B D E C)
+  have "\<exists>\<beta>'. wff (\<beta> \<^bold>\<Leftarrow> \<beta>') C"
+    using replace_App_right.prems(3) by auto
+  then obtain \<beta>' where wff_C: "wff (\<beta> \<^bold>\<Leftarrow> \<beta>') C"
+    by auto
+  have wff_E: "wff \<beta>' E"
+    using wff_C unique_type replace_App_right by fastforce
+  define \<alpha>' where \<alpha>': "\<alpha>' = \<beta> \<^bold>\<Leftarrow> \<beta>'"
+  have "wff \<beta> (C \<^bold>\<cdot> E)"
+    using wff_C wff_E by auto
+  then show ?case
+    using \<alpha>' by auto
+next
+  case (replace_Abs A B C D x \<alpha>')
+  then have "\<exists>\<beta>'. wff \<beta>' D"
+    by auto
+  then obtain \<beta>' where wff_D: "wff \<beta>' D"
+    by auto
+  have \<beta>: "\<beta> = \<beta>' \<^bold>\<Leftarrow> \<alpha>'"
+    using wff_D unique_type replace_Abs by auto
+  have "wff (\<beta>' \<^bold>\<Leftarrow> \<alpha>') (\<^bold>[\<^bold>\<lambda>x:\<alpha>'. D\<^bold>])"
+    using wff_D by auto
+  then show ?case
+    using \<beta> by auto
+qed
+
+lemma replacement_preserved_type:
+  assumes "replacement A B C D"
+  assumes "wff \<alpha> A"
+  assumes "wff \<alpha> B"
+  assumes "wff \<beta> D"
+  shows "wff \<beta> C"
+  using assms
+proof (induction arbitrary: \<alpha> \<beta> rule: replacement.induct)
+  case (replace A B)
+  then show ?case 
+    using unique_type by auto
+next
+  case (replace_App_left A B C E D)
+  then obtain \<gamma> where \<gamma>: "wff (\<beta> \<^bold>\<Leftarrow> \<gamma>) E \<and> wff \<gamma> D"
+    by auto
+  then have "wff (\<beta> \<^bold>\<Leftarrow> \<gamma>) C"
+    using replace_App_left by auto
+  then show ?case
+    using \<gamma> by auto 
+next
+  case (replace_App_right A B D E C)
+  then obtain \<gamma> where \<gamma>: "wff (\<beta> \<^bold>\<Leftarrow> \<gamma>) C \<and> wff \<gamma> E"
+    by auto
+  then have "wff \<gamma> D"
+    using replace_App_right by auto
+  then show ?case
+    using \<gamma> by auto 
+next
+  case (replace_Abs A B C D x \<alpha>')
+  then obtain \<gamma> where "wff \<gamma> D"
+    by auto
+  then show ?case
+    using unique_type replace_Abs by auto
+qed
+
+
+section \<open>Defined wffs\<close>
+  \<comment> \<open>This section formalizes most of the definitions and abbreviations from page 212.
+    We formalize enough to define the Q0 proof system.\<close>
+
+
+subsection \<open>Common expressions\<close>
+
+abbreviation (input) Var_yi ("y\<^sub>i") where
+  "y\<^sub>i == Cst ''y'' Ind"
+
+abbreviation (input) Var_xo ("x\<^sub>o") where
+  "x\<^sub>o == Var ''x'' Tv"
+
+abbreviation (input) Var_yo ("y\<^sub>o") where
+  "y\<^sub>o == Var ''y'' Tv"
+
+abbreviation (input) Fun_oo ("oo") where
+  "oo == Tv \<^bold>\<Leftarrow> Tv"
+
+abbreviation (input) Fun_ooo ("ooo") where
+  "ooo == oo \<^bold>\<Leftarrow> Tv"
+
+abbreviation (input) Var_goo ("g\<^sub>o\<^sub>o") where
+  "g\<^sub>o\<^sub>o == Var ''g'' oo"
+
+abbreviation (input) Var_gooo ("g\<^sub>o\<^sub>o\<^sub>o") where
+  "g\<^sub>o\<^sub>o\<^sub>o == Var ''g'' ooo"
+
+
+subsection \<open>Equality symbol\<close>
+
+abbreviation QQ :: "type_sym \<Rightarrow> trm" ("\<^bold>Q") where
+  "\<^bold>Q \<alpha> \<equiv> Cst ''Q'' \<alpha>"
+
+
+subsection \<open>Description or selection operator\<close>
+
+abbreviation \<iota>\<iota> :: "trm" ("\<^bold>\<iota>") where
+  "\<^bold>\<iota> \<equiv> Cst ''i'' (Ind \<^bold>\<Leftarrow> (Tv \<^bold>\<Leftarrow> Ind))"
+
+
+subsection \<open>Equality\<close>
+
+definition Eql :: "trm \<Rightarrow> trm \<Rightarrow> type_sym \<Rightarrow> trm" where
+  "Eql A B \<alpha> \<equiv> (\<^bold>Q (Tv \<^bold>\<Leftarrow> \<alpha> \<^bold>\<Leftarrow> \<alpha>)) \<^bold>\<cdot> A \<^bold>\<cdot> B"
+
+abbreviation Eql' :: "trm \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> trm" ("\<^bold>[_ \<^bold>=_\<^bold>= _\<^bold>]" [89]) where
+  "\<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>] \<equiv> Eql A B \<alpha>"
+
+definition LHS where
+  "LHS EqlAB = (case EqlAB of (_ \<^bold>\<cdot> A \<^bold>\<cdot> _) \<Rightarrow> A)"
+
+lemma LHS_def2[simp]: "LHS \<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>] = A"
+  unfolding LHS_def Eql_def by auto
+
+definition RHS where
+  "RHS EqlAB = (case EqlAB of (_ \<^bold>\<cdot> B ) \<Rightarrow> B)"
+
+lemma RHS_def2[simp]: "RHS (\<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>]) = B"
+  unfolding RHS_def Eql_def by auto
+
+lemma wff_Eql[simp]:
+  "wff \<alpha> A \<Longrightarrow> wff \<alpha> B \<Longrightarrow> wff Tv \<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>]"
+  unfolding Eql_def by force
+
+lemma wff_Eql_iff[simp]:
+  "wff \<beta> \<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>] \<longleftrightarrow> wff \<alpha> A \<and> wff \<alpha> B \<and> \<beta> = Tv"
+  using Eql_def by auto
+
+
+subsection \<open>Truth\<close>
+
+definition T :: trm where
+  "T \<equiv> \<^bold>[(\<^bold>Q ooo) \<^bold>=ooo\<^bold>= (\<^bold>Q ooo)\<^bold>]"
+
+lemma wff_T[simp]: "wff Tv T"
+  unfolding T_def by auto
+
+lemma wff_T_iff[simp]: "wff \<alpha> T \<longleftrightarrow> \<alpha> = Tv"
+  using unique_type wff_T by blast
+
+subsection \<open>Falsity\<close>
+
+abbreviation F :: trm where
+  "F \<equiv> \<^bold>[\<^bold>[\<^bold>\<lambda>''x'':Tv. T\<^bold>] \<^bold>= oo\<^bold>= \<^bold>[\<^bold>\<lambda>''x'':Tv. x\<^sub>o\<^bold>]\<^bold>]"
+
+lemma wff_F[simp]: "wff Tv F"
+  by auto
+
+lemma wff_F_iff[simp]: "wff \<alpha> F \<longleftrightarrow> \<alpha> = Tv"
+  using unique_type wff_F by blast
+
+
+subsection \<open>Pi\<close>
+
+definition PI :: "type_sym \<Rightarrow> trm" where
+  "PI \<alpha> \<equiv> (\<^bold>Q (Tv \<^bold>\<Leftarrow> (Tv \<^bold>\<Leftarrow> \<alpha>) \<^bold>\<Leftarrow> (Tv \<^bold>\<Leftarrow> \<alpha>))) \<^bold>\<cdot> \<^bold>[\<^bold>\<lambda> ''x'':\<alpha>. T\<^bold>]"
+
+lemma wff_PI[simp]: "wff (Tv \<^bold>\<Leftarrow> (Tv \<^bold>\<Leftarrow> \<alpha>)) (PI \<alpha>)"
+  unfolding PI_def by auto
+
+lemma wff_PI_subterm[simp]: "wff (Tv \<^bold>\<Leftarrow> \<alpha>) \<^bold>[\<^bold>\<lambda> ''x'':\<alpha>. T\<^bold>]"
+  by auto
+
+lemma wff_PI_subterm_iff[simp]:
+  "wff \<beta> \<^bold>[\<^bold>\<lambda> ''x'':\<alpha>. T\<^bold>] \<longleftrightarrow> \<beta> = (Tv \<^bold>\<Leftarrow> \<alpha>)"
+  by auto
+
+
+subsection \<open>Forall\<close>
+
+definition Forall :: "string \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> trm" ("\<^bold>[\<^bold>\<forall>_:_. _\<^bold>]" [80,80,80]) where 
+  "\<^bold>[\<^bold>\<forall>x:\<alpha>. A\<^bold>] = (PI \<alpha>) \<^bold>\<cdot> \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>]"
+
+lemma wff_Forall[simp]: "wff Tv A \<Longrightarrow> wff Tv \<^bold>[\<^bold>\<forall>x:\<alpha>. A\<^bold>]"
+  unfolding Forall_def by force
+
+lemma wff_Forall_iff[simp]: "wff \<beta> \<^bold>[\<^bold>\<forall>x:\<alpha>. A\<^bold>] \<longleftrightarrow> wff Tv A \<and> \<beta> = Tv"
+proof 
+  assume "wff \<beta> \<^bold>[\<^bold>\<forall>x:\<alpha>. A\<^bold>]"
+  then show "wff Tv A \<and> \<beta> = Tv"
+    by (smt Forall_def unique_type type_sym.inject wff_Abs' wff_App' wff_PI)
+next
+  assume "wff Tv A \<and> \<beta> = Tv"
+  then show "wff \<beta> \<^bold>[\<^bold>\<forall>x:\<alpha>. A\<^bold>]" 
+    unfolding Forall_def by force
+qed
+
+
+subsection \<open>Conjunction symbol\<close>
+
+definition Con_sym :: trm where
+  "Con_sym \<equiv>
+    \<^bold>[\<^bold>\<lambda>''x'':Tv. \<^bold>[\<^bold>\<lambda>''y'':Tv.
+      \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>]  \<^bold>=Tv \<^bold>\<Leftarrow> ooo\<^bold>=  \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]
+    \<^bold>]\<^bold>]"
+
+lemma wff_Con_sym[simp]: "wff ooo Con_sym"
+  unfolding Con_sym_def by auto
+
+lemma wff_Con_sym'[simp]: "wff \<alpha> Con_sym \<longleftrightarrow> \<alpha> = ooo"
+  unfolding Con_sym_def by auto
+
+
+lemma wff_Con_sym_subterm0[simp]:
+  "wff Tv A \<Longrightarrow> wff Tv B \<Longrightarrow> wff (Tv \<^bold>\<Leftarrow> ooo) \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> A \<^bold>\<cdot> B\<^bold>]"
+  by force
+
+lemma wff_Con_sym_subterm0_iff[simp]:
+  "wff \<beta> \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> A \<^bold>\<cdot> B\<^bold>] \<longleftrightarrow> wff Tv A \<and> wff Tv B \<and> \<beta> = (Tv \<^bold>\<Leftarrow> ooo)"
+proof
+  assume wff: "wff \<beta> \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> A \<^bold>\<cdot> B\<^bold>]"
+  then have "wff Tv A"
+    by auto
+  moreover
+  from wff have "wff Tv B"
+    by auto
+  moreover
+  from wff have "\<beta> = Tv \<^bold>\<Leftarrow> ooo"
+    by auto
+  ultimately show "wff Tv A \<and> wff Tv B \<and> \<beta> = Tv \<^bold>\<Leftarrow> ooo"
+    by auto
+next
+  assume "wff Tv A \<and> wff Tv B \<and> \<beta> = Tv \<^bold>\<Leftarrow> ooo"
+  then show "wff \<beta> \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> A \<^bold>\<cdot> B\<^bold>]"
+    by force
+qed
+
+lemma wff_Con_sym_subterm1[simp]:
+  "wff Tv \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]"
+  by auto
+
+lemma wff_Con_sym_subterm1_iff[simp]:
+  "wff \<alpha> \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>] \<longleftrightarrow> \<alpha> = Tv"
+  using unique_type wff_Con_sym_subterm1 by blast
+
+lemma wff_Con_sym_subterm2[simp]:
+  "wff oo \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>]"
+  by auto
+
+lemma wff_Con_sym_subterm2_iff[simp]:
+  "wff \<alpha> \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot>  x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>] \<longleftrightarrow> \<alpha> = oo"
+  by auto
+
+subsection \<open>Conjunction\<close>
+
+definition Con :: "trm \<Rightarrow> trm \<Rightarrow> trm" (infix "\<^bold>\<and>" 80) where
+  "A \<^bold>\<and> B = Con_sym \<^bold>\<cdot> A \<^bold>\<cdot> B"
+
+lemma wff_Con[simp]: "wff Tv A \<Longrightarrow> wff Tv B \<Longrightarrow> wff Tv (A \<^bold>\<and> B)"
+  unfolding Con_def by auto
+
+lemma wff_Con_iff[simp]: "wff \<alpha> (A \<^bold>\<and> B) \<longleftrightarrow> wff Tv A \<and> wff Tv B \<and> \<alpha> = Tv"
+  unfolding Con_def by auto
+
+
+subsection \<open>Implication symbol\<close>
+
+definition Imp_sym :: trm where
+  "Imp_sym \<equiv> \<^bold>[\<^bold>\<lambda>''x'':Tv. \<^bold>[\<^bold>\<lambda>''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>]\<^bold>]"
+
+lemma wff_Imp_sym[simp]:
+  "wff ooo Imp_sym"
+  unfolding Imp_sym_def by auto
+
+lemma wff_Imp_sym_iff[simp]:
+  "wff \<alpha> Imp_sym \<longleftrightarrow> \<alpha> = ooo"
+  unfolding Imp_sym_def by auto
+
+lemma wff_Imp_sym_subterm0[simp]:
+  "wff Tv (x\<^sub>o \<^bold>\<and> y\<^sub>o)"
+  by auto
+
+lemma wff_Imp_sym_subterm0_iff[simp]:
+  "wff \<alpha> (x\<^sub>o \<^bold>\<and> y\<^sub>o) \<longleftrightarrow> \<alpha> = Tv"
+   by auto
+
+lemma wff_Imp_sym_subterm1[simp]:
+  "wff Tv \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]"
+  by auto
+
+lemma wff_Imp_sym_subterm1_iff[simp]:
+  "wff \<alpha> \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>] \<longleftrightarrow> \<alpha> = Tv"
+  using unique_type wff_Imp_sym_subterm1 by blast
+
+lemma wff_Imp_sym_subterm2[simp]:
+  "wff oo \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>]"
+  by auto
+
+lemma wff_Imp_sym_subterm2_iff[simp]:
+  "wff \<alpha> \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>] \<longleftrightarrow> \<alpha> = oo"
+  by auto
+
+
+subsection \<open>Implication\<close>
+
+definition Imp :: "trm \<Rightarrow> trm \<Rightarrow> trm" (infix "\<^bold>\<longrightarrow>" 80) where
+  "A \<^bold>\<longrightarrow> B = Imp_sym \<^bold>\<cdot> A \<^bold>\<cdot> B"
+
+lemma wff_Imp[simp]: "wff Tv A \<Longrightarrow> wff Tv B \<Longrightarrow> wff Tv (A \<^bold>\<longrightarrow> B)"
+  unfolding Imp_def by auto
+
+lemma wff_Imp_iff[simp]: "wff \<alpha> (A \<^bold>\<longrightarrow> B) \<longleftrightarrow> wff Tv A \<and> wff Tv B \<and> \<alpha> = Tv"
+  using Imp_def by auto
+
+
+section \<open>The Q0 proof system\<close>
+
+definition axiom_1 :: trm where
+  "axiom_1 \<equiv> \<^bold>[((g\<^sub>o\<^sub>o \<^bold>\<cdot> T) \<^bold>\<and> (g\<^sub>o\<^sub>o \<^bold>\<cdot> F)) \<^bold>=Tv\<^bold>= \<^bold>[\<^bold>\<forall>''x'':Tv. g\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o\<^bold>]\<^bold>]"
+
+lemma wff_axiom_1[simp]: "wff Tv axiom_1"
+  unfolding axiom_1_def by auto
+
+definition axiom_2 :: "type_sym \<Rightarrow> trm" where
+  "axiom_2 \<alpha> \<equiv>
+       \<^bold>[(Var ''x'' \<alpha>) \<^bold>=\<alpha>\<^bold>= (Var ''y'' \<alpha>)\<^bold>] \<^bold>\<longrightarrow>
+       \<^bold>[((Var ''h'' (Tv \<^bold>\<Leftarrow> \<alpha>)) \<^bold>\<cdot> (Var ''x'' \<alpha>)) \<^bold>=Tv\<^bold>= ((Var ''h'' (Tv \<^bold>\<Leftarrow> \<alpha>)) \<^bold>\<cdot> (Var ''y'' \<alpha>))\<^bold>]"
+
+definition axiom_3 :: "type_sym \<Rightarrow> type_sym \<Rightarrow> trm" where
+  "axiom_3 \<alpha> \<beta> \<equiv>
+       \<^bold>[\<^bold>[(Var ''f'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<^bold>=\<alpha> \<^bold>\<Leftarrow> \<beta>\<^bold>= (Var ''g'' (\<alpha> \<^bold>\<Leftarrow> \<beta>))\<^bold>] \<^bold>=Tv\<^bold>=
+       \<^bold>[\<^bold>\<forall>''x'':\<beta>. \<^bold>[((Var ''f'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<^bold>\<cdot> (Var ''x'' \<beta>)) \<^bold>=\<alpha>\<^bold>= ((Var ''g'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<^bold>\<cdot> (Var ''x'' \<beta>))\<^bold>]\<^bold>]\<^bold>]"
+
+definition axiom_4_1 :: "var_sym \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> trm" where
+  "axiom_4_1 x \<alpha> B \<beta> A \<equiv> \<^bold>[(\<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A) \<^bold>=\<beta>\<^bold>= B\<^bold>]"
+
+definition axiom_4_1_side_condition :: "var_sym \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> bool" where
+  "axiom_4_1_side_condition x \<alpha> B \<beta> A \<equiv> (\<exists>c. B = Cst c \<beta>) \<or> (\<exists>y. B = Var y \<beta> \<and> (x \<noteq> y \<or> \<alpha> \<noteq> \<beta>))"
+
+definition axiom_4_2 :: "var_sym \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> trm" where
+  "axiom_4_2 x \<alpha> A = \<^bold>[(\<^bold>[\<^bold>\<lambda>x:\<alpha>. Var x \<alpha>\<^bold>] \<^bold>\<cdot> A) \<^bold>=\<alpha>\<^bold>= A\<^bold>]"
+
+definition axiom_4_3 :: "var_sym \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow>
+                          type_sym \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> trm  \<Rightarrow> trm" where
+  "axiom_4_3 x \<alpha> B \<beta> \<gamma> C A = \<^bold>[(\<^bold>[\<^bold>\<lambda>x:\<alpha>. B \<^bold>\<cdot> C\<^bold>] \<^bold>\<cdot> A) \<^bold>=\<beta>\<^bold>= ((\<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A) \<^bold>\<cdot> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. C\<^bold>] \<^bold>\<cdot> A))\<^bold>]"
+
+definition axiom_4_4 :: "var_sym \<Rightarrow> type_sym \<Rightarrow> var_sym \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> trm" where
+  "axiom_4_4 x \<alpha> y \<gamma> B \<delta> A = \<^bold>[(\<^bold>[\<^bold>\<lambda>x:\<alpha>. \<^bold>[\<^bold>\<lambda>y:\<gamma>. B\<^bold>]\<^bold>] \<^bold>\<cdot> A) \<^bold>=\<delta> \<^bold>\<Leftarrow> \<gamma>\<^bold>= \<^bold>[\<^bold>\<lambda>y:\<gamma>. \<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A\<^bold>]\<^bold>]"
+
+definition axiom_4_4_side_condition :: "var_sym \<Rightarrow> type_sym \<Rightarrow> var_sym \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> bool" where
+  "axiom_4_4_side_condition x \<alpha> y \<gamma> B \<delta> A \<equiv> (x \<noteq> y \<or> \<alpha> \<noteq> \<gamma>) \<and> (y, \<gamma>) \<notin> vars A"
+
+definition axiom_4_5 :: "var_sym \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> trm" where
+  "axiom_4_5 x \<alpha> B \<delta> A = \<^bold>[(\<^bold>[\<^bold>\<lambda>x:\<alpha>. \<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>]\<^bold>] \<^bold>\<cdot> A) \<^bold>=\<delta> \<^bold>\<Leftarrow> \<alpha> \<^bold>= \<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>]\<^bold>]"
+
+definition axiom_5 where
+  "axiom_5 = \<^bold>[(\<^bold>\<iota> \<^bold>\<cdot> ((\<^bold>Q (Tv \<^bold>\<Leftarrow> Ind \<^bold>\<Leftarrow> Ind)) \<^bold>\<cdot> y\<^sub>i)) \<^bold>=Ind\<^bold>= y\<^sub>i\<^bold>]"
+
+inductive axiom :: "trm \<Rightarrow> bool" where
+  by_axiom_1: 
+  "axiom axiom_1"
+| by_axiom_2: 
+  "axiom (axiom_2 \<alpha>)"
+| by_axiom_3: 
+  "axiom (axiom_3 \<alpha> \<beta>)"
+| by_axiom_4_1: 
+  "wff \<alpha> A \<Longrightarrow>
+   wff \<beta> B \<Longrightarrow>
+   axiom_4_1_side_condition x \<alpha> B \<beta> A \<Longrightarrow>
+   axiom (axiom_4_1 x \<alpha> B \<beta> A)"
+| by_axiom_4_2: 
+  "wff \<alpha> A \<Longrightarrow>
+   axiom (axiom_4_2 x \<alpha> A)"
+| by_axiom_4_3: 
+  "wff \<alpha> A \<Longrightarrow>
+   wff (\<beta> \<^bold>\<Leftarrow> \<gamma>) B \<Longrightarrow>
+   wff \<gamma> C \<Longrightarrow>
+   axiom (axiom_4_3 x \<alpha> B \<beta> \<gamma> C A)"
+| by_axiom_4_4: 
+  "wff \<alpha> A \<Longrightarrow>
+   wff \<delta> B \<Longrightarrow>
+   axiom_4_4_side_condition x \<alpha> y \<gamma> B \<delta> A \<Longrightarrow>
+   axiom (axiom_4_4 x \<alpha> y \<gamma> B \<delta> A)"
+| by_axiom_4_5: 
+  "wff \<alpha> A \<Longrightarrow>
+   wff \<delta> B \<Longrightarrow>
+   axiom (axiom_4_5 x \<alpha> B \<delta> A)"
+| by_axiom_5: 
+  "axiom (axiom_5)"
+
+inductive rule_R :: "trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> bool" where
+  "replacement A B C D \<Longrightarrow> rule_R C (\<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>]) D"
+
+definition "proof" :: "trm \<Rightarrow> trm list \<Rightarrow> bool" where
+  "proof A p \<longleftrightarrow> (p \<noteq> [] \<and> last p = A \<and>
+                    (\<forall>i<length p. axiom (p ! i) 
+                  \<or> (\<exists>j<i. \<exists>k<i. rule_R (p ! j) (p ! k) (p ! i))))"
+
+(* Peter Andrews defines theorems directly from "proof", here I instead define it as an inductive predicate based on rule_R *)
+inductive "theorem" :: "trm \<Rightarrow> bool" where
+  by_axiom: "axiom A \<Longrightarrow> theorem A"
+| by_rule_R: "theorem A \<Longrightarrow> theorem B \<Longrightarrow> rule_R A B C \<Longrightarrow> theorem C"
+
+(* Two variant formulations of axiom 4_1: *)
+definition axiom_4_1_variant_cst :: "var_sym \<Rightarrow> type_sym \<Rightarrow> var_sym \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> trm" where
+  "axiom_4_1_variant_cst x \<alpha> c \<beta> A \<equiv> \<^bold>[(\<^bold>[\<^bold>\<lambda>x:\<alpha>. Cst c \<beta>\<^bold>] \<^bold>\<cdot> A) \<^bold>=\<beta>\<^bold>= (Cst c \<beta>)\<^bold>]"
+
+definition axiom_4_1_variant_var :: "var_sym \<Rightarrow> type_sym \<Rightarrow> var_sym \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> trm" where
+  "axiom_4_1_variant_var x \<alpha> y \<beta> A \<equiv>  \<^bold>[(\<^bold>[\<^bold>\<lambda>x:\<alpha>. Var y \<beta>\<^bold>] \<^bold>\<cdot> A) \<^bold>=\<beta>\<^bold>= Var y \<beta>\<^bold>]"
+
+definition axiom_4_1_variant_var_side_condition :: "var_sym \<Rightarrow> type_sym \<Rightarrow> var_sym \<Rightarrow> type_sym \<Rightarrow> trm \<Rightarrow> bool" where
+  "axiom_4_1_variant_var_side_condition x \<alpha> y \<beta> A \<equiv> x \<noteq> y \<or> \<alpha> \<noteq> \<beta>"
+
+
+section \<open>Semantics\<close>
+
+type_synonym 's frame = "type_sym \<Rightarrow> 's"
+
+type_synonym 's denotation = "cst_sym \<Rightarrow> type_sym \<Rightarrow> 's"
+
+type_synonym 's asg = "var_sym * type_sym \<Rightarrow> 's"
+
+definition agree_off_asg :: "'s asg \<Rightarrow> 's asg \<Rightarrow> var_sym \<Rightarrow> type_sym \<Rightarrow> bool" where
+  "agree_off_asg \<phi> \<psi> x \<alpha> \<longleftrightarrow> (\<forall>y \<beta>. (y\<noteq>x \<or> \<beta> \<noteq> \<alpha>) \<longrightarrow> \<phi> (y,\<beta>) = \<psi> (y,\<beta>))"
+
+lemma agree_off_asg_def2:
+  "agree_off_asg \<psi> \<phi> x \<alpha> \<longleftrightarrow> (\<exists>xa. \<phi>((x, \<alpha>) := xa) = \<psi>)"
+  unfolding agree_off_asg_def by force
+
+lemma agree_off_asg_disagree_var_sym[simp]:
+  "agree_off_asg \<psi> \<phi> x \<alpha> \<Longrightarrow> x \<noteq> y \<Longrightarrow> \<psi>(y,\<beta>) = \<phi>(y,\<beta>)"
+  unfolding agree_off_asg_def by auto
+
+lemma agree_off_asg_disagree_type_sym[simp]:
+  "agree_off_asg \<psi> \<phi> x \<alpha> \<Longrightarrow> \<alpha> \<noteq> \<beta> \<Longrightarrow> \<psi>(y,\<beta>) = \<phi>(y,\<beta>)"
+  unfolding agree_off_asg_def by auto
+
+
+context set_theory
+begin
+
+definition wf_frame :: "'s frame \<Rightarrow> bool" where
+  "wf_frame D \<longleftrightarrow> D Tv = boolset \<and> (\<forall>\<alpha> \<beta>. D (\<alpha> \<^bold>\<Leftarrow> \<beta>) \<subseteq>: funspace (D \<beta>) (D \<alpha>)) \<and> (\<forall>\<alpha>. D \<alpha> \<noteq> Ø)"
+
+definition inds :: "'s frame \<Rightarrow> 's" where
+  "inds Fr = Fr Ind"
+
+inductive wf_interp :: "'s frame \<Rightarrow> 's denotation \<Rightarrow> bool" where
+  "wf_frame D \<Longrightarrow>
+   \<forall>c \<alpha>. I c \<alpha> \<in>: D \<alpha> \<Longrightarrow>
+   \<forall>\<alpha>. I ''Q'' (Tv \<^bold>\<Leftarrow> \<alpha> \<^bold>\<Leftarrow> \<alpha>) = iden (D \<alpha>) \<Longrightarrow>
+   (I ''i'' (Ind \<^bold>\<Leftarrow> (Tv \<^bold>\<Leftarrow> Ind))) \<in>: funspace (D (Tv \<^bold>\<Leftarrow> Ind)) (D Ind) \<Longrightarrow>
+   \<forall>x. x \<in>: D Ind \<longrightarrow> (I ''i'' (Ind \<^bold>\<Leftarrow> (Tv \<^bold>\<Leftarrow> Ind))) \<cdot> one_elem_fun x (D Ind) = x \<Longrightarrow>
+   wf_interp D I"
+
+definition asg_into_frame :: "'s asg \<Rightarrow> 's frame \<Rightarrow> bool" where
+  "asg_into_frame \<phi> D \<longleftrightarrow> (\<forall>x \<alpha>. \<phi> (x, \<alpha>) \<in>: D \<alpha>)"
+
+abbreviation(input) asg_into_interp :: "'s asg \<Rightarrow> 's frame \<Rightarrow> 's denotation \<Rightarrow> bool" where
+  "asg_into_interp \<phi> D I \<equiv> asg_into_frame \<phi> D"
+
+(* Note that because Isabelle's HOL is total, val will also give values to trms that are not wffs *)
+fun val :: "'s frame \<Rightarrow> 's denotation \<Rightarrow> 's asg \<Rightarrow> trm \<Rightarrow> 's" where
+  "val D I \<phi> (Var x \<alpha>) = \<phi> (x,\<alpha>)"
+| "val D I \<phi> (Cst c \<alpha>) = I c \<alpha>"
+| "val D I \<phi> (A \<^bold>\<cdot> B) = val D I \<phi> A \<cdot> val D I \<phi> B"
+| "val D I \<phi> \<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] = abstract (D \<alpha>) (D (type_of B)) (\<lambda>z. val D I (\<phi>((x,\<alpha>):=z)) B)"
+
+fun general_model :: "'s frame \<Rightarrow> 's denotation \<Rightarrow> bool" where
+  "general_model D I \<longleftrightarrow> wf_interp D I \<and> (\<forall>\<phi> A \<alpha>. asg_into_interp \<phi> D I \<longrightarrow> wff \<alpha> A \<longrightarrow> val D I \<phi> A \<in>: D \<alpha>)"
+
+fun standard_model :: "'s frame \<Rightarrow> 's denotation \<Rightarrow> bool" where
+  "standard_model D I \<longleftrightarrow> wf_interp D I \<and> (\<forall>\<alpha> \<beta>. D (\<alpha> \<^bold>\<Leftarrow> \<beta>) = funspace (D \<beta>) (D \<alpha>))"
+
+lemma asg_into_frame_fun_upd:
+  assumes "asg_into_frame \<phi> D"
+  assumes "xa \<in>: D \<alpha>"
+  shows "asg_into_frame (\<phi>((x, \<alpha>) := xa)) D"
+  using assms unfolding asg_into_frame_def by auto
+
+lemma asg_into_interp_fun_upd:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "wff \<alpha> A"
+  shows "asg_into_interp (\<phi>((x, \<alpha>) := val D I \<phi> A)) D I"
+  using assms asg_into_frame_fun_upd by auto
+
+lemma standard_model_is_general_model: (* property mentioned on page 239 *)
+  assumes "standard_model D I"
+  shows "general_model D I" 
+proof -
+  have "wf_interp D I"
+    using assms by auto
+  moreover
+  have "wff \<alpha> A \<Longrightarrow> asg_into_interp \<phi> D I \<Longrightarrow> val D I \<phi> A \<in>: D \<alpha>" for \<phi> \<alpha> A
+  proof (induction arbitrary: \<phi> rule: wff.induct)
+    case (wff_Var \<alpha> uu)
+    then show ?case
+      unfolding asg_into_frame_def using assms by auto
+  next
+    case (wff_Cst \<alpha> uv)
+    then show ?case 
+      using assms using wf_interp.simps by auto
+  next
+    case (wff_App \<alpha> \<beta> A B)
+    then show ?case
+      using apply_in_rng assms by fastforce
+  next
+    case (wff_Abs \<beta> A \<alpha> x)
+    then show ?case 
+      using assms abstract_in_funspace asg_into_frame_fun_upd by force
+  qed
+  ultimately
+  have "general_model D I"
+    unfolding general_model.simps by auto
+  then show "general_model D I"
+    by auto
+qed
+
+abbreviation agree_on_asg :: "'s asg \<Rightarrow> 's asg \<Rightarrow> var_sym \<Rightarrow> type_sym \<Rightarrow> bool" where
+  "agree_on_asg \<phi> \<psi> x \<alpha> == (\<phi> (x, \<alpha>) = \<psi> (x, \<alpha>))"
+
+(* Corresponds to Andrews' proposition 5400 *)
+proposition prop_5400:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "asg_into_interp \<psi> D I"
+  assumes "wff \<alpha> A"
+  assumes "\<forall>(x,\<alpha>) \<in> frees A. agree_on_asg \<phi> \<psi> x \<alpha>"
+  shows "val D I \<phi> A = val D I \<psi> A"
+  using assms(4) assms(1-3,5)
+proof (induction arbitrary: \<phi> \<psi> rule: wff.induct)
+  case (wff_Var \<alpha> x)
+  then show ?case by auto
+next
+  case (wff_Cst \<alpha> c)
+  then show ?case by auto
+next
+  case (wff_App \<alpha> \<beta> A B)
+  show ?case
+    using wff_App(1,2,5,6,7,8) wff_App(3,4)[of \<phi> \<psi>] by auto
+next
+  case (wff_Abs \<beta> A \<alpha> x)
+  have "abstract (D \<alpha>) (D \<beta>) (\<lambda>z. val D I (\<phi>((x, \<alpha>) := z)) A) = 
+        abstract (D \<alpha>) (D \<beta>) (\<lambda>z. val D I (\<psi>((x, \<alpha>) := z)) A)"
+  proof (rule abstract_extensional, rule, rule)
+    fix xa
+    assume "xa \<in>: D \<alpha>"
+    then have "val D I (\<phi>((x, \<alpha>) := xa)) A \<in>: D \<beta>"
+      using wff_Abs asg_into_frame_fun_upd by auto
+    moreover
+    {
+      have "asg_into_frame (\<psi>((x, \<alpha>) := xa)) D"
+        using \<open>xa \<in>: D \<alpha>\<close> asg_into_frame_fun_upd wff_Abs by auto
+      moreover
+      have "asg_into_frame (\<phi>((x, \<alpha>) := xa)) D"
+        using \<open>xa \<in>: D \<alpha>\<close> asg_into_frame_fun_upd wff_Abs by auto
+      moreover
+      have "(\<forall>y\<in>frees A. (\<phi>((x, \<alpha>) := xa)) y = (\<psi>((x, \<alpha>) := xa)) y)"
+        using wff_Abs by auto
+      ultimately
+      have "val D I (\<phi>((x, \<alpha>) := xa)) A = val D I (\<psi>((x, \<alpha>) := xa)) A"
+        using assms wff_Abs by (smt case_prodI2) 
+    }  
+    ultimately
+    show "val D I (\<phi>((x, \<alpha>) := xa)) A \<in>: D \<beta> \<and> val D I (\<phi>((x, \<alpha>) := xa)) A = val D I (\<psi>((x, \<alpha>) := xa)) A"
+      by auto
+  qed
+  then show ?case
+    using wff_Abs by auto 
+qed
+
+(* definitions on page 239 *)
+abbreviation satisfies :: "'s frame \<Rightarrow> 's denotation \<Rightarrow> 's asg \<Rightarrow> trm \<Rightarrow> bool" where
+  "satisfies D I \<phi> A \<equiv> (val D I \<phi> A = true)"
+
+definition valid_in_model :: "'s frame \<Rightarrow> 's denotation \<Rightarrow> trm \<Rightarrow> bool" where
+  "valid_in_model D I A \<equiv> (\<forall>\<phi>. asg_into_interp \<phi> D I \<longrightarrow> val D I \<phi> A = true)"
+
+definition valid_general :: "trm \<Rightarrow> bool" where
+  "valid_general A \<equiv> \<forall>D I. general_model D I \<longrightarrow> valid_in_model D I A"
+
+definition valid_standard :: "trm \<Rightarrow> bool" where
+  "valid_standard A \<equiv> \<forall>D I. standard_model D I \<longrightarrow> valid_in_model D I A"
+
+
+section \<open>Semantics of defined wffs\<close>
+
+(* Corresponds to Andrews' lemma 5401 a *)
+lemma lemma_5401_a:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "wff \<alpha> A" "wff \<beta> B"
+  shows "val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A) = val D I (\<phi>((x,\<alpha>):=val D I \<phi> A)) B"
+proof -
+  have val_A: "val D I \<phi> A \<in>: D \<alpha>"
+    using assms  by simp
+  have "asg_into_interp (\<phi>((x, \<alpha>) := val D I \<phi> A)) D I"
+    using assms asg_into_frame_fun_upd  by force
+  then have val_B: "val D I (\<phi>((x, \<alpha>) := val D I \<phi> A)) B \<in>: D \<beta>"
+    using assms by simp
+
+  have "val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A) =
+          (abstract (D \<alpha>) (D \<beta>) (\<lambda>z. val D I (\<phi>((x, \<alpha>) := z)) B)) \<cdot> val D I \<phi> A"
+    using assms by auto
+  also
+  have "... = val D I (\<phi>((x, \<alpha>) := val D I \<phi> A)) B"
+    using apply_abstract val_A val_B by auto
+  finally
+  show ?thesis 
+    by auto
+qed
+
+(* Corresponds to Andrews' lemma 5401 b *)
+lemma lemma_5401_b_variant_1:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "wff \<alpha> A" "wff \<alpha> B"
+  shows "val D I \<phi> (\<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>]) = (boolean (val D I \<phi> A = val D I \<phi> B))"
+proof -
+  have "val D I \<phi> (\<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>]) = (I ''Q'' (Tv \<^bold>\<Leftarrow> \<alpha> \<^bold>\<Leftarrow> \<alpha>)) \<cdot> val D I \<phi> A \<cdot> val D I \<phi> B"
+    unfolding Eql_def by auto
+  have "... = (iden (D \<alpha>)) \<cdot> val D I \<phi> A \<cdot> val D I \<phi> B"
+    using assms general_model.simps wf_interp.simps by auto 
+  also
+  have "... = boolean (val D I \<phi> A = val D I \<phi> B)"
+    using apply_id using assms general_model.simps by blast
+  finally show ?thesis 
+    unfolding Eql_def by simp
+qed
+
+(* Corresponds to Andrews' lemma 5401 b *)
+lemma lemma_5401_b:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "wff \<alpha> A" "wff \<alpha> B"
+  shows "val D I \<phi> (\<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>]) = true \<longleftrightarrow> val D I \<phi> A = val D I \<phi> B"
+  using lemma_5401_b_variant_1[OF assms] boolean_eq_true by auto
+
+(* Corresponds to Andrews' lemma 5401 b *)
+lemma lemma_5401_b_variant_2: \<comment> \<open>Just a reformulation of @{thm [source] lemma_5401_b}'s directions\<close> 
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "wff \<alpha> A" "wff \<alpha> B"
+  assumes "val D I \<phi> A = val D I \<phi> B"
+  shows "val D I \<phi> (\<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>]) = true"
+  using assms(5) lemma_5401_b[OF assms(1,2,3,4)] by auto 
+
+(* Corresponds to Andrews' lemma 5401 b *)
+lemma lemma_5401_b_variant_3: \<comment> \<open>Just a reformulation of @{thm [source] lemma_5401_b}'s directions\<close> 
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "wff \<alpha> A" "wff \<alpha> B"
+  assumes "val D I \<phi> A \<noteq> val D I \<phi> B"
+  shows "val D I \<phi> (\<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>]) = false"
+  using assms(5) lemma_5401_b_variant_1[OF assms(1,2,3,4)] by (simp add: boolean_def) 
+
+(* Corresponds to Andrews' lemma 5401 c *)
+lemma lemma_5401_c:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  shows "val D I \<phi> T = true"
+  using assms lemma_5401_b[OF assms(1,2)] unfolding T_def by auto
+
+(* Corresponds to Andrews' lemma 5401 d *)
+lemma lemma_5401_d:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  shows "val D I \<phi> F = false"
+proof -
+  have "iden boolset \<in>: D ooo"
+    using assms general_model.simps wf_interp.simps wf_frame_def by metis
+  then have "(val D I \<phi> \<^bold>[\<^bold>\<lambda>''x'':Tv. T\<^bold>]) \<cdot> false \<noteq> (val D I \<phi> \<^bold>[\<^bold>\<lambda>''x'':Tv. x\<^sub>o\<^bold>]) \<cdot> false" 
+    using assms wf_interp.simps wf_frame_def true_neq_false 
+      apply_id[of "iden boolset" "(D ooo)" "iden boolset"]
+    unfolding boolean_def Eql_def T_def by auto
+  then have neqLR: "val D I \<phi> \<^bold>[\<^bold>\<lambda>''x'':Tv. T\<^bold>] \<noteq> val D I \<phi> \<^bold>[\<^bold>\<lambda>''x'':Tv. x\<^sub>o\<^bold>]"
+    by metis
+  have "val D I \<phi> F = boolean (val D I \<phi> (\<^bold>[\<^bold>\<lambda>''x'':Tv. T\<^bold>]) = val D I \<phi> \<^bold>[\<^bold>\<lambda>''x'':Tv. x\<^sub>o\<^bold>])"
+    using lemma_5401_b_variant_1[OF assms(1,2), 
+        of "oo" "(\<^bold>[\<^bold>\<lambda>''x'':Tv. T\<^bold>])" "\<^bold>[\<^bold>\<lambda>''x'':Tv. x\<^sub>o\<^bold>]"] assms
+    by auto
+  also
+  have "... = boolean False"
+    using neqLR by auto
+  also
+  have "... = false"
+    unfolding boolean_def by auto
+  finally
+  show ?thesis
+    by auto
+qed
+
+lemma asg_into_interp_fun_upd_true:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  shows "asg_into_interp (\<phi>((x, Tv) := true)) D I"
+  using asg_into_interp_fun_upd[OF assms wff_T, of x] lemma_5401_c[OF assms(1,2)] by auto
+
+lemma asg_into_interp_fun_upd_false:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  shows "asg_into_interp (\<phi>((x, Tv) := false)) D I"
+  using asg_into_interp_fun_upd[OF assms wff_F, of x] lemma_5401_d[OF assms] by auto
+
+(* Corresponds to Andrews' lemma 5401 e_1 *)
+lemma lemma_5401_e_1:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  shows "(val D I \<phi> Con_sym) \<cdot> true \<cdot> true = true"
+proof -
+  define \<phi>' where "\<phi>' \<equiv> \<phi>((''x'',Tv) := val D I \<phi> T)"
+  define \<phi>'' where "\<phi>'' \<equiv> \<phi>'((''y'',Tv) :=  val D I \<phi>' T)"
+  define \<phi>''' where "\<phi>''' \<equiv> \<lambda>z. \<phi>''((''g'', ooo) := z)"
+  have \<phi>'_asg_into: "asg_into_interp \<phi>' D I"
+    unfolding \<phi>'_def using asg_into_interp_fun_upd[OF assms wff_T] by blast
+  have \<phi>''_asg_into: "asg_into_interp \<phi>'' D I"
+    unfolding \<phi>''_def using asg_into_interp_fun_upd[OF assms(1) \<phi>'_asg_into wff_T] by blast
+
+  have "(val D I \<phi> Con_sym) \<cdot> true \<cdot> true = val D I \<phi> (Con_sym \<^bold>\<cdot> T \<^bold>\<cdot> T)"
+    using lemma_5401_c[OF assms(1,2)] by auto
+  also
+  have "... = val D I \<phi> (\<^bold>[\<^bold>\<lambda>''x'':Tv. \<^bold>[\<^bold>\<lambda>''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>]\<^bold>] \<^bold>\<cdot> T \<^bold>\<cdot> T)"
+    unfolding Con_sym_def by auto 
+  also
+  have "... = (val D I \<phi> ((\<^bold>[\<^bold>\<lambda>''x'':Tv. \<^bold>[\<^bold>\<lambda>''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>]\<^bold>] \<^bold>\<cdot> T))) \<cdot> val D I \<phi> T"
+    by simp
+  also
+  have "... = (val D I (\<phi>((''x'',Tv) := val D I \<phi> T)) ((\<^bold>[\<^bold>\<lambda>''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>]))) \<cdot> val D I \<phi> T"
+    by (metis lemma_5401_a[OF assms(1,2)] wff_Con_sym_subterm2 wff_T)
+  also
+  have "... = (val D I \<phi>' ((\<^bold>[\<^bold>\<lambda>''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>]))) \<cdot> val D I \<phi> T"
+    unfolding \<phi>'_def ..
+  also
+  have "... = (val D I \<phi>' ((\<^bold>[\<^bold>\<lambda>''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>]))) \<cdot> val D I \<phi>' T"
+    using \<phi>'_asg_into assms(2) lemma_5401_c[OF assms(1)] by auto
+  also
+  have "... = (val D I \<phi>' (\<^bold>[\<^bold>\<lambda>''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>] \<^bold>\<cdot> T))"
+    by simp
+  also
+  have "... = (val D I (\<phi>'((''y'',Tv) :=  val D I \<phi>' T)) (\<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]))"
+    by (meson \<phi>'_asg_into assms(1) lemma_5401_a[OF assms(1)] wff_Con_sym_subterm1 wff_T)
+  also
+  have "... = (val D I \<phi>'' (\<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]))"
+    unfolding \<phi>''_def ..
+  also
+  have "... = true"
+  proof (rule lemma_5401_b_variant_2[OF assms(1)])
+    show "wff (Tv \<^bold>\<Leftarrow> ooo) \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>]"
+      by auto
+  next
+    show "wff (Tv \<^bold>\<Leftarrow> ooo) \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]"
+      by auto
+  next
+    show "asg_into_frame \<phi>'' D"
+      using \<phi>''_asg_into by blast
+  next
+    have "val D I \<phi>'' \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] = abstract (D ooo) (D Tv)
+                  (\<lambda>z. val D I (\<phi>''((''g'', ooo) := z)) 
+                     (g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T))"
+      by (simp only: val.simps(4) type_of.simps type_sym.case)
+    also
+    have "... = abstract (D ooo) (D Tv) 
+                  (\<lambda>z. val D I (\<phi>''' z) (g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T))"
+      unfolding \<phi>'''_def ..
+    also
+    have "... = abstract (D ooo) (D Tv) 
+                  (\<lambda>z. val D I (\<phi>''' z) g\<^sub>o\<^sub>o\<^sub>o \<cdot> val D I (\<phi>''' z) T
+                     \<cdot> val D I (\<phi>''' z) T)"
+      unfolding val.simps(3) ..
+    also
+    have "... = abstract (D ooo) (D Tv) 
+                  (\<lambda>z. val D I (\<phi>''' z) g\<^sub>o\<^sub>o\<^sub>o \<cdot> true \<cdot> true)"
+    proof (rule abstract_extensional')
+      fix x
+      assume "x \<in>: D ooo"
+      then have "val D I (\<phi>''' x) (g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T) \<in>: D Tv"
+        using \<phi>'''_def \<phi>''_asg_into asg_into_frame_fun_upd assms(1) 
+          general_model.elims(2) type_sym.inject wff_Abs_type_of wff_Con_sym_subterm0 wff_T 
+        by (metis wff_App wff_Var)
+      then show "val D I (\<phi>''' x) g\<^sub>o\<^sub>o\<^sub>o \<cdot> val D I (\<phi>''' x) T \<cdot>
+                   val D I (\<phi>''' x) T
+                 \<in>: D Tv"
+        by simp
+    next
+      fix x
+      assume "x \<in>: D ooo"
+      then have "val D I (\<phi>''' x) T = true"
+        unfolding \<phi>'''_def using  \<phi>''_asg_into asg_into_frame_fun_upd 
+          lemma_5401_c[OF assms(1)] by blast
+      then show "val D I (\<phi>''' x) g\<^sub>o\<^sub>o\<^sub>o \<cdot> val D I (\<phi>''' x) T \<cdot>
+                   val D I (\<phi>''' x) T =
+                 val D I (\<phi>''' x) g\<^sub>o\<^sub>o\<^sub>o \<cdot> true \<cdot> true" by auto
+    qed
+    also
+    have "... = abstract (D ooo) (D Tv) 
+                  (\<lambda>z. val D I (\<phi>''' z) g\<^sub>o\<^sub>o\<^sub>o \<cdot>
+                         val D I (\<phi>''' z) x\<^sub>o \<cdot> val D I (\<phi>''' z) y\<^sub>o)"
+    proof (rule abstract_extensional')
+      fix x
+      assume x_in_D: "x \<in>: D ooo"
+      then have "val D I (\<phi>''' x) (g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T) \<in>: D Tv"
+        using \<phi>'''_def \<phi>''_asg_into asg_into_frame_fun_upd assms(1) 
+          general_model.elims(2) type_sym.inject wff_Abs_type_of wff_Con_sym_subterm0 wff_T 
+        by (metis wff_App wff_Var)
+      then have "val D I (\<phi>''' x) g\<^sub>o\<^sub>o\<^sub>o \<cdot> val D I (\<phi>''' x) T \<cdot>
+                   val D I (\<phi>''' x) T \<in>: D Tv"
+        by simp
+      then show "val D I (\<phi>''' x) g\<^sub>o\<^sub>o\<^sub>o \<cdot> true \<cdot> true \<in>: D Tv"
+        by (metis \<phi>'''_def \<phi>''_asg_into lemma_5401_c[OF assms(1)] asg_into_frame_fun_upd x_in_D)
+    next
+      fix x
+      assume x_in_D: "x \<in>: D ooo"
+      then have "val D I (\<phi>''' x) x\<^sub>o = true"
+        unfolding \<phi>'''_def \<phi>''_def \<phi>'_def using lemma_5401_c[OF assms(1,2)] by auto
+      moreover
+      from x_in_D have "val D I (\<phi>''' x) y\<^sub>o = true"
+        unfolding \<phi>'''_def \<phi>''_def using \<phi>'_asg_into lemma_5401_c[OF assms(1)] by auto
+      ultimately
+      show "val D I (\<phi>''' x) g\<^sub>o\<^sub>o\<^sub>o \<cdot> true \<cdot> true =
+        val D I (\<phi>''' x)
+          g\<^sub>o\<^sub>o\<^sub>o \<cdot>
+            val D I (\<phi>''' x) x\<^sub>o \<cdot> val D I (\<phi>''' x) y\<^sub>o" 
+        by auto
+    qed
+    also
+    have "... = abstract (D ooo) (D Tv) (\<lambda>z. val D I (\<phi>''' z)
+                  (g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o))"
+      unfolding val.simps(3) ..
+    also
+    have "... = abstract (D ooo) (D Tv)
+                  (\<lambda>z. val D I (\<phi>''((''g'', ooo) := z)) 
+                         (g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o))"
+      unfolding \<phi>'''_def ..
+    also
+    have "... = val D I \<phi>'' \<^bold>[\<^bold>\<lambda>''g'':ooo.
+                                g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]"
+      by (simp only: val.simps(4) type_of.simps type_sym.case)
+    finally
+    show "val D I \<phi>'' \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] = val D I \<phi>'' \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]" 
+      .
+  qed
+  finally show ?thesis .
+qed
+
+(* Corresponds to Andrews' lemma 5401 e_2 *)
+lemma lemma_5401_e_2:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "y = true \<or> y = false"
+  shows "(val D I \<phi> Con_sym) \<cdot> false \<cdot> y = false"
+proof -
+  define give_x :: trm where "give_x = \<^bold>[\<^bold>\<lambda>''y'':Tv. x\<^sub>o\<^bold>]"
+  define give_fst :: trm where "give_fst = \<^bold>[\<^bold>\<lambda> ''x'':Tv. give_x\<^bold>]"
+  define val_give_fst :: 's where "val_give_fst = val D I \<phi> give_fst"
+  have wff_give_x: "wff oo give_x"
+    unfolding give_x_def by auto
+
+  have "\<And>a b. a \<in>: D Tv \<Longrightarrow> 
+               b \<in>: D Tv \<Longrightarrow> 
+               val D I (\<phi>((''x'', Tv) := a)) give_x \<in>: D (type_of give_x)"
+    using wff_give_x asg_into_frame_def assms(1,2) by auto
+  moreover
+  have "\<And>a b. a \<in>: D Tv \<Longrightarrow> b \<in>: D Tv \<Longrightarrow> val D I (\<phi>((''x'', Tv) := a)) give_x \<cdot> b = a"
+    unfolding give_x_def by auto
+  ultimately
+  have "\<And>a b. a \<in>: D Tv \<Longrightarrow>
+               b \<in>: D Tv \<Longrightarrow> 
+               abstract (D Tv) (D (type_of give_x)) (\<lambda>z. val D I (\<phi>((''x'', Tv) := z)) give_x) \<cdot> a \<cdot> b
+               = a"
+    by auto
+  then have val_give_fst_simp: "\<And>a b. a \<in>: D Tv \<Longrightarrow> b \<in>: D Tv \<Longrightarrow> val_give_fst \<cdot> a \<cdot> b = a"
+    unfolding val_give_fst_def give_fst_def by auto
+
+  have wff_give_fst: "wff ooo give_fst"
+    unfolding give_fst_def give_x_def by auto
+  then have val_give_fst_fun: "val_give_fst \<in>: D ooo"
+    unfolding val_give_fst_def using assms by auto
+
+  have "val D I (\<phi>((''x'', Tv) := false, 
+                   (''y'', Tv) := y, 
+                   (''g'', ooo) := val_give_fst)) T \<in>: D Tv"
+    by (smt Pair_inject wff_give_fst assms(1,2,3) fun_upd_twist general_model.simps
+        asg_into_interp_fun_upd[OF assms(1,2)] asg_into_interp_fun_upd_true[OF assms(1)] 
+        asg_into_interp_fun_upd_false[OF assms(1)] type_sym.distinct(5) val_give_fst_def wff_T)
+  then have val_give_fst_D:
+    "val_give_fst \<cdot> val D I (\<phi>((''x'', Tv) := false, 
+                               (''y'', Tv) := y, 
+                               (''g'', ooo) := val_give_fst)) T \<cdot>
+                      val D I (\<phi>((''x'', Tv) := false, 
+                               (''y'', Tv) := y, 
+                               (''g'', ooo) := val_give_fst)) T
+       \<in>: D Tv"
+    using val_give_fst_simp[of
+        "val D I (\<phi>((''x'', Tv) := false, 
+                    (''y'', Tv) := y, 
+                    (''g'', ooo) := val_give_fst)) T" 
+        "val D I (\<phi>((''x'', Tv) := false, 
+                     (''y'', Tv) := y, 
+                     (''g'', ooo) := val_give_fst)) T" ]
+    by auto
+
+  have false_y_TV: "false \<in>: D Tv \<and> y \<in>: D Tv"
+    using assms(1) assms(3) wf_frame_def wf_interp.simps by auto
+  then have val_give_fst_in_D: "val_give_fst \<cdot> false \<cdot> y \<in>: D Tv"
+    using val_give_fst_simp by auto
+
+  have "true \<in>: D Tv"
+    by (metis assms(1) assms(2) general_model.simps lemma_5401_c[OF assms(1,2)] wff_T)
+  from this val_give_fst_in_D false_y_TV have "val_give_fst \<cdot> true \<cdot> true \<noteq> val_give_fst \<cdot> false \<cdot> y"
+    using val_give_fst_simp true_neq_false by auto
+  then have val_give_fst_not_false: 
+    "val_give_fst \<cdot> val D I (\<phi>((''x'', Tv) := false, 
+                             (''y'', Tv) := y, 
+                             (''g'', ooo) := val_give_fst)) T
+                  \<cdot> val D I (\<phi>((''x'', Tv) := false, 
+                             (''y'', Tv) := y, 
+                             (''g'', ooo) := val_give_fst)) T 
+     \<noteq> val_give_fst \<cdot> false \<cdot> y"
+    using asg_into_frame_fun_upd assms(1) assms(2) lemma_5401_c false_y_TV val_give_fst_fun by auto
+  have Con_sym_subterm0TT_neq_Con_sym_subterm0xy: 
+    "val D I (\<phi>((''x'', Tv) := false, (''y'', Tv) := y)) \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<noteq> 
+     val D I (\<phi>((''x'', Tv) := false, (''y'', Tv) := y)) \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]"
+    using abstract_cong_specific[of
+        val_give_fst
+        "(D ooo)" 
+        "(\<lambda>z. z \<cdot> val D I (\<phi>((''x'', Tv) := false, 
+                           (''y'', Tv) := y, 
+                           (''g'', ooo) := z)) T
+                 \<cdot> val D I (\<phi>((''x'', Tv) := false, 
+                            (''y'', Tv) := y, 
+                            (''g'', ooo) := z)) T)" 
+        "(D Tv)"
+        "(\<lambda>z. z \<cdot> false \<cdot> y)"]
+    using val_give_fst_fun val_give_fst_D val_give_fst_in_D val_give_fst_not_false by auto
+
+  have "asg_into_frame (\<phi>((''x'', Tv) := false, (''y'', Tv) := y)) D"
+    using asg_into_interp_fun_upd_false[OF assms(1)] general_model.simps[of D I] assms wff_Con_sym_subterm1
+      asg_into_interp_fun_upd_true[OF assms(1)] by auto
+  then have val_Con_sym_subterm1: "val D I (\<phi>((''x'', Tv) := false, (''y'', Tv) := y)) \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>] = false"
+    using Con_sym_subterm0TT_neq_Con_sym_subterm0xy lemma_5401_b_variant_3[OF assms(1)] 
+    by auto
+
+  have "y \<in>: D Tv"
+    using general_model.simps lemma_5401_d[OF assms(1,2)] wff_F assms
+    by (metis lemma_5401_c[OF assms(1,2)] wff_T) 
+  moreover
+  have "val D I (\<phi>((''x'', Tv) := false, (''y'', Tv) := y)) \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>] \<in>: D Tv"
+    using asg_into_interp_fun_upd_false[OF assms(1)] general_model.simps[of D I] assms wff_Con_sym_subterm1 
+      asg_into_interp_fun_upd_true[OF assms(1)] by auto
+  moreover
+  have "val D I (\<phi>((''x'', Tv) := false, (''y'', Tv) := y)) \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>] = false"
+    using val_Con_sym_subterm1 by auto
+  ultimately
+  have val_y: "(val D I (\<phi>((''x'', Tv) := false)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>]) \<cdot> y = false"
+    by simp
+
+  have 11: "val D I (\<phi>((''x'', Tv) := false)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>] \<in>: D oo"
+    using asg_into_interp_fun_upd_false[OF assms(1,2)] general_model.simps[of D I] assms
+      wff_Con_sym_subterm2 by blast 
+  moreover
+  have "val D I (\<phi>((''x'', Tv) := false)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>] \<cdot> y = false"
+    using val_y by auto
+  ultimately
+  have "(val D I \<phi> \<^bold>[\<^bold>\<lambda>''x'':Tv. \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>]\<^bold>]) \<cdot> false \<cdot> y = false"
+    using false_y_TV by simp
+  then show "(val D I \<phi> Con_sym) \<cdot> false \<cdot> y = false"
+    unfolding Con_sym_def by auto
+qed
+
+(* Corresponds to Andrews' lemma 5401 e_3 *)
+lemma lemma_5401_e_3:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "x = true \<or> x = false"
+  shows "(val D I \<phi> Con_sym) \<cdot> x \<cdot> false = false"
+proof -
+  (* proof adapted from lemma_5401_e_2 *)
+  define give_y :: trm where "give_y = (\<^bold>[\<^bold>\<lambda> ''y'':Tv. y\<^sub>o\<^bold>])"
+  define give_snd :: trm where "give_snd = \<^bold>[\<^bold>\<lambda> ''x'':Tv. give_y\<^bold>]"
+  define val_give_snd :: 's where "val_give_snd = val D I \<phi> give_snd"
+  have wff_give_y: "wff oo give_y"
+    unfolding give_y_def by auto
+
+  have  "\<And>a b. a \<in>: D Tv \<Longrightarrow> b \<in>: D Tv \<Longrightarrow> a \<in>: D Tv"
+    by simp
+  moreover
+  have "\<And>a b. a \<in>: D Tv \<Longrightarrow> b \<in>: D Tv \<Longrightarrow> val D I (\<phi>((''x'', Tv) := a)) give_y \<in>: D (type_of give_y)"
+    using wff_give_y asg_into_frame_def assms(1) assms(2) by auto
+  moreover
+  have "\<And>a b. a \<in>: D Tv \<Longrightarrow> b \<in>: D Tv \<Longrightarrow> val D I (\<phi>((''x'', Tv) := a)) give_y \<cdot> b = b"
+    unfolding give_y_def by auto
+  ultimately
+  have val_give_snd_simp: "\<And>a b. a \<in>: D Tv \<Longrightarrow> b \<in>: D Tv \<Longrightarrow> val_give_snd \<cdot> a \<cdot> b = b"
+    unfolding val_give_snd_def give_snd_def by auto
+
+  have wff_give_snd: "wff ooo give_snd"
+    unfolding give_snd_def give_y_def by auto
+  then have val_give_snd_in_D: "val_give_snd \<in>: D ooo"
+    unfolding val_give_snd_def using assms
+    by auto
+
+  then have "val D I (\<phi>((''x'', Tv) := x, 
+                   (''y'', Tv) := false, 
+                   (''g'', ooo) := val_give_snd)) T \<in>: D Tv"
+    by (smt Pair_inject wff_give_snd assms(1,2,3) 
+        fun_upd_twist general_model.simps asg_into_interp_fun_upd[OF assms(1,2)] 
+        asg_into_interp_fun_upd_false[OF assms(1)] asg_into_interp_fun_upd_true[OF assms(1)] 
+        type_sym.distinct(5) val_give_snd_def wff_T)
+  then have val_give_snd_app_in_D: 
+    "val_give_snd \<cdot> val D I (\<phi>((''x'', Tv) := x, 
+                             (''y'', Tv) := false, 
+                             (''g'', ooo) := val_give_snd)) T
+                  \<cdot> val D I (\<phi>((''x'', Tv) := x, 
+                             (''y'', Tv) := false, 
+                             (''g'', ooo) := val_give_snd)) T
+     \<in>: D Tv"
+    using val_give_snd_simp[of
+        "val D I (\<phi>((''x'', Tv) := x, 
+                    (''y'', Tv) := false, 
+                    (''g'', ooo) := val_give_snd)) T" 
+        "val D I (\<phi>((''x'', Tv) := x, 
+                     (''y'', Tv) := false, 
+                     (''g'', ooo) := val_give_snd)) T" ]
+    by auto
+
+  have false_and_x_in_D: "false \<in>: D Tv \<and> x \<in>: D Tv"
+    using assms(1,3) wf_frame_def wf_interp.simps by auto
+  then have val_give_snd_app_x_false_in_D: "val_give_snd \<cdot> x \<cdot> false \<in>: D Tv"
+    using val_give_snd_simp by auto
+
+  have "true \<in>: D Tv"
+    by (metis assms(1) assms(2) general_model.simps lemma_5401_c[OF assms(1,2)] wff_T)
+  then have "val_give_snd \<cdot> true \<cdot> true \<noteq> val_give_snd \<cdot> x \<cdot> false"
+    using val_give_snd_simp true_neq_false val_give_snd_app_in_D false_and_x_in_D by auto
+  then have
+    "val_give_snd \<cdot> val D I (\<phi>((''x'', Tv) := x, 
+                             (''y'', Tv) := false, 
+                             (''g'', ooo) := val_give_snd)) T
+                  \<cdot> val D I (\<phi>((''x'', Tv) := x, 
+                             (''y'', Tv) := false, 
+                             (''g'', ooo) := val_give_snd)) T \<noteq>
+     val_give_snd \<cdot> x \<cdot> false"
+    using asg_into_frame_fun_upd assms(1) assms(2) lemma_5401_c false_and_x_in_D val_give_snd_in_D
+    by auto
+  then have "val D I (\<phi>((''x'', Tv) := x, (''y'', Tv) := false)) \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<noteq> 
+        val D I (\<phi>((''x'', Tv) := x, (''y'', Tv) := false)) 
+          \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]"
+    using abstract_cong_specific[of 
+        val_give_snd 
+        "(D ooo)" 
+        "(\<lambda>z. z \<cdot> val D I (\<phi>((''x'', Tv) := x, (''y'', Tv) := false, (''g'', ooo) := z))
+             T \<cdot> val D I (\<phi>((''x'', Tv) := x, (''y'', Tv) := false, (''g'', ooo) := z)) T)" 
+        "(D Tv)"
+        "(\<lambda>z. z \<cdot> x \<cdot> false)"
+        ]
+    using val_give_snd_in_D val_give_snd_app_x_false_in_D val_give_snd_app_in_D by auto
+  then have "val D I (\<phi>((''x'', Tv) := x, (''y'', Tv) := false)) \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>] = false"
+    using asg_into_frame_fun_upd assms(1,2) lemma_5401_b_variant_3 false_and_x_in_D by auto
+  then have val_Con_sym_subterm2_false: "(val D I (\<phi>((''x'', Tv) := x)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>]) \<cdot> false = false"
+    using false_and_x_in_D by simp
+
+  have "x \<in>: D Tv"
+    by (simp add: false_and_x_in_D)
+  moreover
+  have "val D I (\<phi>((''x'', Tv) := x)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>] \<in>: D oo"
+    by (metis assms(1,3) general_model.simps lemma_5401_c[OF assms(1,2)] 
+        asg_into_interp_fun_upd[OF assms(1,2)] asg_into_interp_fun_upd_false[OF assms(1,2)] 
+        wff_Con_sym_subterm2 wff_T)
+  moreover
+  have "val D I (\<phi>((''x'', Tv) := x)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>] \<cdot> false = false"
+    using val_Con_sym_subterm2_false by auto
+  ultimately
+  have "(val D I \<phi> \<^bold>[\<^bold>\<lambda>''x'':Tv. \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[\<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> T \<^bold>\<cdot> T\<^bold>] \<^bold>=(Tv \<^bold>\<Leftarrow> ooo)\<^bold>= \<^bold>[\<^bold>\<lambda>''g'':ooo. g\<^sub>o\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o \<^bold>\<cdot> y\<^sub>o\<^bold>]\<^bold>]\<^bold>]\<^bold>]) \<cdot> x \<cdot> false = false"
+    by auto
+  then show "(val D I \<phi> Con_sym) \<cdot> x \<cdot> false = false"
+    unfolding Con_sym_def by auto
+qed
+
+(* Corresponds to Andrews' lemma 5401 e *)
+lemma lemma_5401_e_variant_1:
+  assumes "asg_into_interp \<phi> D I"
+  assumes "general_model D I"
+  assumes "y = true \<or> y = false"
+  assumes "x = true \<or> x = false"
+  shows "(val D I \<phi> Con_sym) \<cdot> x \<cdot> y = boolean (x = true \<and> y = true)"
+proof (cases "y = true")
+  case True
+  note True_outer = this
+  then show ?thesis
+  proof (cases "x = true")
+    case True
+    then show ?thesis
+      using True_outer assms lemma_5401_e_1 unfolding boolean_def by auto
+  next
+    case False
+    then show ?thesis
+      using True_outer assms  lemma_5401_e_2 unfolding boolean_def by auto
+  qed
+next
+  case False
+  note False_outer = this
+  then show ?thesis 
+  proof (cases "x = true")
+    case True
+    then show ?thesis
+      using False_outer assms lemma_5401_e_3 unfolding boolean_def by auto
+  next
+    case False
+    then show ?thesis
+      using False_outer assms lemma_5401_e_2 unfolding boolean_def by auto
+  qed
+qed
+
+lemma asg_into_interp_is_true_or_false:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  shows "\<phi> (x, Tv) = true \<or> \<phi> (x, Tv) = false"
+proof -
+  have "wff Tv (Var x Tv)"
+    by auto
+  then have "val D I \<phi> (Var x Tv) \<in>: D Tv"
+    using assms general_model.simps by blast
+  then have "val D I \<phi> (Var x Tv) \<in>: boolset"
+    using assms unfolding general_model.simps wf_interp.simps wf_frame_def by auto
+  then show ?thesis
+    using mem_boolset by simp 
+qed
+
+lemma wff_Tv_is_true_or_false:
+  assumes "asg_into_interp \<phi> D I"
+  assumes "general_model D I"
+  assumes "wff Tv A"
+  shows "val D I \<phi> A = true \<or> val D I \<phi> A = false"
+proof -
+  have "val D I \<phi> A \<in>: D Tv"
+    using assms by auto
+  then have "val D I \<phi> A \<in>: boolset"
+    using assms unfolding general_model.simps wf_interp.simps wf_frame_def by force
+  then show ?thesis
+    using mem_boolset by blast
+qed
+
+(* Corresponds to Andrews' lemma 5401 e *)
+lemma lemma_5401_e_variant_2:
+  assumes "asg_into_interp \<phi> D I"
+  assumes "general_model D I"
+  assumes "wff Tv A"
+  assumes "wff Tv B"
+  shows "(val D I \<phi> (A \<^bold>\<and> B)) = boolean (satisfies D I \<phi> A \<and> satisfies D I \<phi> B)"
+  using assms wff_Tv_is_true_or_false[of \<phi> D I] lemma_5401_e_variant_1 unfolding Con_def by auto
+
+(* Corresponds to Andrews' lemma 5401 f_1 *)
+lemma lemma_5401_f_1:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "y = true \<or> y = false"
+  shows "(val D I \<phi> Imp_sym) \<cdot> false \<cdot> y = true"
+proof -
+  define Imp_subterm2 :: trm where
+    "Imp_subterm2 \<equiv> \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>]"
+
+  have val_Imp_subterm0_false: "val D I (\<phi>((''x'', Tv) := false, (''y'', Tv) := y)) (x\<^sub>o \<^bold>\<and> y\<^sub>o) = false"
+    using assms asg_into_interp_fun_upd_false[OF assms(1)] asg_into_interp_fun_upd_true[OF assms(1)] 
+      boolean_def lemma_5401_e_variant_2 by auto
+
+  have "asg_into_frame (\<phi>((''x'', Tv) := false, (''y'', Tv) := y)) D"
+    using assms(1, 2, 3) lemma_5401_c[OF assms(1)] asg_into_interp_fun_upd wff_T
+      asg_into_interp_fun_upd_false by metis
+  then have "val D I (\<phi>((''x'', Tv) := false, (''y'', Tv) := y)) \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>] = true"
+    using lemma_5401_b_variant_1[OF assms(1)] val_Imp_subterm0_false unfolding boolean_def by auto
+  then have val_Imp_subterm2_true: "(val D I (\<phi>((''x'', Tv) := false)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>]) \<cdot> y = true"
+    using assms(1,3) wf_frame_def wf_interp.simps by auto 
+
+  have "val D I \<phi> \<^bold>[\<^bold>\<lambda> ''x'':Tv. \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>]\<^bold>] \<cdot> false \<cdot> y = true"
+  proof -
+    have "false \<in>: D Tv"
+      by (metis asg_into_frame_def asg_into_interp_fun_upd_false assms(1) assms(2) fun_upd_same)
+    then have "val D I (\<phi>((''x'', Tv) := false)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>] = val D I \<phi> \<^bold>[\<^bold>\<lambda>''x'':Tv. \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>]\<^bold>] \<cdot> false"
+      using asg_into_interp_fun_upd_false assms(1,2) Imp_subterm2_def[symmetric] wff_Imp_sym_subterm2_iff by force
+    then show ?thesis
+      by (metis val_Imp_subterm2_true)
+  qed
+  then show "(val D I \<phi> Imp_sym) \<cdot> false \<cdot> y = true"
+    unfolding Imp_sym_def Imp_subterm2_def by auto
+qed
+
+(* Corresponds to Andrews' lemma 5401 f_2 *)
+lemma lemma_5401_f_2:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "x = true \<or> x = false"
+  shows "(val D I \<phi> Imp_sym) \<cdot> x \<cdot> true = true"
+proof -
+  have asg: "asg_into_frame (\<phi>((''x'', Tv) := x, (''y'', Tv) := true)) D"
+    using assms(1,2,3) asg_into_interp_fun_upd_false asg_into_interp_fun_upd_true[OF assms(1)] by blast
+  then have "val D I (\<phi>((''x'', Tv) := x, (''y'', Tv) := true)) (x\<^sub>o \<^bold>\<and> y\<^sub>o) = x"
+    using lemma_5401_e_variant_2 assms unfolding boolean_def by auto
+  then have val_Imp_subterm1_true: "val D I (\<phi>((''x'', Tv) := x, (''y'', Tv) := true)) \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>] = true"
+    using asg lemma_5401_b_variant_1[OF assms(1)] boolean_eq_true  by auto 
+
+  have val_Imp_subterm2_true: "val D I (\<phi>((''x'', Tv) := x)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>] \<cdot> true = true"
+    using val_Imp_subterm1_true assms(1) wf_frame_def wf_interp.simps by auto 
+
+  have "x \<in>: D Tv"
+    by (metis asg_into_frame_def assms(1) assms(3) fun_upd_same asg_into_interp_fun_upd_false 
+        asg_into_interp_fun_upd_true[OF assms(1,2)])
+  moreover
+  have "val D I (\<phi>((''x'', Tv) := x)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>] \<in>: D oo"
+    using wff_Imp_sym_subterm2
+    by (metis assms(1,2,3) general_model.simps lemma_5401_c[OF assms(1,2)]
+        asg_into_interp_fun_upd[OF assms(1,2)] asg_into_interp_fun_upd_false wff_T)
+  ultimately
+  have "(val D I \<phi> \<^bold>[\<^bold>\<lambda>''x'':Tv. \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>]\<^bold>]) \<cdot> x \<cdot> true = true"
+    using val_Imp_subterm2_true by auto
+  then show "(val D I \<phi> Imp_sym) \<cdot> x \<cdot> true = true"
+    unfolding Imp_sym_def by auto
+qed
+
+(* Corresponds to Andrews' lemma 5401 f_3 *)
+lemma lemma_5401_f_3:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  shows "(val D I \<phi> Imp_sym) \<cdot> true \<cdot> false = false"
+proof -
+  have asg: "asg_into_frame (\<phi>((''x'', Tv) := true, (''y'', Tv) := false)) D"
+    by (meson assms(1,2) asg_into_interp_fun_upd_false asg_into_interp_fun_upd_true)
+  moreover
+  have "false = true \<or> false = false"
+    unfolding boolean_def by auto
+  moreover
+  have "boolean (true = true \<and> false = true) = false"
+    unfolding boolean_def by auto
+  ultimately
+  have 3: "val D I (\<phi>((''x'', Tv) := true, (''y'', Tv) := false)) (x\<^sub>o \<^bold>\<and> y\<^sub>o) = false"
+    using lemma_5401_e_variant_2 assms by auto
+  then have Imp_subterm1_false: "val D I (\<phi>((''x'', Tv) := true, (''y'', Tv) := false)) \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>] = false"
+    using subst lemma_5401_b_variant_1[OF assms(1)] asg boolean_def by auto
+
+  have asdff: "wff Tv \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]"
+    by auto
+
+  have false_Tv: "false \<in>: D Tv"
+    using assms(1) wf_frame_def wf_interp.simps by auto
+  moreover
+  have "val D I (\<phi>((''x'', Tv) := true, (''y'', Tv) := false)) \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>] \<in>: D Tv"
+    by (simp add: Imp_subterm1_false false_Tv)
+  moreover
+  have "val D I (\<phi>((''x'', Tv) := true, (''y'', Tv) := false)) \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>] = false"
+    using Imp_subterm1_false by auto
+  ultimately 
+  have Imp_subterm2_app_false: "val D I (\<phi>((''x'', Tv) := true)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>] \<cdot> false = false"
+    by auto
+
+  have wff_Imp_sym_subterm2: "wff oo \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>]"
+    by auto
+
+  have "(val D I \<phi> \<^bold>[\<^bold>\<lambda> ''x'':Tv. \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>]\<^bold>]) \<cdot> true \<cdot> false = false"
+  proof -
+    have "true \<in>: D Tv"
+      by (metis assms(1) assms(2) general_model.simps lemma_5401_c[OF assms(1,2)] wff_T)
+    moreover
+    have "val D I (\<phi>((''x'', Tv) := true)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>] \<in>: D oo"
+      using wff_Imp_sym_subterm2 
+      by (metis assms(1) general_model.simps asg_into_interp_fun_upd_true[OF assms(1,2)])
+    moreover
+    have "val D I (\<phi>((''x'', Tv) := true)) \<^bold>[\<^bold>\<lambda> ''y'':Tv. \<^bold>[x\<^sub>o \<^bold>=Tv\<^bold>= (x\<^sub>o \<^bold>\<and> y\<^sub>o)\<^bold>]\<^bold>] \<cdot> false = false"
+      using Imp_subterm2_app_false by auto
+    ultimately
+    show ?thesis
+      by auto
+  qed
+  then show "(val D I \<phi> Imp_sym) \<cdot> true \<cdot> false = false"
+    unfolding Imp_sym_def by auto
+qed
+
+(* Corresponds to Andrews' lemma 5401 f *)
+lemma lemma_5401_f_variant_1:
+  assumes "asg_into_interp \<phi> D I"
+  assumes "general_model D I"
+  assumes "x = true \<or> x = false"
+  assumes "y = true \<or> y = false"
+  shows "(val D I \<phi> Imp_sym) \<cdot> x \<cdot> y = boolean (x = true \<longrightarrow> y = true)"
+proof (cases "y = true")
+  case True
+  note True_outer = this
+  then show ?thesis
+  proof (cases "x = true")
+    case True
+    then show ?thesis
+      using True_outer assms lemma_5401_f_2 unfolding boolean_def by auto
+  next
+    case False
+    then show ?thesis
+      using True_outer assms  lemma_5401_f_2 unfolding boolean_def by auto
+  qed
+next
+  case False
+  note False_outer = this
+  then show ?thesis 
+  proof (cases "x = true")
+    case True
+    then show ?thesis
+      using False_outer assms lemma_5401_f_3 unfolding boolean_def by auto
+  next
+    case False
+    then show ?thesis
+      using False_outer assms lemma_5401_f_1 unfolding boolean_def by auto
+  qed
+qed
+
+(* Corresponds to Andrews' lemma 5401 f *)
+lemma lemma_5401_f_variant_2:
+  assumes "asg_into_interp \<phi> D I"
+  assumes "general_model D I"
+  assumes "wff Tv A"
+  assumes "wff Tv B"
+  shows "(val D I \<phi> (A \<^bold>\<longrightarrow> B)) = boolean (satisfies D I \<phi> A \<longrightarrow> satisfies D I \<phi> B)"
+  using assms unfolding Imp_def
+  by (simp add: lemma_5401_f_variant_1 wff_Tv_is_true_or_false)
+
+(* Corresponds to Andrews' lemma 5401 g *)
+lemma lemma_5401_g:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "wff Tv A"
+  shows "satisfies D I \<phi> \<^bold>[\<^bold>\<forall>x:\<alpha>. A\<^bold>] \<longleftrightarrow> 
+        (\<forall>\<psi>. asg_into_interp \<psi> D I \<longrightarrow> agree_off_asg \<psi> \<phi> x \<alpha> \<longrightarrow> satisfies D I \<psi> A)"
+proof -
+  have "wff (Tv \<^bold>\<Leftarrow> \<alpha>) \<^bold>[\<^bold>\<lambda> ''x'':\<alpha>. T\<^bold>]"
+    by auto
+  then have PI_subterm_in_D: "val D I \<phi> \<^bold>[\<^bold>\<lambda> ''x'':\<alpha>. T\<^bold>] \<in>: D (Tv \<^bold>\<Leftarrow> \<alpha>)"
+    using assms(1,2) general_model.simps by blast
+
+  have "wff (Tv \<^bold>\<Leftarrow> \<alpha>) (\<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>])"
+    using assms by auto
+  moreover
+  have "\<forall>\<phi>. asg_into_frame \<phi> D \<longrightarrow> (\<forall>A \<alpha>. wff \<alpha> A \<longrightarrow> val D I \<phi> A \<in>: D \<alpha>)"
+    using assms(1) by auto
+  then have "\<forall>t cs. val D I \<phi> \<^bold>[\<^bold>\<lambda>cs:t. A\<^bold>] \<in>: D (Tv \<^bold>\<Leftarrow> t)"
+    using wff_Abs assms(1,2,3) by presburger
+  then have "abstract (D \<alpha>) (D Tv) (\<lambda>u. val D I (\<phi>((x, \<alpha>) := u)) A) \<in>: D (Tv \<^bold>\<Leftarrow> \<alpha>)"
+    using assms(3) by simp
+  ultimately
+  have val_lambda_A: "val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>]) \<in>: D (Tv \<^bold>\<Leftarrow> \<alpha>)"
+    using assms by auto
+
+  have true_and_A_in_D: "\<forall>z. z \<in>: D \<alpha> \<longrightarrow> true \<in>: D Tv \<and> val D I (\<phi>((x, \<alpha>) := z)) A \<in>: D Tv"
+    by (metis assms(1,2,3) general_model.simps lemma_5401_c[OF assms(1,2)] asg_into_frame_fun_upd wff_T)
+
+  have "satisfies D I \<phi> \<^bold>[\<^bold>\<forall> x: \<alpha>. A\<^bold>] \<longleftrightarrow> val D I \<phi> \<^bold>[\<^bold>\<forall>x: \<alpha>. A\<^bold>] = true"
+    by auto
+  moreover have "... \<longleftrightarrow> val D I \<phi> (PI \<alpha>) \<cdot> val D I \<phi> \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>] = true"
+    unfolding Forall_def by simp
+  moreover have "... \<longleftrightarrow> I ''Q'' ((Tv \<^bold>\<Leftarrow> (Tv \<^bold>\<Leftarrow> \<alpha>)) \<^bold>\<Leftarrow> (Tv \<^bold>\<Leftarrow> \<alpha>))
+                            \<cdot> val D I \<phi> \<^bold>[\<^bold>\<lambda> ''x'':\<alpha>. T\<^bold>] \<cdot> val D I \<phi> \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>] =
+                         true"
+    unfolding PI_def by simp
+  moreover have "... \<longleftrightarrow> (iden (D (Tv \<^bold>\<Leftarrow> \<alpha>))) \<cdot> val D I \<phi> \<^bold>[\<^bold>\<lambda> ''x'':\<alpha>. T\<^bold>] \<cdot> val D I \<phi> \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>] =
+                         true"
+    unfolding PI_def using wf_interp.simps assms by simp
+  moreover have "... \<longleftrightarrow> val D I \<phi> \<^bold>[\<^bold>\<lambda>''x'':\<alpha>. T\<^bold>] = val D I \<phi> \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>]"
+    using PI_subterm_in_D val_lambda_A apply_id_true by auto
+  moreover have "... \<longleftrightarrow> abstract (D \<alpha>) (D Tv) (\<lambda>z. val D I (\<phi>((''x'', \<alpha>) := z)) T) = val D I \<phi> \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>]"
+    using assms wff_T by simp
+  moreover have "... \<longleftrightarrow> abstract (D \<alpha>) (D Tv) (\<lambda>z. true) = val D I \<phi> \<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>]"
+  proof -
+    have "\<forall>x. x \<in>: D \<alpha> \<longrightarrow> val D I (\<phi>((''x'', \<alpha>) := x)) T \<in>: D Tv \<and> true \<in>: D Tv"
+      using true_and_A_in_D assms(1,2)  asg_into_frame_fun_upd by auto
+    moreover
+    have "\<forall>x. x \<in>: D \<alpha> \<longrightarrow> val D I (\<phi>((''x'', \<alpha>) := x)) T \<in>: D Tv \<and> satisfies D I (\<phi>((''x'', \<alpha>) := x)) T"
+      using true_and_A_in_D assms(1) assms(2) lemma_5401_c[OF assms(1)] asg_into_frame_fun_upd by auto
+    ultimately
+    have "abstract (D \<alpha>) (D Tv) (\<lambda>z. val D I (\<phi>((''x'', \<alpha>) := z)) T) = abstract (D \<alpha>) (D Tv) (\<lambda>z. true)"
+      using abstract_extensional by auto
+    then show ?thesis
+      by auto
+  qed
+  moreover have "... \<longleftrightarrow> abstract (D \<alpha>) (D Tv) (\<lambda>z. true) = val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. A\<^bold>])"
+    by auto
+  moreover have "... \<longleftrightarrow> abstract (D \<alpha>) (D Tv) (\<lambda>z. true) = 
+                         abstract (D \<alpha>) (D Tv) (\<lambda>z. val D I (\<phi>((x, \<alpha>) := z)) A)"
+    using assms by simp
+  moreover have "... \<longleftrightarrow> (\<forall>z. z \<in>: D \<alpha> \<longrightarrow> true \<in>: D Tv \<and> true = val D I (\<phi>((x, \<alpha>) := z)) A)"
+  proof -
+    have "\<forall>z. z \<in>: D \<alpha> \<longrightarrow> true \<in>: D Tv \<and> val D I (\<phi>((x, \<alpha>) := z)) A \<in>: D Tv"
+      using true_and_A_in_D by auto
+    then show ?thesis
+      using abstract_iff_extensional by auto
+  qed
+  moreover have "... \<longleftrightarrow> (\<forall>z. z \<in>: D \<alpha> \<longrightarrow> true = val D I (\<phi>((x, \<alpha>) := z)) A)"
+    by (metis assms(1,2) general_model.simps lemma_5401_c[OF assms(1,2)] wff_T)
+  moreover have "... \<longleftrightarrow> (\<forall>z. z \<in>: D \<alpha> \<longrightarrow> satisfies D I (\<phi>((x, \<alpha>) := z)) A)"
+    by auto
+  moreover have "... \<longleftrightarrow> (\<forall>\<psi>. asg_into_interp \<psi> D I \<longrightarrow> agree_off_asg \<psi> \<phi> x \<alpha> \<longrightarrow> satisfies D I \<psi> A)"
+  proof -
+    show ?thesis
+    proof
+      assume A_sat: "\<forall>z. z \<in>: D \<alpha> \<longrightarrow> satisfies D I (\<phi>((x, \<alpha>) := z)) A"
+      show "\<forall>\<psi>. asg_into_frame \<psi> D \<longrightarrow> agree_off_asg \<psi> \<phi> x \<alpha> \<longrightarrow> satisfies D I \<psi> A"
+      proof (rule; rule; rule)
+        fix \<psi>
+        assume a1: "asg_into_frame \<psi> D"
+        assume a2: "agree_off_asg \<psi> \<phi> x \<alpha>"
+        have "\<exists>xa. (\<phi>((x, \<alpha>) := xa)) = \<psi>"
+          using a1 a2 agree_off_asg_def2 by blast
+        then show "satisfies D I \<psi> A"
+          using A_sat a1 a2 by (metis asg_into_frame_def fun_upd_same)
+      qed
+    next
+      assume "\<forall>\<psi>. asg_into_frame \<psi> D \<longrightarrow> agree_off_asg \<psi> \<phi> x \<alpha> \<longrightarrow> satisfies D I \<psi> A"
+      then show "\<forall>z. z \<in>: D \<alpha> \<longrightarrow> satisfies D I (\<phi>((x, \<alpha>) := z)) A"
+        using asg_into_frame_fun_upd asg_into_interp_fun_upd[OF assms(1,2)] assms(2) fun_upd_other 
+        unfolding agree_off_asg_def by auto
+    qed
+  qed
+  ultimately show ?thesis
+    by auto
+qed
+
+(* Corresponds to Andrews' lemma 5401 g *)
+theorem lemma_5401_g_variant_1:
+  assumes "asg_into_interp \<phi> D I"
+  assumes "general_model D I"
+  assumes "wff Tv A"
+  shows "val D I \<phi> \<^bold>[\<^bold>\<forall>x:\<alpha>. A\<^bold>] =
+        boolean (\<forall>\<psi>. asg_into_interp \<psi> D I \<longrightarrow> agree_off_asg \<psi> \<phi> x \<alpha> \<longrightarrow> satisfies D I \<psi> A)"
+proof -
+  have "val D I \<phi> \<^bold>[\<^bold>\<forall>x:\<alpha>. A\<^bold>] = (if satisfies D I \<phi> \<^bold>[\<^bold>\<forall>x:\<alpha>. A\<^bold>] then true else false)"
+    using assms wff_Forall wff_Tv_is_true_or_false by metis
+  then show ?thesis
+    using assms lemma_5401_g[symmetric] unfolding boolean_def by auto
+qed
+
+
+section \<open>Soundness\<close>
+
+lemma fun_sym_asg_to_funspace:
+  assumes "asg_into_frame \<phi> D"
+  assumes "general_model D I"
+  shows "\<phi> (f, \<alpha> \<^bold>\<Leftarrow> \<beta>) \<in>: funspace (D \<beta>) (D \<alpha>)"
+proof -
+  have "wff (\<alpha> \<^bold>\<Leftarrow> \<beta>) (Var f (\<alpha> \<^bold>\<Leftarrow> \<beta>))"
+    by auto
+  then have "val D I \<phi> (Var f (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<in>: D (\<alpha> \<^bold>\<Leftarrow> \<beta>)"
+    using assms
+    using general_model.simps by blast
+  then show "\<phi> (f, \<alpha> \<^bold>\<Leftarrow> \<beta>) \<in>: funspace (D \<beta>) (D \<alpha>)"
+    using assms unfolding general_model.simps wf_interp.simps wf_frame_def
+    by (simp add: subs_def)
+qed
+
+lemma fun_sym_interp_to_funspace:
+  assumes "asg_into_frame \<phi> D"
+  assumes "general_model D I"
+  shows "I f (\<alpha> \<^bold>\<Leftarrow> \<beta>) \<in>: funspace (D \<beta>) (D \<alpha>)"
+proof -
+  have "wff (\<alpha> \<^bold>\<Leftarrow> \<beta>) (Cst f (\<alpha> \<^bold>\<Leftarrow> \<beta>))"
+    by auto
+  then have "val D I \<phi> (Cst f (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<in>: D (\<alpha> \<^bold>\<Leftarrow> \<beta>)"
+    using assms general_model.simps by blast
+  then show "I f (\<alpha> \<^bold>\<Leftarrow> \<beta>) \<in>: funspace (D \<beta>) (D \<alpha>)"
+    using assms subs_def unfolding general_model.simps wf_interp.simps wf_frame_def by auto
+qed
+
+(* Corresponds to Andrews' theorem 5402 a for rule R *)
+theorem theorem_5402_a_rule_R:
+  assumes A_eql_B: "valid_general (\<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>])"
+  assumes "valid_general C"
+  assumes "rule_R C (\<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>]) C'"
+  assumes "wff \<alpha> A"
+  assumes "wff \<alpha> B"
+  assumes "wff \<beta> C"
+  shows "valid_general C'"
+  unfolding valid_general_def 
+proof (rule allI, rule allI, rule impI)
+  fix D :: "type_sym \<Rightarrow> 's" and I :: "char list \<Rightarrow> type_sym \<Rightarrow> 's"
+  assume DI: "general_model D I"
+  then have "valid_in_model D I (\<^bold>[A \<^bold>=\<alpha>\<^bold>= B\<^bold>])"
+    using A_eql_B unfolding valid_general_def by auto
+  then have x: "\<forall>\<phi>. asg_into_frame \<phi> D \<longrightarrow> (val D I \<phi> A = val D I \<phi> B)"
+    unfolding valid_in_model_def using lemma_5401_b[OF DI, of _ \<alpha> A B ] assms(4,5) by auto
+  have r: "replacement A B C C'"
+    using assms(3) using Eql_def rule_R.cases by fastforce 
+  from r have "\<forall>\<phi>. asg_into_frame \<phi> D \<longrightarrow> (val D I \<phi> C = val D I \<phi> C')"
+    using x assms(4,5,6) 
+  proof (induction arbitrary: \<beta> rule: replacement.induct)
+    case (replace A B)
+    then show ?case by auto
+  next
+    case (replace_App_left A B C E D')
+    define \<alpha>' where "\<alpha>' = type_of C"
+    define \<beta>' where "\<beta>' = type_of D'"
+    show ?case
+    proof (rule, rule)
+      fix \<phi>
+      assume asg: "asg_into_frame \<phi> D"
+      have \<alpha>': "\<alpha>' = \<beta> \<^bold>\<Leftarrow> \<beta>'"
+        using trm.distinct(11) trm.distinct(3,7) trm.inject(3) replace_App_left.prems(4) wff.simps
+        by (metis \<alpha>'_def \<beta>'_def wff_App_type_of)
+      from asg have "wff \<alpha>' C"
+        using replace_App_left trm.distinct(3,7,11) trm.inject(3) wff.simps
+        by (metis \<alpha>' \<beta>'_def type_of wff_App')   
+      then have "val D I \<phi> C = val D I \<phi> E"
+        using asg replace_App_left by auto
+      then show "val D I \<phi> (C \<^bold>\<cdot> D') = val D I \<phi> (E \<^bold>\<cdot> D')"
+        using \<alpha>' by auto
+    qed
+  next
+    case (replace_App_right A B D' E C)
+    define \<alpha>' where "\<alpha>' = type_of C"
+    define \<beta>' where "\<beta>' = type_of D'"
+    show ?case 
+    proof (rule, rule)
+      fix \<phi>
+      assume asg: "asg_into_frame \<phi> D"
+      have \<alpha>': "\<alpha>' = \<beta> \<^bold>\<Leftarrow> \<beta>'"
+        using trm.distinct(11) trm.distinct(3) trm.distinct(7) trm.inject(3) 
+          replace_App_right.prems(4) wff.simps by (metis \<alpha>'_def \<beta>'_def type_of wff_App')
+      from asg have "wff \<beta>' D'"
+        using \<beta>'_def replace_App_right.prems(4) by fastforce
+      then have "val D I \<phi> D' = val D I \<phi> E"
+        using asg replace_App_right by auto
+      then show "val D I \<phi> (C \<^bold>\<cdot> D') = val D I \<phi> (C \<^bold>\<cdot> E)"
+        using \<alpha>' by auto
+    qed
+  next
+    case (replace_Abs A B C D' x \<alpha>')
+    define \<beta>' where "\<beta>' = type_of C"
+    show ?case
+    proof (rule, rule)
+      fix \<phi>
+      assume asg: "asg_into_frame \<phi> D"
+      then have val_C_eql_val_D':
+        "\<forall>z. z \<in>: D \<alpha>' \<longrightarrow> val D I (\<phi>((x, \<alpha>') := z)) C = val D I (\<phi>((x, \<alpha>') := z)) D'"
+        using asg replace_App_right
+        by (metis trm.distinct(11) trm.distinct(5) trm.distinct(9) trm.inject(4) 
+            asg_into_frame_fun_upd replace_Abs.IH replace_Abs.prems(1) replace_Abs.prems(2) 
+            replace_Abs.prems(3) replace_Abs.prems(4) wff.cases)
+
+      have val_C_eql_val_D'_type: 
+        "\<forall>z. z \<in>: D \<alpha>' \<longrightarrow>
+                val D I (\<phi>((x, \<alpha>') := z)) C \<in>: D (type_of C) \<and>
+                  val D I (\<phi>((x, \<alpha>') := z)) C = val D I (\<phi>((x, \<alpha>') := z)) D'"
+      proof (rule; rule)
+        fix z 
+        assume a2: "z \<in>: D \<alpha>'"
+        have "val D I (\<phi>((x, \<alpha>') := z)) C \<in>: D (type_of C)"
+          using DI asg a2 asg_into_frame_fun_upd replace_Abs.prems(4) by auto
+        moreover
+        have "val D I (\<phi>((x, \<alpha>') := z)) C = val D I (\<phi>((x, \<alpha>') := z)) D'"
+          using a2 val_C_eql_val_D' replace_Abs by auto
+        ultimately
+        show
+          "val D I (\<phi>((x, \<alpha>') := z)) C \<in>: D (type_of C) \<and>
+          val D I (\<phi>((x, \<alpha>') := z)) C = val D I (\<phi>((x, \<alpha>') := z)) D'"
+          by auto
+      qed
+      have "wff (type_of C) D'"
+        using replacement_preserves_type replace_Abs.hyps replace_Abs.prems(2) 
+          replace_Abs.prems(3) replace_Abs.prems(4) wff_Abs_type_of by blast
+      then have same_type: 
+        "abstract (D \<alpha>') (D (type_of C)) (\<lambda>z. val D I (\<phi>((x, \<alpha>') := z)) D') =
+         abstract (D \<alpha>') (D (type_of D')) (\<lambda>z. val D I (\<phi>((x, \<alpha>') := z)) D')"
+        using type_of by presburger
+      then show "val D I \<phi> \<^bold>[\<^bold>\<lambda>x:\<alpha>'. C\<^bold>] = val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>'. D'\<^bold>])"
+        using val_C_eql_val_D'_type same_type 
+          abstract_extensional[of _ _ _ "\<lambda>xa. val D I (\<phi>((x, \<alpha>') := xa)) D'"]
+        by (simp add: val_C_eql_val_D'_type same_type)
+    qed
+  qed
+  then show "valid_in_model D I C'"
+    using assms(2) DI unfolding valid_in_model_def valid_general_def by auto
+qed
+
+theorem Fun_Tv_Tv_frame_subs_funspace:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  shows "D oo \<subseteq>: funspace (boolset) (boolset)"
+  by (metis assms(1) general_model.elims(2) wf_frame_def wf_interp.simps)
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 1 *)
+theorem theorem_5402_a_axiom_1_variant:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  shows "satisfies D I \<phi> axiom_1"
+proof (cases "(\<phi> (''g'',oo)) \<cdot> true = true \<and> (\<phi> (''g'',oo)) \<cdot> false = true")
+  case True
+  then have val: "val D I \<phi> ((g\<^sub>o\<^sub>o \<^bold>\<cdot> T) \<^bold>\<and> (g\<^sub>o\<^sub>o \<^bold>\<cdot> F)) = true"
+    using assms lemma_5401_e_variant_2
+    by (auto simp add: boolean_eq_true lemma_5401_c[OF assms(1,2)] lemma_5401_d[OF assms(1,2)])
+  have "\<forall>\<psi>. asg_into_frame \<psi> D \<longrightarrow> 
+            agree_off_asg \<psi> \<phi> ''x'' Tv \<longrightarrow> 
+            satisfies D I \<psi> (g\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o)"
+  proof (rule; rule; rule)
+    fix \<psi>
+    assume \<psi>: "asg_into_frame \<psi> D" "agree_off_asg \<psi> \<phi> ''x'' Tv"
+    then have "\<psi> (''x'', Tv) = true \<or> \<psi> (''x'', Tv) = false"
+      using asg_into_interp_is_true_or_false assms
+      by auto
+    then show " satisfies D I \<psi> (g\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o)"
+      using True \<psi> unfolding agree_off_asg_def by auto
+  qed
+  then have  "val D I \<phi> (\<^bold>[\<^bold>\<forall>''x'':Tv. (g\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o)\<^bold>]) = true"
+    using lemma_5401_g using assms by auto
+  then show ?thesis
+    unfolding axiom_1_def
+    using lemma_5401_b[OF assms(1,2)] val by auto
+next
+  case False
+  have "\<phi> (''g'', oo) \<in>: D oo"
+    using assms
+    by (simp add: asg_into_frame_def) 
+  then have 0: "\<phi> (''g'', oo) \<in>: funspace (D Tv) (D Tv)"
+    using assms(1) assms(2) fun_sym_asg_to_funspace by blast
+
+  from False have "(\<phi> (''g'', oo) \<cdot> true \<noteq> true \<or> \<phi> (''g'', oo) \<cdot> false \<noteq> true)"
+    by auto
+  then have "\<exists>z. \<phi> (''g'', oo) \<cdot> z = false \<and> z \<in>: D Tv"
+  proof
+    assume a: "\<phi> (''g'', oo) \<cdot> true \<noteq> true"
+    have "\<phi> (''g'', oo) \<cdot> true \<in>: boolset"
+      by (metis "0" apply_abstract assms(1) boolset_def general_model.elims(2) in_funspace_abstract 
+          mem_two true_def wf_frame_def wf_interp.simps)
+    from this a have "\<phi> (''g'', oo) \<cdot> true = false \<and> true \<in>: D Tv"
+      using assms(1) wf_frame_def wf_interp.simps by auto  
+    then show "\<exists>z. \<phi> (''g'', oo) \<cdot> z = false \<and> z \<in>: D Tv"
+      by auto
+  next
+    assume a: "\<phi> (''g'', oo) \<cdot> false \<noteq> true"
+    have "\<phi> (''g'', oo) \<cdot> false \<in>: boolset"
+      by (metis "0" apply_abstract assms(1) boolset_def general_model.elims(2) in_funspace_abstract 
+          mem_two false_def wf_frame_def wf_interp.simps)
+    from this a have "\<phi> (''g'', oo) \<cdot> false = false \<and> false \<in>: D Tv" 
+      using assms(1) wf_frame_def wf_interp.simps by auto
+    then show "\<exists>z. \<phi> (''g'', oo) \<cdot> z = false \<and> z \<in>: D Tv"
+      by auto
+  qed
+  then obtain z where z_p: "\<phi> (''g'', oo) \<cdot> z = false \<and> z \<in>: D Tv"
+    by auto
+  have "boolean (satisfies D I \<phi> (g\<^sub>o\<^sub>o \<^bold>\<cdot> T)
+          \<and> satisfies D I \<phi> (g\<^sub>o\<^sub>o \<^bold>\<cdot> F)) = false"
+    using False
+    by (smt boolean_def val.simps(1) val.simps(3) lemma_5401_c[OF assms(1,2)] 
+        lemma_5401_d[OF assms(1,2)])
+  then have 1: "val D I \<phi> ( 
+         (g\<^sub>o\<^sub>o \<^bold>\<cdot> T) \<^bold>\<and>
+         (g\<^sub>o\<^sub>o \<^bold>\<cdot> F)) = false"
+    using lemma_5401_e_variant_2 assms by auto
+  have 3: "asg_into_frame (\<phi>((''x'', Tv) := z)) D \<and>
+    agree_off_asg (\<phi>((''x'', Tv) := z)) \<phi> ''x'' Tv \<and>
+    \<phi> (''g'', oo) \<cdot> (\<phi>((''x'', Tv) := z)) (''x'', Tv) \<noteq> true"
+    using z_p Pair_inject agree_off_asg_def2 asg_into_frame_fun_upd assms(2) true_neq_false by fastforce
+  then have 2: "val D I \<phi> (\<^bold>[\<^bold>\<forall>''x'':Tv. (g\<^sub>o\<^sub>o \<^bold>\<cdot> x\<^sub>o)\<^bold>]) = false"
+    using  lemma_5401_g_variant_1 assms boolean_def by auto
+  then show ?thesis
+    unfolding axiom_1_def using 1 2 lemma_5401_b_variant_2[OF assms(1,2)] by auto 
+qed
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 1 *)
+theorem theorem_5402_a_axiom_1: "valid_general axiom_1"
+  using theorem_5402_a_axiom_1_variant unfolding valid_general_def valid_in_model_def by auto
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 2 *)
+theorem theorem_5402_a_axiom_2_variant:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  shows "satisfies D I \<phi> (axiom_2 \<alpha>)"
+proof (cases "\<phi>(''x'',\<alpha>) = \<phi>(''y'',\<alpha>)")
+  case True
+  have "val D I \<phi> ((Var ''h'' (Tv \<^bold>\<Leftarrow> \<alpha>)) \<^bold>\<cdot> (Var ''x'' \<alpha>)) = 
+           (\<phi> (''h'', (Tv \<^bold>\<Leftarrow> \<alpha>))) \<cdot> \<phi> (''x'', \<alpha>)"
+    using assms by auto
+  also
+  have "... = \<phi> (''h'', (Tv \<^bold>\<Leftarrow> \<alpha>)) \<cdot> \<phi> (''y'', \<alpha>)"
+    using True by auto
+  also
+  have "... = val D I \<phi> ((Var ''h'' (Tv \<^bold>\<Leftarrow> \<alpha>)) \<^bold>\<cdot> (Var ''y'' \<alpha>))"
+    using assms by auto
+  finally
+  show ?thesis
+    unfolding axiom_2_def 
+    using lemma_5401_f_variant_2 assms lemma_5401_b_variant_1[OF assms(1,2)] boolean_def by auto
+next
+  case False
+  have "asg_into_frame \<phi> D"
+    using assms(2) by blast
+  moreover
+  have "general_model D I"
+    using assms(1) by blast
+  ultimately
+  have 
+    "boolean (satisfies D I \<phi> \<^bold>[Var ''x'' \<alpha> \<^bold>=\<alpha>\<^bold>= Var ''y'' \<alpha>\<^bold>] \<longrightarrow>
+       satisfies D I \<phi>
+         \<^bold>[(Var ''h'' (Tv \<^bold>\<Leftarrow> \<alpha>) \<^bold>\<cdot> Var ''x'' \<alpha>) \<^bold>=Tv\<^bold>= Var ''h'' (Tv \<^bold>\<Leftarrow> \<alpha>) \<^bold>\<cdot> Var ''y'' \<alpha>\<^bold>]) =
+       true"
+    using boolean_eq_true lemma_5401_b by auto
+  then
+  show ?thesis
+    using assms lemma_5401_f_variant_2 unfolding axiom_2_def by auto
+qed                                   
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 2 *)
+theorem theorem_5402_a_axiom_2: "valid_general (axiom_2 \<alpha>)"
+  using theorem_5402_a_axiom_2_variant unfolding valid_general_def valid_in_model_def by auto
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 3 *)
+theorem theorem_5402_a_axiom_3_variant:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  shows "satisfies D I \<phi> (axiom_3 \<alpha> \<beta>)"
+proof (cases "\<phi> (''f'',\<alpha> \<^bold>\<Leftarrow> \<beta>) = \<phi> (''g'',\<alpha> \<^bold>\<Leftarrow> \<beta>)")
+  case True
+  {
+    fix \<psi>
+    assume agree: "agree_off_asg \<psi> \<phi> ''x'' \<beta>"
+    assume asg: "asg_into_interp \<psi> D I"
+    have "val D I \<psi> ((Var ''f'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<^bold>\<cdot> (Var ''x'' \<beta>)) = \<psi> (''f'',\<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> \<psi> (''x'', \<beta>)"
+      by auto
+    also
+    have "... = \<phi> (''f'',\<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> \<psi> (''x'', \<beta>)"
+      using agree by auto
+    also
+    have "... = \<phi> (''g'',\<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> \<psi> (''x'', \<beta>)"
+      using True by auto
+    also
+    have "... = \<psi> (''g'',\<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> \<psi> (''x'', \<beta>)"
+      using agree by auto
+    also
+    have "... = val D I \<psi> ((Var ''g'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<^bold>\<cdot> (Var ''x'' \<beta>))"
+      by auto
+    finally
+    have 
+      "val D I \<psi>
+            (\<^bold>[((Var ''f'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<^bold>\<cdot> (Var ''x'' \<beta>)) \<^bold>=\<alpha>\<^bold>= ((Var ''g'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<^bold>\<cdot> (Var ''x'' \<beta>))\<^bold>]) 
+       = true"
+      using lemma_5401_b_variant_1[OF assms(1)] assms agree asg boolean_eq_true by auto
+  }
+  then have "satisfies D I \<phi>
+        (\<^bold>[\<^bold>\<forall>''x'':\<beta>. \<^bold>[(Var ''f'' (\<alpha> \<^bold>\<Leftarrow> \<beta>) \<^bold>\<cdot> Var ''x'' \<beta>) \<^bold>=\<alpha>\<^bold>= Var ''g'' (\<alpha> \<^bold>\<Leftarrow> \<beta>) \<^bold>\<cdot> Var ''x'' \<beta>\<^bold>]\<^bold>])"
+    using assms lemma_5401_g by force
+  moreover
+  have "satisfies D I \<phi> \<^bold>[Var ''f'' (\<alpha> \<^bold>\<Leftarrow> \<beta>) \<^bold>=\<alpha> \<^bold>\<Leftarrow> \<beta>\<^bold>= Var ''g'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)\<^bold>]"
+    using True assms using lemma_5401_b_variant_2 wff_Var by auto
+  ultimately
+  show ?thesis
+    using axiom_3_def lemma_5401_b_variant_2 assms by auto
+next
+  case False
+  then have "\<exists>z. z \<in>: D \<beta> \<and> \<phi> (''f'', \<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> z \<noteq> \<phi> (''g'', \<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> z"
+    using funspace_difference_witness[of "\<phi> (''f'', \<alpha> \<^bold>\<Leftarrow> \<beta>)" "D \<beta>" "D \<alpha>" "\<phi> (''g'', \<alpha> \<^bold>\<Leftarrow> \<beta>)"]
+      assms(1,2) fun_sym_asg_to_funspace by blast
+  then obtain z where
+    z\<beta>: "z \<in>: D \<beta>" and
+    z_neq: "\<phi> (''f'', \<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> z \<noteq> \<phi> (''g'', \<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> z"
+    by auto
+  define \<psi> where "\<psi> = (\<phi>((''x'',\<beta>):= z))"
+  have agree: "agree_off_asg \<psi> \<phi> ''x'' \<beta>"
+    using \<psi>_def agree_off_asg_def2 by blast
+  have asg: "asg_into_interp \<psi> D I"
+    using z\<beta> \<psi>_def asg_into_frame_fun_upd assms(2) by blast
+  have "val D I \<psi> ((Var ''f'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<^bold>\<cdot> (Var ''x'' \<beta>)) = \<psi> (''f'',\<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> \<psi> (''x'', \<beta>)"
+    by auto
+  moreover
+  have "... = \<phi> (''f'',\<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> z"
+    by (simp add: \<psi>_def)
+  moreover
+  have "... \<noteq> \<phi> (''g'',\<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> z"
+    using False z_neq by blast
+  moreover
+  have "\<phi> (''g'',\<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> z = \<psi> (''g'',\<alpha> \<^bold>\<Leftarrow> \<beta>) \<cdot> \<psi> (''x'', \<beta>)"
+    by (simp add: \<psi>_def)
+  moreover
+  have "... = val D I \<psi> ((Var ''g'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<^bold>\<cdot> (Var ''x'' \<beta>))"
+    by auto
+  ultimately
+  have 
+    "val D I \<psi>
+            (\<^bold>[((Var ''f'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<^bold>\<cdot> (Var ''x'' \<beta>)) \<^bold>=\<alpha>\<^bold>= ((Var ''g'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)) \<^bold>\<cdot> (Var ''x'' \<beta>))\<^bold>]) 
+       = false"
+    by (metis asg assms(1) lemma_5401_b_variant_3 wff_App wff_Var)
+  have "val D I \<phi>
+        (\<^bold>[\<^bold>\<forall>''x'':\<beta>. \<^bold>[(Var ''f'' (\<alpha> \<^bold>\<Leftarrow> \<beta>) \<^bold>\<cdot> Var ''x'' \<beta>) \<^bold>=\<alpha>\<^bold>= Var ''g'' (\<alpha> \<^bold>\<Leftarrow> \<beta>) \<^bold>\<cdot> Var ''x'' \<beta>\<^bold>]\<^bold>]) = false"
+    by (smt (verit) \<open>val D I \<psi> \<^bold>[(Var ''f'' (\<alpha> \<^bold>\<Leftarrow> \<beta>) \<^bold>\<cdot> Var ''x'' \<beta>) \<^bold>=\<alpha>\<^bold>= Var ''g'' (\<alpha> \<^bold>\<Leftarrow> \<beta>) \<^bold>\<cdot> Var ''x'' \<beta>\<^bold>] = false\<close> 
+        agree asg assms(1,2) lemma_5401_g wff_App wff_Eql wff_Forall wff_Tv_is_true_or_false wff_Var)
+  moreover
+  have "val D I \<phi> \<^bold>[Var ''f'' (\<alpha> \<^bold>\<Leftarrow> \<beta>) \<^bold>=\<alpha> \<^bold>\<Leftarrow> \<beta>\<^bold>= Var ''g'' (\<alpha> \<^bold>\<Leftarrow> \<beta>)\<^bold>] = false"
+    using False assms(1,2) lemma_5401_b_variant_3 wff_Var by auto
+  ultimately show ?thesis
+    using assms(1,2) axiom_3_def lemma_5401_b by auto
+qed
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 3 *)
+theorem theorem_5402_a_axiom_3: "valid_general (axiom_3 \<alpha> \<beta>)"
+  using theorem_5402_a_axiom_3_variant unfolding valid_general_def valid_in_model_def by auto
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 4_1 with a constant *)
+theorem theorem_5402_a_axiom_4_1_variant_cst:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "wff \<alpha> A"
+  shows "satisfies D I \<phi> (axiom_4_1_variant_cst x \<alpha> c \<beta> A)"
+proof -
+  let ?\<psi> = "\<phi>((x,\<alpha>):=val D I \<phi> A)"
+  have "val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. (Cst c \<beta>)\<^bold>] \<^bold>\<cdot> A) = val D I ?\<psi> (Cst c \<beta>)"
+    by (rule lemma_5401_a[of _ _ _ _ _ \<beta>]; use assms in auto)
+  then have "val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. Cst c \<beta>\<^bold>] \<^bold>\<cdot> A) = val D I \<phi> (Cst c \<beta>)"
+    by auto
+  moreover
+  have "wff \<beta> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. Cst c \<beta>\<^bold>] \<^bold>\<cdot> A)"
+    using assms by auto
+  ultimately
+  show ?thesis
+    unfolding axiom_4_1_variant_cst_def
+    using lemma_5401_b_variant_2[OF assms(1,2)] by auto
+qed
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 4_1 *)
+theorem theorem_5402_a_axiom_4_1_variant_var:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "wff \<alpha> A"
+  assumes "axiom_4_1_variant_var_side_condition x \<alpha> y \<beta> A"
+  shows "satisfies D I \<phi> (axiom_4_1_variant_var x \<alpha> y \<beta> A)"
+proof -
+  let ?\<psi> = "\<phi>((x,\<alpha>):=val D I \<phi> A)"
+  have  "val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. (Var y \<beta>)\<^bold>] \<^bold>\<cdot> A) = val D I ?\<psi> (Var y \<beta>)"
+    by (rule lemma_5401_a[of _ _ _ _ _  \<beta>], use assms in auto)
+  then have "val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. Var y \<beta>\<^bold>] \<^bold>\<cdot> A) = val D I \<phi> (Var y \<beta>)"   
+    using assms unfolding axiom_4_1_variant_var_side_condition_def by auto
+  moreover
+  have "wff \<beta> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. Var y \<beta>\<^bold>] \<^bold>\<cdot> A)"
+    using assms by auto
+  moreover
+  have "wff \<beta> (Var y \<beta>)"
+    using assms by auto
+  ultimately
+  show ?thesis
+    unfolding axiom_4_1_variant_var_def
+    using lemma_5401_b_variant_2[OF assms(1,2)] by auto
+qed
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 4_1 *)
+theorem theorem_5402_a_axiom_4_1:
+  assumes "asg_into_interp \<phi> D I"
+  assumes "general_model D I"
+  assumes "axiom_4_1_side_condition x \<alpha> y \<beta> A"
+  assumes "wff \<alpha> A"
+  shows "satisfies D I \<phi> (axiom_4_1 x \<alpha> y \<beta> A)"
+  using assms theorem_5402_a_axiom_4_1_variant_cst theorem_5402_a_axiom_4_1_variant_var
+  unfolding axiom_4_1_variant_cst_def axiom_4_1_variant_var_side_condition_def
+    axiom_4_1_side_condition_def axiom_4_1_variant_var_def
+    axiom_4_1_def by auto
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 4_2 *)
+theorem theorem_5402_a_axiom_4_2: 
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "wff \<alpha> A"
+  shows "satisfies D I \<phi> (axiom_4_2 x \<alpha> A)"
+proof -
+  let ?\<psi> = "\<phi>((x,\<alpha>):=val D I \<phi> A)"
+  have "wff \<alpha> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. Var x \<alpha>\<^bold>] \<^bold>\<cdot> A)"
+    using assms by auto
+  moreover
+  have "wff \<alpha> A"
+    using assms by auto
+  moreover
+  have "val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. Var x \<alpha>\<^bold>] \<^bold>\<cdot> A) = val D I \<phi> A"
+    using lemma_5401_a[of _ _ _ _ _ \<alpha> _ _] assms by auto
+  ultimately
+  show ?thesis
+    unfolding axiom_4_2_def by (rule lemma_5401_b_variant_2[OF assms(1,2)])
+qed
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 4_3 *)
+theorem theorem_5402_a_axiom_4_3: 
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "wff \<alpha> A"
+  assumes "wff (\<beta> \<^bold>\<Leftarrow> \<gamma>) B"
+  assumes "wff \<gamma> C"
+  shows "satisfies D I \<phi> (axiom_4_3 x \<alpha> B \<beta> \<gamma> C A)"
+proof -
+  let ?\<psi> = "\<phi>((x,\<alpha>):=val D I \<phi> A)"
+  let ?E = "B \<^bold>\<cdot> C"
+
+  have "val D I \<phi> (LHS (axiom_4_3 x \<alpha> B \<beta> \<gamma> C A)) = val D I ?\<psi> ?E"
+    by (metis LHS_def2 assms(3) assms(4) assms(5) axiom_4_3_def lemma_5401_a[OF assms(1,2)] wff_App)
+  moreover
+  have "... = val D I ?\<psi> (B \<^bold>\<cdot> C)"
+    by simp
+  moreover
+  have "... = (val D I ?\<psi> B) \<cdot> val D I ?\<psi> C"
+    by simp
+  moreover
+  have "... = (val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A)) \<cdot> val D I \<phi> (App \<^bold>[\<^bold>\<lambda>x :\<alpha>. C\<^bold>] A)"
+    by (metis assms(3) assms(4) assms(5) lemma_5401_a[OF assms(1,2)])
+  moreover
+  have "... = val D I \<phi> (RHS (axiom_4_3 x \<alpha> B \<beta> \<gamma> C A))"
+    unfolding axiom_4_3_def by auto
+  ultimately
+  have "val D I \<phi> (LHS (axiom_4_3 x \<alpha> B \<beta> \<gamma> C A)) = val D I \<phi> (RHS (axiom_4_3 x \<alpha> B \<beta> \<gamma> C A))"
+    by auto
+  then have "val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. B \<^bold>\<cdot> C\<^bold>] \<^bold>\<cdot> A) = val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A \<^bold>\<cdot> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. C\<^bold>] \<^bold>\<cdot> A))"
+    unfolding axiom_4_3_def by auto
+  moreover
+  have "wff \<beta> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. B \<^bold>\<cdot> C\<^bold>] \<^bold>\<cdot> A)"
+    using assms by auto
+  moreover
+  have "wff \<beta> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A \<^bold>\<cdot> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. C\<^bold>] \<^bold>\<cdot> A))"
+    using assms by auto
+  ultimately
+  show ?thesis
+    unfolding axiom_4_3_def using lemma_5401_b_variant_2[OF assms(1,2)] by auto
+qed
+
+lemma lemma_to_help_with_theorem_5402_a_axiom_4_4:
+  assumes lambda_eql_lambda_lambda: 
+    "\<And>z. z \<in>: D \<gamma> \<Longrightarrow> val D I \<psi> \<^bold>[\<^bold>\<lambda>y:\<gamma>. B\<^bold>] \<cdot> z = val D I \<phi> \<^bold>[\<^bold>\<lambda>y:\<gamma>. \<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A\<^bold>] \<cdot> z" 
+  assumes \<psi>_eql: "\<psi> = \<phi>((x, \<alpha>) := val D I \<phi> A)" 
+  assumes "asg_into_frame \<phi> D" 
+  assumes "general_model D I" 
+  assumes "axiom_4_4_side_condition x \<alpha> y \<gamma> B \<delta> A" 
+  assumes "wff \<alpha> A" 
+  assumes "wff \<delta> B"
+  shows "val D I \<psi> \<^bold>[\<^bold>\<lambda>y:\<gamma>. B\<^bold>] = val D I \<phi> \<^bold>[\<^bold>\<lambda>y:\<gamma>. \<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A\<^bold>]"
+proof -
+  {
+    fix e
+    assume e_in_D: "e \<in>: D \<gamma>"
+    then have "val D I (\<psi>((y, \<gamma>) := e)) B \<in>: D (type_of B)"
+      using asg_into_frame_fun_upd assms(3,4,6,7) \<psi>_eql by auto
+    then have val_lambda_B: "val D I \<psi> \<^bold>[\<^bold>\<lambda>y:\<gamma>. B\<^bold>] \<cdot> e = val D I (\<psi>((y, \<gamma>) := e)) B"
+      using e_in_D by auto
+    have
+      "val D I \<phi> \<^bold>[\<^bold>\<lambda>y:\<gamma>. \<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A\<^bold>] \<cdot> e = 
+       abstract (D \<alpha>) (D (type_of B))
+         (\<lambda>z. val D I (\<phi>((y, \<gamma>) := e, (x, \<alpha>) := z)) B) \<cdot> val D I (\<phi>((y, \<gamma>) := e)) A"
+      using apply_abstract e_in_D asg_into_frame_fun_upd assms(3,4,6,7) by auto
+    then have "val D I (\<psi>((y, \<gamma>) := e)) B =
+        abstract (D \<alpha>) (D (type_of B))
+         (\<lambda>z. val D I (\<phi>((y, \<gamma>) := e, (x, \<alpha>) := z)) B) \<cdot> val D I (\<phi>((y, \<gamma>) := e)) A" 
+      using val_lambda_B lambda_eql_lambda_lambda e_in_D by metis
+  }
+  note val_eql_abstract = this
+
+  have 
+    "\<forall>e. e \<in>: D \<gamma> \<longrightarrow>
+            val D I (\<psi>((y, \<gamma>) := e)) B \<in>: D (type_of B) \<and>
+            val D I (\<psi>((y, \<gamma>) := e)) B =
+            abstract (D \<alpha>) (D (type_of B))
+              (\<lambda>za. val D I (\<phi>((y, \<gamma>) := e, (x, \<alpha>) := za)) B) \<cdot> val D I (\<phi>((y, \<gamma>) := e)) A"
+    using asg_into_frame_fun_upd assms(3,4,6,7) \<psi>_eql val_eql_abstract by auto
+  then have 
+    "abstract (D \<gamma>) (D (type_of B)) (\<lambda>z. val D I (\<psi>((y, \<gamma>) := z)) B) =
+     abstract (D \<gamma>) (D (type_of B))
+       (\<lambda>z. abstract (D \<alpha>) (D (type_of B))
+         (\<lambda>za. val D I (\<phi>((y, \<gamma>) := z, (x, \<alpha>) := za)) B) \<cdot> val D I (\<phi>((y, \<gamma>) := z)) A)"
+    by (rule abstract_extensional)
+  then show ?thesis 
+    by auto
+qed
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 4_4 *)
+theorem theorem_5402_a_axiom_4_4:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "axiom_4_4_side_condition x \<alpha> y \<gamma> B \<delta> A"
+  assumes "wff \<alpha> A"
+  assumes "wff \<delta> B"
+  shows "satisfies D I \<phi> (axiom_4_4 x \<alpha> y \<gamma> B \<delta> A)"
+proof -
+  define \<psi> where "\<psi> = \<phi>((x,\<alpha>):=val D I \<phi> A)"
+  let ?E = "\<^bold>[\<^bold>\<lambda>y:\<gamma>. B\<^bold>]"
+  have fr: "(y, \<gamma>) \<notin> vars A"
+    using assms(3) axiom_4_4_side_condition_def by blast
+  {
+    fix z
+    assume z_in_D: "z \<in>: D \<gamma>"
+    define \<phi>' where "\<phi>' = \<phi>((y,\<gamma>) := z)"
+    have "asg_into_frame \<phi>' D"
+      using assms z_in_D unfolding asg_into_frame_def \<phi>'_def by auto
+    moreover
+    have "\<forall>(x, \<alpha>)\<in>vars A. agree_on_asg \<phi> \<phi>' x \<alpha>"
+      using fr unfolding \<phi>'_def by auto
+    ultimately
+    have "val D I \<phi> A = val D I \<phi>' A"
+      using prop_5400[OF assms(1), of _ _ \<alpha>] assms(2) assms(4) frees_subset_vars by blast
+    then have Az: "\<phi>'((x,\<alpha>):=(val D I \<phi>' A)) = \<psi>((y,\<gamma>):=z)"
+      using assms(3) unfolding axiom_4_4_side_condition_def
+      by (simp add: fun_upd_twist \<phi>'_def \<psi>_def) 
+    then have "abstract (D \<gamma>) (D (type_of B)) (\<lambda>z. val D I (\<psi>((y, \<gamma>) := z)) B) \<cdot> z = 
+               val D I (\<psi>((y, \<gamma>) := z)) B"
+      using apply_abstract_matchable assms(1,2,4,5) type_of asg_into_frame_fun_upd 
+        general_model.elims(2) z_in_D by (metis \<phi>'_def)
+    then have "(val D I \<psi> ?E) \<cdot> z = (val D I (\<psi>((y,\<gamma>):=z)) B)"
+      by auto
+    moreover
+    have "... = val D I \<phi>' (\<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A)"
+      using assms(1,2,4,5) asg_into_frame_fun_upd lemma_5401_a z_in_D
+      by (metis Az \<phi>'_def) 
+    moreover
+    have "... = val D I \<phi> \<^bold>[\<^bold>\<lambda>y:\<gamma>. \<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A\<^bold>] \<cdot> z"
+    proof -
+      have valA: "val D I \<phi>' A \<in>: D \<alpha>"
+        using \<phi>'_def asg_into_frame_fun_upd z_in_D assms by simp
+      have valB: "val D I (\<phi>'((x, \<alpha>) := val D I \<phi>' A)) B \<in>: D (type_of B)" 
+        using asg_into_frame_fun_upd z_in_D assms by (simp add: Az \<psi>_def) 
+      have valA': "val D I (\<phi>((y, \<gamma>) := z)) A \<in>: D \<alpha>"
+        using z_in_D assms asg_into_frame_fun_upd valA unfolding \<psi>_def \<phi>'_def 
+        by blast
+      have valB':
+        "val D I (\<phi>((y, \<gamma>) := z, (x, \<alpha>) := val D I (\<phi>((y, \<gamma>) := z)) A)) B 
+         \<in>: D (type_of B)"
+        using asg_into_frame_fun_upd z_in_D assms valB \<phi>'_def by blast 
+      have
+        "val D I (\<phi>'((x, \<alpha>) := val D I \<phi>' A)) B =
+         val D I (\<phi>((y, \<gamma>) := z, (x, \<alpha>) := val D I (\<phi>((y, \<gamma>) := z)) A)) B"
+        unfolding \<psi>_def \<phi>'_def by (metis apply_abstract asg_into_frame_fun_upd)
+      then have valB_eql_abs: 
+        "val D I (\<phi>'((x, \<alpha>) := val D I \<phi>' A)) B =
+         abstract (D \<alpha>) (D (type_of B))
+           (\<lambda>za. val D I (\<phi>((y, \<gamma>) := z, (x, \<alpha>) := za)) B) \<cdot> val D I (\<phi>((y, \<gamma>) := z)) A"
+        using valA' valB' by auto
+      then have "abstract (D \<alpha>) (D (type_of B))
+              (\<lambda>za. val D I (\<phi>((y, \<gamma>) := z, (x, \<alpha>) := za)) B) \<cdot> val D I (\<phi>((y, \<gamma>) := z)) A 
+            \<in>: D (type_of B)"
+        using valB assms z_in_D by auto
+      then have 
+        "val D I (\<phi>'((x, \<alpha>) := val D I \<phi>' A)) B =
+         abstract (D \<gamma>) (D (type_of B))
+           (\<lambda>z. abstract (D \<alpha>) (D (type_of B))
+             (\<lambda>za. val D I (\<phi>((y, \<gamma>) := z, (x, \<alpha>) := za)) B) \<cdot> val D I (\<phi>((y, \<gamma>) := z)) A) \<cdot> z"
+        using z_in_D valB_eql_abs by auto
+      then show "val D I \<phi>' (\<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A) = val D I \<phi> \<^bold>[\<^bold>\<lambda>y:\<gamma>. \<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A\<^bold>] \<cdot> z"
+        using valA valB by auto
+    qed
+    ultimately
+    have "val D I \<psi> \<^bold>[\<^bold>\<lambda>y:\<gamma>. B\<^bold>] \<cdot> z = val D I \<phi> \<^bold>[\<^bold>\<lambda>y:\<gamma>. \<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A\<^bold>] \<cdot> z"
+      by simp
+  }
+  note lambda_eql_lambda_lambda = this
+  have equal_funs: "val D I \<psi> ?E = val D I \<phi> (\<^bold>[\<^bold>\<lambda>y:\<gamma>. (\<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>]) \<^bold>\<cdot> A\<^bold>])"
+    using lambda_eql_lambda_lambda \<psi>_def assms lemma_to_help_with_theorem_5402_a_axiom_4_4 by metis
+  have "val D I \<phi> (\<^bold>[\<^bold>\<lambda>x:\<alpha>. \<^bold>[\<^bold>\<lambda>y:\<gamma>. B\<^bold>]\<^bold>] \<^bold>\<cdot> A) = val D I \<phi> \<^bold>[\<^bold>\<lambda>y:\<gamma>. \<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A\<^bold>]"
+    using equal_funs by (metis \<psi>_def assms(1,2,4,5) lemma_5401_a wff_Abs) 
+  then have "satisfies D I \<phi> \<^bold>[(\<^bold>[\<^bold>\<lambda>x:\<alpha>. \<^bold>[\<^bold>\<lambda>y:\<gamma>. B\<^bold>]\<^bold>] \<^bold>\<cdot> A) \<^bold>=\<delta> \<^bold>\<Leftarrow> \<gamma>\<^bold>= \<^bold>[\<^bold>\<lambda>y:\<gamma>. \<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>] \<^bold>\<cdot> A\<^bold>]\<^bold>]"
+    using lemma_5401_b[OF assms(1,2)] assms by auto
+  then show ?thesis
+    unfolding axiom_4_4_def .
+qed
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 4_5 *)
+theorem theorem_5402_a_axiom_4_5:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  assumes "wff \<alpha> A"
+  assumes "wff \<delta> B"
+  shows "satisfies D I \<phi> (axiom_4_5 x \<alpha> B \<delta> A)"
+proof -
+  define \<psi> where "\<psi> = \<phi>((x,\<alpha>):=val D I \<phi> A)"
+  let ?E = "\<^bold>[\<^bold>\<lambda>x:\<alpha>. B\<^bold>]"
+
+  {
+    assume val: "\<forall>\<phi>. asg_into_frame \<phi> D \<longrightarrow> (\<forall>A \<alpha>. wff \<alpha> A \<longrightarrow> val D I \<phi> A \<in>: D \<alpha>)"
+    assume asg: "asg_into_frame \<phi> D"
+    assume wffA: "wff \<alpha> A"
+    assume wffB: "wff \<delta> B"
+    have valA: "val D I \<phi> A \<in>: D \<alpha>"
+      using val asg wffA by blast
+    have "\<forall>t cs. val D I \<phi> \<^bold>[\<^bold>\<lambda>cs:t. B\<^bold>] \<in>: D (\<delta> \<^bold>\<Leftarrow> t)"
+      using val asg wffB wff_Abs by blast
+    then have "abstract (D \<alpha>) (D (\<delta> \<^bold>\<Leftarrow> \<alpha>)) 
+                 (\<lambda>u. abstract (D \<alpha>) (D \<delta>) (\<lambda>u. val D I (\<phi>((x, \<alpha>) := u)) B)) \<cdot> val D I \<phi> A =
+               abstract (D \<alpha>) (D \<delta>) (\<lambda>u. val D I (\<phi>((x, \<alpha>) := u)) B)"
+      using valA wffB by simp
+  }
+  note abstract_eql = this
+
+  have "val D I \<psi> ?E = val D I \<phi> ?E"
+    using prop_5400[OF assms(1), of _ _ "\<delta> \<^bold>\<Leftarrow> \<alpha>"] \<psi>_def assms(2) by auto
+  then show ?thesis
+    unfolding axiom_4_5_def using lemma_5401_b[OF assms(1,2)] assms abstract_eql by auto
+qed
+
+(* Corresponds to Andrews' theorem 5402 a for axiom 5 *)
+theorem theorem_5402_a_axiom_5:
+  assumes "general_model D I"
+  assumes "asg_into_interp \<phi> D I"
+  shows "satisfies D I \<phi> (axiom_5)"
+proof -
+  have iden_eql: "iden (D Ind) \<cdot> I ''y'' Ind = one_elem_fun (I ''y'' Ind) (D Ind)"
+  proof -
+    have "I ''y'' Ind \<in>: D Ind"
+      using assms unfolding  general_model.simps wf_interp.simps[simplified] iden_def one_elem_fun_def
+      by auto
+    moreover
+    have "abstract (D Ind) boolset (\<lambda>y. boolean (I ''y'' Ind = y)) \<in>: funspace (D Ind) boolset"
+      using boolean_in_boolset by auto
+    ultimately
+    show ?thesis
+      unfolding iden_def one_elem_fun_def by auto
+  qed
+
+  have "val D I \<phi> (\<^bold>\<iota> \<^bold>\<cdot> ((\<^bold>Q (Tv \<^bold>\<Leftarrow> Ind \<^bold>\<Leftarrow> Ind)) \<^bold>\<cdot> y\<^sub>i)) = 
+          val D I \<phi> \<^bold>\<iota> \<cdot> val D I \<phi> ((\<^bold>Q (Tv \<^bold>\<Leftarrow> Ind \<^bold>\<Leftarrow> Ind)) \<^bold>\<cdot> y\<^sub>i)"
+    by auto
+  moreover
+  have "... = val D I \<phi> y\<^sub>i"
+    using assms iden_eql unfolding general_model.simps wf_interp.simps[simplified] by auto
+  ultimately
+  show ?thesis
+    unfolding axiom_5_def using lemma_5401_b[OF assms(1,2)] by auto
+qed
+
+lemma theorem_isa_Tv:
+  assumes "theorem A"
+  shows "wff Tv A"
+  using assms proof (induction)
+  case (by_axiom A)
+  then show ?case 
+  proof (induction)
+    case by_axiom_1
+    then show ?case 
+      unfolding axiom_1_def by auto
+  next
+    case (by_axiom_2 \<alpha>)
+    then show ?case 
+      unfolding axiom_2_def by auto
+  next
+    case (by_axiom_3 \<alpha> \<beta>)
+    then show ?case 
+      unfolding axiom_3_def by auto
+  next
+    case (by_axiom_4_1 \<alpha> A \<beta> B x)
+    then show ?case 
+      unfolding axiom_4_1_def by auto
+  next
+    case (by_axiom_4_2 \<alpha> A x)
+    then show ?case 
+      unfolding axiom_4_2_def by auto
+  next
+    case (by_axiom_4_3 \<alpha> A \<beta> \<gamma> B C x)
+    then show ?case 
+      unfolding axiom_4_3_def by auto
+  next
+    case (by_axiom_4_4 \<alpha> A \<delta> B x y \<gamma>)
+    then show ?case 
+      unfolding axiom_4_4_def by auto
+  next
+    case (by_axiom_4_5 \<alpha> A \<delta> B x)
+    then show ?case 
+      unfolding axiom_4_5_def by auto
+  next
+    case by_axiom_5
+    then show ?case 
+      unfolding axiom_5_def by auto
+  qed
+next
+  case (by_rule_R A B C)
+  then show ?case
+    by (smt replacement_preserves_type rule_R.cases wff_Eql_iff)
+qed
+
+(* Corresponds to Andrews' theorem 5402 a *)
+theorem theorem_5402_a_general:
+  assumes "theorem A"
+  shows "valid_general A"
+  using assms 
+proof (induction)
+  case (by_axiom A)
+  then show ?case
+  proof (induction)
+    case by_axiom_1
+    then show ?case 
+      using theorem_5402_a_axiom_1 by auto
+  next
+    case (by_axiom_2 \<alpha>)
+    then show ?case 
+      using theorem_5402_a_axiom_2 by auto
+  next
+    case (by_axiom_3 \<alpha> \<beta>)
+    then show ?case 
+      using theorem_5402_a_axiom_3 by auto
+  next
+    case (by_axiom_4_1 \<alpha> A \<beta> B x)
+    then show ?case 
+      using theorem_5402_a_axiom_4_1
+      unfolding valid_general_def valid_in_model_def by auto
+  next
+    case (by_axiom_4_2 \<alpha> A x)
+    then show ?case 
+      using theorem_5402_a_axiom_4_2 
+      unfolding valid_general_def valid_in_model_def by auto
+  next
+    case (by_axiom_4_3 \<alpha> A \<beta> \<gamma> B C x)
+    then show ?case 
+      using theorem_5402_a_axiom_4_3 
+      unfolding valid_general_def valid_in_model_def by auto
+  next
+    case (by_axiom_4_4 \<alpha> A \<delta> B x y \<gamma>)
+    then show ?case 
+      using theorem_5402_a_axiom_4_4 
+      unfolding valid_general_def valid_in_model_def by auto
+  next
+    case (by_axiom_4_5 \<alpha> A \<delta> B x)
+    then show ?case 
+      using theorem_5402_a_axiom_4_5 
+      unfolding valid_general_def valid_in_model_def by auto
+  next
+    case by_axiom_5
+    then show ?case
+      using theorem_5402_a_axiom_5 
+      unfolding valid_general_def valid_in_model_def by auto
+  qed
+next
+  case (by_rule_R C AB C')
+  then have C_isa_Tv: "wff Tv C"
+    using theorem_isa_Tv by blast
+  have "\<exists>A B \<beta>. AB = \<^bold>[A \<^bold>=\<beta>\<^bold>= B\<^bold>] \<and> wff \<beta> A \<and> wff \<beta> B"
+    using by_rule_R rule_R.simps theorem_isa_Tv by fastforce
+  then obtain A B \<beta> where A_B_\<beta>_p: "AB = \<^bold>[A \<^bold>=\<beta>\<^bold>= B\<^bold>] \<and> wff \<beta> A \<and> wff \<beta> B"
+    by blast
+  then have R: "rule_R C \<^bold>[A \<^bold>=\<beta>\<^bold>= B\<^bold>] C'"
+    using by_rule_R by auto
+  then have "replacement A B C C'"
+    using Eql_def rule_R.cases by fastforce
+  show ?case
+    using theorem_5402_a_rule_R[of A B \<beta> C C' Tv] by_rule_R.IH R
+      A_B_\<beta>_p C_isa_Tv by auto
+qed
+
+(* Corresponds to Andrews' theorem 5402 a *)
+theorem theorem_5402_a_standard:
+  assumes "theorem A"
+  shows "valid_standard A"
+  using theorem_5402_a_general assms standard_model_is_general_model valid_general_def 
+    valid_standard_def by blast
+
+end
+
+end
diff --git a/thys/Q0_Soundness/ROOT b/thys/Q0_Soundness/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Q0_Soundness/ROOT
@@ -0,0 +1,14 @@
+chapter AFP
+
+session Q0_Soundness = "HOL-ZF" +
+  options [timeout = 300]
+  sessions
+    ZFC_in_HOL
+  theories
+    Set_Theory
+    HOLZF_Set_Theory
+    ZFC_in_HOL_Set_Theory
+    Q0
+  document_files
+    "root.bib"
+    "root.tex"
diff --git a/thys/Q0_Soundness/Set_Theory.thy b/thys/Q0_Soundness/Set_Theory.thy
new file mode 100644
--- /dev/null
+++ b/thys/Q0_Soundness/Set_Theory.thy
@@ -0,0 +1,594 @@
+section \<open>Set Theory\<close>
+
+theory Set_Theory imports Main begin
+
+
+subsection \<open>CakeML License\<close>
+
+text \<open>
+CakeML Copyright Notice, License, and Disclaimer.
+
+Copyright 2013-2023 by Anthony Fox, Google LLC, Ramana Kumar, Magnus Myreen,
+Michael Norrish, Scott Owens, Yong Kiam Tan, and other contributors listed
+at https://cakeml.org
+
+All rights reserved.
+
+CakeML is free software. Redistribution and use in source and binary forms,
+with or without modification, are permitted provided that the following
+conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above copyright
+      notice, this list of conditions and the following disclaimer in the
+      documentation and/or other materials provided with the distribution.
+
+    * The names of the copyright holders and contributors may not be
+      used to endorse or promote products derived from this software without
+      specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ``AS IS''
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+\<close>
+
+
+subsection \<open>Set theory specification\<close>
+
+text \<open>
+  This formal document is the set theory from 
+  https://github.com/CakeML/cakeml/blob/master/candle/set-theory/setSpecScript.sml
+  ported to Isabelle/HOL and extended.
+\<close>
+
+(* Corresponds to CakeML's constant is_set_theory_def *)
+locale set_theory =
+  fixes mem :: "'s \<Rightarrow> 's \<Rightarrow> bool" (infix "\<in>:" 67)
+  fixes sub :: "'s \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> 's" (infix "suchthat" 67)
+  fixes pow :: "'s \<Rightarrow> 's"
+  fixes uni :: "'s \<Rightarrow> 's" ("\<Union>:_" [900] 900)
+  fixes upair :: "'s \<Rightarrow> 's \<Rightarrow> 's" (infix "+:" 67)
+  assumes extensional: "\<And>x y. x = y \<longleftrightarrow> (\<forall>a. a \<in>: x \<longleftrightarrow> a \<in>: y)"
+  assumes mem_sub[simp]: "\<And>x P a. a \<in>: (x suchthat P) \<longleftrightarrow> a \<in>: x \<and> P a"
+  assumes mem_pow[simp]: "\<And>x a. a \<in>: (pow x) \<longleftrightarrow> (\<forall>b. b \<in>: a \<longrightarrow> b \<in>: x)"
+  assumes mem_uni[simp]: "\<And>x a. a \<in>: \<Union>:x \<longleftrightarrow> (\<exists>b. a \<in>: b \<and> b \<in>: x)"
+  assumes mem_upair[simp]: "\<And>x y a. a \<in>: (x +: y) \<longleftrightarrow> a = x \<or> a = y" 
+begin
+
+(* Corresponds to CakeML's theorem separation_unique *)
+lemma seperation_unique:
+  assumes "\<forall>x P a. a \<in>: (sub2 x P) \<longleftrightarrow> a \<in>: x \<and> P a"
+  shows "sub2 = sub"
+proof
+  fix x
+  show "sub2 x = (suchthat) x"
+    using assms extensional by auto
+qed
+
+(* Corresponds to CakeML's theorem power_unique *)
+lemma pow_unique:
+  assumes "\<forall>x a. a \<in>: (pow2 x) \<longleftrightarrow> (\<forall>b. b \<in>: a \<longrightarrow> b \<in>: x)"
+  shows "pow2 = pow"
+  using assms extensional by auto
+
+(* Corresponds to CakeML's theorem union_unique *)
+lemma uni_unique:
+  assumes "\<forall>x a. a \<in>: uni2 x \<longleftrightarrow> (\<exists>b. a \<in>: b \<and> b \<in>: x)"
+  shows "uni2 = uni"
+  using assms extensional by auto
+
+(* Corresponds to CakeML's theorem upair_unique *)
+lemma upair_unique:
+  assumes "\<forall>x y a. a \<in>: upair2 x y \<longleftrightarrow> a = x \<or> a = y"
+  shows "upair2 = upair"
+proof 
+  fix x 
+  show "upair2 x = (+:) x"
+    using assms extensional by auto
+qed
+
+(* Corresponds to CakeML's Ø *)
+definition empt :: 's ("Ø") where
+ "Ø = undefined suchthat (\<lambda>x. False)" 
+
+(* Corresponds to CakeML's theorem mem_empty *)
+lemma mem_empty[simp]: "\<not>x \<in>: Ø"
+  unfolding empt_def using mem_sub by auto
+
+(* Corresponds to CakeML's constant unit *)
+definition unit :: "'s \<Rightarrow> 's" where
+  "unit x = x +: x"
+
+(* Corresponds to CakeML's theorem mem_unit *)
+lemma mem_unit[simp]: "x \<in>: (unit y) \<longleftrightarrow> x = y"
+  unfolding unit_def using mem_upair by auto
+
+(* Corresponds to CakeML's theorem unit_inj *)
+lemma unit_inj: "unit x = unit y \<longleftrightarrow> x = y"
+  using extensional unfolding unit_def by auto 
+
+(* Corresponds to CakeML's constant one *)
+definition one :: 's where
+  "one = unit Ø"
+
+(* Corresponds to CakeML's theorem mem_one *)
+lemma mem_one[simp]: "x \<in>: one \<longleftrightarrow> x = Ø"
+  unfolding one_def by auto
+
+(* Corresponds to CakeML's constant two *)
+definition two :: 's where
+  "two = Ø +: one"
+
+(* Corresponds to CakeML's theorem mem_two *)
+lemma mem_two[simp]: "\<forall>x. x \<in>: two \<longleftrightarrow> x = Ø \<or> x = one"
+  unfolding two_def by auto 
+
+(* Corresponds to CakeML's constant pair *)
+definition pair :: "'s \<Rightarrow> 's \<Rightarrow> 's" (infix ",:" 50) where
+  "(x,:y) = (unit x) +: (x +: y)"
+
+(* Corresponds to CakeML's theorem upair_inj *)
+lemma upair_inj:
+  "a +: b = c +: d \<longleftrightarrow> a = c \<and> b = d \<or> a = d \<and> b = c"
+  using extensional by auto
+
+(* Corresponds to CakeML's theorem unit_eq_upair *)
+lemma unit_eq_upair:
+  "unit x = y +: z \<longleftrightarrow> x = y \<and> y = z"
+  using extensional mem_unit mem_upair by metis
+
+(* Corresponds to CakeML's theorem pair_inj *)
+lemma pair_inj:
+  "(a,:b) = (c,:d) \<longleftrightarrow> a = c \<and> b = d"
+  using pair_def upair_inj unit_inj unit_eq_upair by metis
+
+(* Corresponds to CakeML's constant binary_uni *)
+definition binary_uni (infix "\<union>:" 67) where
+  "x \<union>: y = \<Union>: (x +: y)"
+
+(* Corresponds to CakeML's theorem mem_binary_uni *)
+lemma mem_binary_uni[simp]:
+  "a \<in>: (x \<union>: y) \<longleftrightarrow> a \<in>: x \<or> a \<in>: y"
+  unfolding binary_uni_def by auto
+
+(* Corresponds to CakeML's constant product *)
+definition product :: "'s \<Rightarrow> 's \<Rightarrow> 's" (infix "\<times>:" 67) where
+  "x \<times>: y = (pow (pow (x \<union>: y)) suchthat (\<lambda>a. \<exists>b c. b \<in>: x \<and> c \<in>: y \<and> a = (b,:c)))"
+
+(* Corresponds to CakeML's theorem mem_product *)
+lemma mem_product[simp]:
+  "a \<in>: (x \<times>: y) \<longleftrightarrow> (\<exists>b c. a = (b,:c) \<and> b \<in>: x \<and> c \<in>: y)"
+  using product_def pair_def by auto
+
+(* Corresponds to CakeML's constant product *)
+definition relspace where
+  "relspace x y = pow (x \<times>: y)"
+
+(* Corresponds to CakeML's constant funspace *)
+definition funspace where
+  "funspace x y =
+    (relspace x y suchthat
+     (\<lambda>f. \<forall>a. a \<in>: x \<longrightarrow> (\<exists>!b. (a,:b) \<in>: f)))"
+
+(* Corresponds to CakeML's constant apply *)
+definition "apply" :: "'s \<Rightarrow> 's \<Rightarrow> 's" (infixl "\<cdot>" 68) where
+  "(x\<cdot>y) = (SOME a. (y,:a) \<in>: x)"
+
+(* Corresponds to CakeML's overloading of boolset *)
+definition boolset where
+  "boolset \<equiv> two"
+
+(* Corresponds to CakeML's constant true *)
+definition true where
+  "true = Ø"
+
+(* Corresponds to CakeML's constant false *)
+definition false where
+  "false = one"
+
+(* Corresponds to CakeML's theorem true_neq_false *)
+lemma true_neq_false:
+  "true \<noteq> false"
+  using true_def false_def extensional one_def by auto
+
+(* Corresponds to CakeML's theorem mem_boolset *)
+lemma mem_boolset[simp]:
+  "x \<in>: boolset \<longleftrightarrow> ((x = true) \<or> (x = false))"
+  using true_def false_def boolset_def by auto
+
+(* Corresponds to CakeML's constant boolean *)
+definition boolean :: "bool \<Rightarrow> 's" where
+  "boolean b = (if b then true else false)"
+
+(* Corresponds to CakeML's theorem boolean_in_boolset *)
+lemma boolean_in_boolset:
+  "boolean b \<in>: boolset"
+  using boolean_def one_def true_def false_def by auto
+
+(* Corresponds to CakeML's theorem boolean_eq_true *)
+lemma boolean_eq_true:
+  "boolean b = true \<longleftrightarrow> b"
+  using boolean_def true_neq_false by auto
+
+(* Corresponds to CakeML's constant holds *)
+definition "holds s x \<longleftrightarrow> s \<cdot> x = true"
+
+(* Corresponds to CakeML's constant abstract *)
+definition abstract where
+  "abstract doma rang f = ((doma \<times>: rang) suchthat (\<lambda>x. \<exists>a. x = (a,:f a)))"
+
+(* Corresponds to CakeML's theorem apply_abstract *)
+lemma apply_abstract[simp]:
+  "x \<in>: s \<Longrightarrow> f x \<in>: t \<Longrightarrow> abstract s t f \<cdot> x = f x"
+  using apply_def abstract_def pair_inj by auto
+
+(* Corresponds to CakeML's theorem apply_abstract_matchable *)
+lemma apply_abstract_matchable:
+  "x \<in>: s \<Longrightarrow> f x \<in>: t \<Longrightarrow> f x = u \<Longrightarrow> abstract s t f \<cdot> x = u"
+  using apply_abstract by auto
+
+(* Corresponds to CakeML's theorem apply_in_rng *)
+lemma apply_in_rng:
+  assumes "x \<in>: s"
+  assumes "f \<in>: funspace s t"
+  shows "f \<cdot> x \<in>: t"
+proof -
+  from assms have "f \<in>: (relspace s t suchthat (\<lambda>f. \<forall>a. a \<in>: s \<longrightarrow> (\<exists>!b. (a ,: b) \<in>: f)))"
+    unfolding funspace_def by auto
+  then have f_p: "f \<in>: relspace s t \<and> (\<forall>a. a \<in>: s \<longrightarrow> (\<exists>!b. (a ,: b) \<in>: f))"
+    by auto
+  then have fxf: "(x ,: f \<cdot> x) \<in>: f"
+    using someI assms apply_def by metis
+  from f_p have "f \<in>: pow (s \<times>: t)"
+    unfolding relspace_def by auto
+  then have "(x ,: f \<cdot> x) \<in>: (s \<times>: t)"
+    using fxf by auto
+  then show ?thesis
+    using pair_inj by auto
+qed
+
+(* Corresponds to CakeML's theorem abstract_in_funspace  *)
+lemma abstract_in_funspace[simp]:
+  "(\<forall>x. x \<in>: s \<longrightarrow> f x \<in>: t) \<Longrightarrow> abstract s t f \<in>: funspace s t"
+  using funspace_def relspace_def abstract_def pair_inj by auto
+
+(* Corresponds to CakeML's theorem abstract_in_funspace_matchable *)
+lemma abstract_in_funspace_matchable:
+  "(\<forall>x. x \<in>: s \<longrightarrow> f x \<in>: t) \<Longrightarrow> fs = funspace s t \<Longrightarrow> abstract s t f \<in>: fs"
+  using abstract_in_funspace by auto
+
+(* Corresponds to CakeML's theorem abstract_eq *)
+lemma abstract_eq:
+  assumes "\<forall>x. x \<in>: s \<longrightarrow> f x \<in>: t1 \<and> g x \<in>: t2 \<and> f x = g x"
+  shows "abstract s t1 f = abstract s t2 g"
+proof (rule iffD2[OF extensional], rule)
+  fix a
+  from assms show "a \<in>: abstract s t1 f = a \<in>: abstract s t2 g"
+    unfolding abstract_def using pair_inj by auto
+qed
+
+lemma abstract_extensional:
+  assumes "\<forall>x. x \<in>: s \<longrightarrow> f x \<in>: t \<and> f x = g x"
+  shows "abstract s t f = abstract s t g"
+proof (rule iffD2[OF extensional], rule)
+  fix a
+  from assms show "a \<in>: abstract s t f = a \<in>: abstract s t g"
+    unfolding abstract_def using pair_inj by auto
+qed
+
+lemma abstract_extensional':
+  assumes "\<And>x. x \<in>: s \<Longrightarrow> f x \<in>: t"
+  assumes "\<And>x. x \<in>: s \<Longrightarrow> f x = g x"
+  shows "abstract s t f = abstract s t g"
+proof (rule iffD2[OF extensional], rule)
+  fix a
+  from assms show "a \<in>: abstract s t f = a \<in>: abstract s t g"
+    unfolding abstract_def using pair_inj by auto
+qed
+
+lemma abstract_cong:
+  assumes "\<forall>x. x \<in>: s \<longrightarrow> f x \<in>: t \<and> g x \<in>: t"
+  assumes "abstract s t f = abstract s t g"
+  assumes "x \<in>: s"
+  shows "f x = g x"
+  using assms
+  by (metis apply_abstract_matchable)
+
+lemma abstract_cong_specific:
+  assumes "x \<in>: s"
+  assumes "f x \<in>: t"
+  assumes "abstract s t f = abstract s t g"
+  assumes "g x \<in>: t"
+  shows "f x = g x"
+proof -
+  have "f x = abstract s t f \<cdot> x"
+    using apply_abstract[of x s f t]
+    using assms by auto
+  also have "... = abstract s t g \<cdot> x"
+    using assms by auto
+  also have "... = g x"
+    using apply_abstract[of x s g t]
+    using assms by auto
+  finally show ?thesis 
+    by auto
+qed
+
+lemma abstract_iff_extensional:
+  assumes "\<forall>x. x \<in>: s \<longrightarrow> f x \<in>: t \<and> g x \<in>: t"
+  shows "(abstract s t f = abstract s t g) \<longleftrightarrow> (\<forall>x. x \<in>: s \<longrightarrow> f x \<in>: t \<and> f x = g x)"
+  using assms abstract_cong
+    abstract_extensional by meson
+
+(* Corresponds to CakeML's theorem in_funspace_abstract *)
+lemma in_funspace_abstract[simp]:
+  assumes "z \<in>: funspace s t"
+  shows "\<exists>f. z = abstract s t f \<and> (\<forall>x. x \<in>: s \<longrightarrow> f x \<in>: t)"
+proof -
+  define f where "f = (\<lambda>x. SOME y. (x,:y) \<in>: z)"
+  have "\<forall>x. x \<in>: z \<longleftrightarrow> x \<in>: (abstract s t f)"
+  proof (rule, rule)
+    fix x
+    assume xz: "x \<in>: z"
+    moreover
+    have "\<forall>b. b \<in>: z \<longrightarrow> (\<exists>ba c. b = (ba ,: c) \<and> ba \<in>: s \<and> c \<in>: t)"
+      using xz assms
+      unfolding funspace_def relspace_def by (auto)
+    moreover
+    have "\<forall>a. a \<in>: s \<longrightarrow> (\<exists>!b. (a ,: b) \<in>: z)"
+      using xz using assms
+      unfolding funspace_def relspace_def by auto
+    ultimately
+    have "\<exists>a. x = (a ,: f a)"
+      using assms f_def someI_ex unfolding funspace_def relspace_def by (metis (no_types, lifting))
+    then show "x \<in>: abstract s t f"
+      using xz assms unfolding funspace_def relspace_def abstract_def by auto
+  next
+    fix x 
+    assume xf: "x \<in>: abstract s t f"
+    then have "(\<exists>b c. x = (b ,: c) \<and> b \<in>: s \<and> c \<in>: t)"
+      unfolding abstract_def by simp
+    moreover
+    have "(\<exists>a. x = (a ,: (SOME y. (a ,: y) \<in>: z)))"
+      using xf f_def unfolding abstract_def by simp
+    moreover
+    have "(\<forall>a. a \<in>: s \<longrightarrow> (\<exists>!b. (a ,: b) \<in>: z))"
+      using assms unfolding funspace_def by simp
+    ultimately
+    show "x \<in>: z"
+      using f_def by (metis pair_inj someI_ex)
+  qed
+  then have "z = abstract s t f"
+    using extensional by auto
+  moreover
+  from f_def have "\<forall>x. x \<in>: s \<longrightarrow> f x \<in>: t"
+    using apply_in_rng assms local.apply_def by force
+  ultimately
+  show ?thesis
+    by auto   
+qed
+
+(* Corresponds to CakeML's theorem axiom_of_choice *)
+theorem axiom_of_choice:
+  assumes "\<forall>a. a \<in>: x \<longrightarrow> (\<exists>b. b \<in>: a)"
+  shows "\<exists>f. \<forall>a. a \<in>: x \<longrightarrow> f \<cdot> a \<in>: a"
+proof -
+  define f where "f = (\<lambda>a. SOME b. mem b a)"
+  define fa where "fa = abstract x (uni x) f"
+
+  have "\<forall>a. a \<in>: x \<longrightarrow> fa \<cdot> a \<in>: a"
+  proof (rule, rule)
+    fix a
+    assume "a \<in>: x"
+    moreover
+    have "f a \<in>: \<Union>:x"
+      by (metis (full_types) assms calculation f_def mem_uni someI_ex)
+    moreover
+    have "f a \<in>: a"
+      using assms calculation(1) f_def someI_ex by force
+    ultimately
+    show "fa \<cdot> a \<in>: a"
+      unfolding fa_def using apply_abstract by auto
+  qed
+  then show ?thesis
+    by auto
+qed
+
+(* Corresponds to CakeML's constant is_infinite *)
+definition is_infinite where
+  "is_infinite s = infinite {a. a \<in>: s}"
+
+(* Corresponds to CakeML's theorem funspace_inhabited *)
+lemma funspace_inhabited:
+  "(\<exists>x. x \<in>: s) \<Longrightarrow> (\<exists>x. x \<in>: t) \<Longrightarrow> (\<exists>f. f \<in>: funspace s t)"
+  apply (rule exI[of _ "abstract s t (\<lambda>x. SOME x. x \<in>: t)"])
+  using abstract_in_funspace
+  using someI by metis 
+
+(* Corresponds to CakeML's constant tuple *)
+fun tuple where
+  "tuple [] = Ø" |
+  "tuple (a#as) = (a,: tuple as)"
+
+(* Corresponds to CakeML's theorem pair_not_empty *)
+lemma pair_not_empty:
+  "(x,:y) \<noteq> Ø"
+  apply rule
+  unfolding extensional using mem_empty pair_def mem_upair by metis
+
+(* Corresponds to CakeML's theorem tuple_empty *)
+lemma tuple_empty:
+  "tuple ls = Ø \<longleftrightarrow> ls = []"
+  using pair_not_empty by (cases ls) auto
+
+(* Corresponds to CakeML's theorem tuple_inj *)
+lemma tuple_inj:
+  "tuple l1 = tuple l2 \<longleftrightarrow> l1 = l2"
+proof (induction l1 arbitrary: l2)
+  case Nil
+  then show ?case 
+    using tuple_empty by metis
+next
+  case (Cons a l1)
+  then show ?case
+    using pair_not_empty pair_inj by (metis tuple.elims tuple.simps(2))
+qed
+
+(* Corresponds to CakeML's constant bigcross *)
+fun bigcross where
+  "bigcross [] = one" |
+  "bigcross (a#as) = a \<times>: (bigcross as)"
+
+(* Corresponds to CakeML's theorem mem_bigcross *)
+lemma mem_bigcross[simp]:
+  "x \<in>: (bigcross ls) \<longleftrightarrow> (\<exists>xs. x = tuple xs \<and> list_all2 mem xs ls)"
+proof (induction ls arbitrary: x)
+  case Nil
+  then show ?case 
+    using mem_one mem_product by simp
+next
+  case (Cons l ls)
+  show ?case 
+  proof
+    assume "x \<in>: bigcross (l # ls)"
+    then obtain b c where bc_p: "x = (b ,: c) \<and> b \<in>: l \<and> c \<in>: bigcross ls " 
+      by auto
+    then obtain xs' where "c = tuple xs' \<and> list_all2 (\<in>:) xs' ls" 
+      using Cons[of c] by auto
+    then have "x = tuple (b#xs') \<and> list_all2 (\<in>:) (b#xs') (l # ls)"
+      using bc_p by auto
+    then show "\<exists>xs. x = tuple xs \<and> list_all2 (\<in>:) xs (l # ls)"
+      by metis
+  next 
+    assume "\<exists>xs. x = tuple xs \<and> list_all2 (\<in>:) xs (l # ls)"
+    then obtain xs where "x = tuple xs \<and> list_all2 (\<in>:) xs (l # ls)"
+      by auto
+    then obtain xs where "x = tuple xs \<and> list_all2 (\<in>:) xs (l # ls)"
+      by auto
+    then show "x \<in>: bigcross (l # ls)"
+      using Cons list.distinct(1) list.rel_cases mem_product by fastforce
+  qed
+qed
+
+definition subs :: "'s \<Rightarrow> 's \<Rightarrow> bool" (infix "\<subseteq>:" 67) where
+  "x \<subseteq>: y \<longleftrightarrow> x \<in>: pow y"
+
+
+definition one_elem_fun :: "'s \<Rightarrow> 's \<Rightarrow> 's" where
+  "one_elem_fun x d = abstract d boolset (\<lambda>y. boolean (x=y))"
+
+definition iden :: "'s \<Rightarrow> 's" where
+  "iden D = abstract D (funspace D boolset) (\<lambda>x. one_elem_fun x D)"
+
+lemma apply_id[simp]:
+  assumes A_in_D: "A \<in>: D"
+  assumes B_in_D: "B \<in>: D"
+  shows "iden D \<cdot> A \<cdot> B = boolean (A = B)"
+proof -
+  have abstract_D: "abstract D boolset (\<lambda>y. boolean (A = y)) \<in>: funspace D boolset"
+    using boolean_in_boolset by auto
+  have bool_in_two: "boolean (A = B) \<in>: boolset"
+    using boolean_in_boolset by blast
+  have "(boolean (A = B)) = (abstract D boolset (\<lambda>y. boolean (A = y)) \<cdot> B)"
+    using apply_abstract[of B D "\<lambda>y. boolean (A = y)" two] B_in_D bool_in_two by auto
+  also
+  have "... = (abstract D (funspace D boolset) (\<lambda>x. abstract D boolset (\<lambda>y. boolean (x = y))) \<cdot> A) \<cdot> B" 
+    using A_in_D abstract_D 
+      apply_abstract[of A D "\<lambda>x. abstract D boolset (\<lambda>y. boolean (x = y))" "funspace D boolset"]
+    by auto 
+  also
+  have "... = iden D \<cdot> A \<cdot> B"
+    unfolding iden_def one_elem_fun_def ..
+  finally
+  show ?thesis
+    by auto
+qed
+
+lemma apply_id_true[simp]:
+  assumes A_in_D: "A \<in>: D"
+  assumes B_in_D: "B \<in>: D"
+  shows "iden D \<cdot> A \<cdot> B = true \<longleftrightarrow> A = B"
+  using assms using boolean_def using true_neq_false by auto
+
+lemma apply_if_pair_in:
+  assumes "(a1,: a2) \<in>: f"
+  assumes "f \<in>: funspace s t"
+  shows "f \<cdot> a1 = a2"
+  using assms
+  by (smt abstract_def apply_abstract mem_product pair_inj set_theory.in_funspace_abstract 
+      set_theory.mem_sub set_theory_axioms)
+
+lemma funspace_app_unique:
+  assumes "f \<in>: funspace s t"
+  assumes "(a1,: a2) \<in>: f"
+  assumes "(a1,: a3) \<in>: f"
+  shows "a3 = a2"
+  using assms apply_if_pair_in by blast
+
+lemma funspace_extensional:
+  assumes "f \<in>: funspace s t"
+  assumes "g \<in>: funspace s t"
+  assumes "\<forall>x. x \<in>: s \<longrightarrow> f \<cdot> x = g \<cdot> x"
+  shows "f = g"
+proof -
+  have "\<And>a. a \<in>: f \<Longrightarrow> a \<in>: g"
+  proof -
+    fix a
+    assume af: "a \<in>: f"
+    from af have "\<exists>a1 a2. a1 \<in>:s \<and> a2 \<in>: t \<and> (a1 ,: a2) = a"
+      using assms unfolding funspace_def apply_def using relspace_def by force
+    then obtain a1 a2 where a12:
+      "a1 \<in>:s \<and> a2 \<in>: t \<and> (a1 ,: a2) = a"
+      by blast
+    then have "\<exists>a3. a2 \<in>: t \<and> (a1 ,: a3) \<in>: g"
+      using assms(2) funspace_def by auto
+    then obtain a3 where a3: "a2 \<in>: t \<and> (a1 ,: a3) \<in>: g"
+      by auto
+    then have "a3 = a2"
+      using a12 af assms(1,2,3) apply_if_pair_in by auto
+    then show "a \<in>: g"
+      using a12 a3 by blast
+  qed
+  moreover
+  have "\<And>a. a \<in>: g \<Longrightarrow> a \<in>: f"
+  proof -
+    fix a
+    assume ag: "a \<in>: g"
+    then have "\<exists>a1 a2. a1 \<in>:s \<and> a2 \<in>: t \<and> (a1 ,: a2) = a"
+      using assms unfolding funspace_def apply_def using relspace_def by force
+    then obtain a1 a2 where a12:
+      "a1 \<in>:s \<and> a2 \<in>: t \<and> (a1 ,: a2) = a"
+      by blast
+    then have "\<exists>a3. a2 \<in>: t \<and> (a1 ,: a3) \<in>: f"
+      using assms(1) funspace_def by auto
+    then obtain a3 where a3: "a2 \<in>: t \<and> (a1 ,: a3) \<in>: f"
+      by auto
+    then have "a3 = a2"
+      using a12 ag assms(1,2,3) apply_if_pair_in by auto
+    then show "a \<in>: f"
+      using a3 a12 by blast
+  qed
+  ultimately
+  show ?thesis 
+    using iffD2[OF extensional] by metis
+qed
+
+lemma funspace_difference_witness:
+  assumes "f \<in>: funspace s t"
+  assumes "g \<in>: funspace s t"
+  assumes "f \<noteq> g"
+  shows "\<exists>z. z \<in>: s \<and> f \<cdot> z \<noteq> g \<cdot> z"
+  using assms(1,2,3) funspace_extensional by blast
+
+
+end
+
+end
diff --git a/thys/Q0_Soundness/ZFC_in_HOL_Set_Theory.thy b/thys/Q0_Soundness/ZFC_in_HOL_Set_Theory.thy
new file mode 100644
--- /dev/null
+++ b/thys/Q0_Soundness/ZFC_in_HOL_Set_Theory.thy
@@ -0,0 +1,34 @@
+section \<open>ZFC\_in\_HOL lives up to CakeML's set theory specification\<close>
+
+theory ZFC_in_HOL_Set_Theory imports ZFC_in_HOL.ZFC_in_HOL Set_Theory begin
+
+interpretation set_theory "\<lambda>x y. x \<in> elts y" "\<lambda>x::V. \<lambda>P. (inv elts) ({y. y \<in> elts x \<and> P y})" VPow
+  "(\<lambda>Y. SOME Z. elts Z = \<Union>(elts ` (elts Y)))" "\<lambda>x y::V. (inv elts) {x, y}"
+  apply unfold_locales
+  subgoal for x y
+    apply blast
+    done
+  subgoal for x P a
+    apply (rule iffI)
+    subgoal
+      using mem_Collect_eq set_of_elts ZFC_in_HOL.set_def subsetI small_iff smaller_than_small 
+      apply smt
+      done
+    subgoal
+      using elts_0 elts_of_set empty_iff f_inv_into_f mem_Collect_eq set_of_elts small_def 
+        small_elts subset_eq subset_iff_less_eq_V zero_V_def
+      apply (smt ZFC_in_HOL.set_def down subsetI)
+      done
+    done
+  subgoal for x a
+    apply blast
+    done
+  subgoal for x a
+    apply (metis (mono_tags) UN_iff elts_Sup small_elts tfl_some)
+    done
+  subgoal for x y a
+    apply (metis ZFC_in_HOL.set_def elts_of_set insert_iff singletonD small_upair)
+    done
+  done
+
+end
diff --git a/thys/Q0_Soundness/document/root.bib b/thys/Q0_Soundness/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Q0_Soundness/document/root.bib
@@ -0,0 +1,390 @@
+@book{andrews2013introduction,
+  title={An introduction to mathematical logic and type theory: to truth through proof},
+  author={Andrews, Peter B.},
+  volume={27},
+  year={2013},
+  edition = {2nd},
+  series={Applied Logic Series},
+  publisher={Springer Science \& Business Media}
+}
+
+@inproceedings{DBLP:conf/itp/AbrahamssonMKS22,
+  author       = {Oskar Abrahamsson and
+                  Magnus O. Myreen and
+                  Ramana Kumar and
+                  Thomas Sewell},
+  editor       = {June Andronick and
+                  Leonardo de Moura},
+  title        = {Candle: {A} Verified Implementation of {HOL Light}},
+  booktitle    = {13th International Conference on Interactive Theorem Proving, {ITP}
+                  2022, August 7-10, 2022, Haifa, Israel},
+  series       = {LIPIcs},
+  volume       = {237},
+  pages        = {3:1--3:17},
+  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
+  year         = {2022},
+  url          = {https://doi.org/10.4230/LIPIcs.ITP.2022.3},
+  doi          = {10.4230/LIPIcs.ITP.2022.3},
+  timestamp    = {Mon, 26 Jun 2023 20:47:39 +0200},
+  biburl       = {https://dblp.org/rec/conf/itp/AbrahamssonMKS22.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{DBLP:journals/jar/KumarAMO16,
+  author       = {Ramana Kumar and
+                  Rob Arthan and
+                  Magnus O. Myreen and
+                  Scott Owens},
+  title        = {Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and
+                  a Verified Implementation},
+  journal      = {J. Autom. Reason.},
+  volume       = {56},
+  number       = {3},
+  pages        = {221--259},
+  year         = {2016},
+  url          = {https://doi.org/10.1007/s10817-015-9357-x},
+  doi          = {10.1007/s10817-015-9357-x},
+  timestamp    = {Wed, 02 Sep 2020 13:29:45 +0200},
+  biburl       = {https://dblp.org/rec/journals/jar/KumarAMO16.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/itp/KumarAMO14,
+  author       = {Ramana Kumar and
+                  Rob Arthan and
+                  Magnus O. Myreen and
+                  Scott Owens},
+  editor       = {Gerwin Klein and
+                  Ruben Gamboa},
+  title        = {{HOL} with Definitions: Semantics, Soundness, and a Verified Implementation},
+  booktitle    = {Interactive Theorem Proving - 5th International Conference, {ITP}
+                  2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
+                  Austria, July 14-17, 2014. Proceedings},
+  series       = {Lecture Notes in Computer Science},
+  volume       = {8558},
+  pages        = {308--324},
+  publisher    = {Springer},
+  year         = {2014},
+  url          = {https://doi.org/10.1007/978-3-319-08970-6\_20},
+  doi          = {10.1007/978-3-319-08970-6\_20},
+  timestamp    = {Tue, 14 May 2019 10:00:37 +0200},
+  biburl       = {https://dblp.org/rec/conf/itp/KumarAMO14.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/itp/AbrahamssonM23,
+  author       = {Oskar Abrahamsson and
+                  Magnus O. Myreen},
+  editor       = {Adam Naumowicz and
+                  Ren{\'{e}} Thiemann},
+  title        = {Fast, Verified Computation for {Candle}},
+  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
+                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
+  series       = {LIPIcs},
+  volume       = {268},
+  pages        = {4:1--4:17},
+  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
+  year         = {2023},
+  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.4},
+  doi          = {10.4230/LIPICS.ITP.2023.4},
+  timestamp    = {Wed, 26 Jul 2023 17:17:16 +0200},
+  biburl       = {https://dblp.org/rec/conf/itp/AbrahamssonM23.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/cade/Harrison06,
+  author       = {John Harrison},
+  editor       = {Ulrich Furbach and
+                  Natarajan Shankar},
+  title        = {Towards Self-verification of {HOL Light}},
+  booktitle    = {Automated Reasoning, Third International Joint Conference, {IJCAR}
+                  2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
+  series       = {Lecture Notes in Computer Science},
+  volume       = {4130},
+  pages        = {177--191},
+  publisher    = {Springer},
+  year         = {2006},
+  url          = {https://doi.org/10.1007/11814771\_17},
+  doi          = {10.1007/11814771\_17},
+  timestamp    = {Thu, 05 Sep 2019 14:51:32 +0200},
+  biburl       = {https://dblp.org/rec/conf/cade/Harrison06.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{Metalogic_ProofChecker-AFP,
+  author  = {Tobias Nipkow and Simon Ro{\ss}kopf},
+  title   = {Isabelle's Metalogic: Formalization and Proof Checker},
+  journal = {Archive of Formal Proofs},
+  month   = {April},
+  year    = {2021},
+  note    = {\url{https://isa-afp.org/entries/Metalogic_ProofChecker.html},
+             Formal proof development},
+  ISSN    = {2150-914x},
+}
+
+@article{DBLP:journals/jar/RosskopfN23,
+  author       = {Simon Ro{\ss}kopf and
+                  Tobias Nipkow},
+  title        = {A Formalization and Proof Checker for {Isabelle's} Metalogic},
+  journal      = {J. Autom. Reason.},
+  volume       = {67},
+  number       = {1},
+  pages        = {1},
+  year         = {2023},
+  url          = {https://doi.org/10.1007/s10817-022-09648-w},
+  doi          = {10.1007/s10817-022-09648-w},
+  timestamp    = {Tue, 28 Feb 2023 10:48:15 +0100},
+  biburl       = {https://dblp.org/rec/journals/jar/RosskopfN23.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/cade/NipkowR21,
+  author       = {Tobias Nipkow and
+                  Simon Ro{\ss}kopf},
+  editor       = {Andr{\'{e}} Platzer and
+                  Geoff Sutcliffe},
+  title        = {Isabelle's Metalogic: Formalization and Proof Checker},
+  booktitle    = {Automated Deduction - {CADE} 28 - 28th International Conference on
+                  Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
+  series       = {Lecture Notes in Computer Science},
+  volume       = {12699},
+  pages        = {93--110},
+  publisher    = {Springer},
+  year         = {2021},
+  url          = {https://doi.org/10.1007/978-3-030-79876-5\_6},
+  doi          = {10.1007/978-3-030-79876-5\_6},
+  timestamp    = {Thu, 29 Jul 2021 13:42:16 +0200},
+  biburl       = {https://dblp.org/rec/conf/cade/NipkowR21.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/cpp/KochK22,
+  author       = {Mark Koch and
+                  Dominik Kirst},
+  editor       = {Andrei Popescu and
+                  Steve Zdancewic},
+  title        = {Undecidability, incompleteness, and completeness of second-order logic
+                  in Coq},
+  booktitle    = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
+                  Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
+  pages        = {274--290},
+  publisher    = {{ACM}},
+  year         = {2022},
+  url          = {https://doi.org/10.1145/3497775.3503684},
+  doi          = {10.1145/3497775.3503684},
+  timestamp    = {Sat, 30 Sep 2023 09:37:48 +0200},
+  biburl       = {https://dblp.org/rec/conf/cpp/KochK22.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/ictac/Obua06,
+  author       = {Steven Obua},
+  editor       = {Kamel Barkaoui and
+                  Ana Cavalcanti and
+                  Antonio Cerone},
+  title        = {Partizan Games in {Isabelle/HOLZF}},
+  booktitle    = {Theoretical Aspects of Computing - {ICTAC} 2006, Third International
+                  Colloquium, Tunis, Tunisia, November 20-24, 2006, Proceedings},
+  series       = {Lecture Notes in Computer Science},
+  volume       = {4281},
+  pages        = {272--286},
+  publisher    = {Springer},
+  year         = {2006},
+  url          = {https://doi.org/10.1007/11921240\_19},
+  doi          = {10.1007/11921240\_19},
+  timestamp    = {Mon, 21 Feb 2022 14:40:49 +0100},
+  biburl       = {https://dblp.org/rec/conf/ictac/Obua06.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{ZFC_in_HOL-AFP,
+  author  = {Lawrence C. Paulson},
+  title   = {Zermelo {Fraenkel} Set Theory in Higher-Order Logic},
+  journal = {Archive of Formal Proofs},
+  month   = {October},
+  year    = {2019},
+  note    = {\url{https://isa-afp.org/entries/ZFC_in_HOL.html},
+             Formal proof development},
+  ISSN    = {2150-914x},
+}
+
+@article{DBLP:journals/pacmpl/SozeauBFTW20,
+  author       = {Matthieu Sozeau and
+                  Simon Boulier and
+                  Yannick Forster and
+                  Nicolas Tabareau and
+                  Th{\'{e}}o Winterhalter},
+  title        = {{Coq} {Coq} correct! verification of type checking and erasure for {Coq},
+                  in {Coq}},
+  journal      = {Proc. {ACM} Program. Lang.},
+  volume       = {4},
+  number       = {{POPL}},
+  pages        = {8:1--8:28},
+  year         = {2020},
+  url          = {https://doi.org/10.1145/3371076},
+  doi          = {10.1145/3371076},
+  timestamp    = {Sat, 30 Sep 2023 10:23:24 +0200},
+  biburl       = {https://dblp.org/rec/journals/pacmpl/SozeauBFTW20.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/types/Barras96,
+  author       = {Bruno Barras},
+  editor       = {Eduardo Gim{\'{e}}nez and
+                  Christine Paulin{-}Mohring},
+  title        = {Verification of the Interface of a Small Proof System in {Coq}},
+  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
+                  France, December 15-19, 1996, Selected Papers},
+  series       = {Lecture Notes in Computer Science},
+  volume       = {1512},
+  pages        = {28--45},
+  publisher    = {Springer},
+  year         = {1996},
+  url          = {https://doi.org/10.1007/BFb0097785},
+  doi          = {10.1007/BFB0097785},
+  timestamp    = {Tue, 14 May 2019 10:00:42 +0200},
+  biburl       = {https://dblp.org/rec/conf/types/Barras96.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@techreport{barras:inria-00073667,
+  TITLE = {{Coq en Coq}},
+  AUTHOR = {Barras, Bruno},
+  URL = {https://inria.hal.science/inria-00073667},
+  NOTE = {Projet COQ, \url{https://inria.hal.science/inria-00073667}},
+  TYPE = {Research Report},
+  NUMBER = {RR-3026},
+  INSTITUTION = {{INRIA}},
+  YEAR = {1996},
+  KEYWORDS = {TYPE THEORY ; METATHEORY ; CALCULUS OF CONSTRUCTIONS ; PROGRAM EXTRACTION},
+  PDF = {https://inria.hal.science/inria-00073667/file/RR-3026.pdf},
+  HAL_ID = {inria-00073667},
+  HAL_VERSION = {v1},
+}
+
+@techreport{coqincoqmanuscript,
+  title = {{Coq} in {Coq} (manuscript)},
+  author = {Bruno Barras and Benjamin Werner},
+  year = {1996},
+  note = {\url{http://www.lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf}}
+}
+
+@inproceedings{coqincoqcontribs,
+  title={coq-in-coq},
+  author={Bruno Barras},
+  booktitle={coq-contribs},
+  note={\url{https://github.com/coq-contribs/coq-in-coq}},
+  year={1997}
+}
+
+@misc{arthan1993,
+  title={{HOL} Formalised: Language and Overview},
+  author={Arthan, Rob},
+  year={1993, revised 2014},
+  note={\url{http://www.lemma-one.com/ProofPower/specs/specs.html}}
+}
+
+@misc{arthan1991sem,
+  title={{HOL} Formalised: Semantics},
+  author={Arthan, Rob},
+  year={1993, revised 2014},
+  note={\url{http://www.lemma-one.com/ProofPower/specs/specs.html}}
+}
+
+@misc{arthan1991ded,
+  title={{HOL} Formalised: Deductive System},
+  author={Arthan, Rob},
+  year={1993, revised 2002},
+  note={\url{http://www.lemma-one.com/ProofPower/specs/specs.html}}
+}
+
+@article{russell1908mathematical,
+  title={Mathematical logic as based on the theory of types},
+  author={Russell, Bertrand},
+  journal={American journal of mathematics},
+  volume={30},
+  number={3},
+  pages={222--262},
+  year={1908}
+}
+
+@book{whiteheadrussel,
+  title={Principia Mathematica},
+  author={Alfred North Whitehead and Bertrand Russell},
+  publisher={Cambridge University Press, Cambridge England},
+  year={1913},
+  note={3 volumes; first edition 1913, second edition 1927}
+}
+
+@article{church1940formulation,
+  title={A formulation of the simple theory of types},
+  author={Church, Alonzo},
+  journal={The journal of symbolic logic},
+  volume={5},
+  number={2},
+  pages={56--68},
+  year={1940},
+  publisher={Cambridge University Press}
+}
+  
+@article{henkin1950completeness,
+  title={Completeness in the theory of types},
+  author={Henkin, Leon},
+  journal={The Journal of Symbolic Logic},
+  volume={15},
+  number={2},
+  pages={81--91},
+  year={1950},
+  publisher={Cambridge University Press}
+}
+
+@article{henkin1963b,
+  title={A Theory of Propositional Types},
+  author={Henkin, Leon},
+  journal={Fundamenta Mathematicae},
+  volume={52},
+  pages={323--344},
+  year={1963}
+}
+
+@article{andrews1963reduction,
+  title={A reduction of the axioms for the theory of propositional types},
+  author={Andrews, Peter},
+  journal={Fundamenta Mathematicae},
+  volume={52},
+  pages={345--350},
+  year={1963}
+}
+
+@article{andrews1972general,
+  title={General models and extensionality},
+  author={Andrews, Peter B},
+  journal={The Journal of Symbolic Logic},
+  volume={37},
+  number={2},
+  pages={395--397},
+  year={1972},
+  publisher={Cambridge University Press}
+}
+
+@article{Q0_Metatheory-AFP,
+  author  = {Javier D{\'i}az},
+  title   = {Metatheory of {Q0}},
+  journal = {Archive of Formal Proofs},
+  month   = {November},
+  year    = {2023},
+  note    = {\url{https://isa-afp.org/entries/Q0_Metatheory.html},
+             Formal proof development},
+  ISSN    = {2150-914x},
+}
+
+@article{Q0IsaFoL,
+  author  = {Anders Schlichtkrull},
+  title   = {Q0},
+  journal = {IsaFoL},
+  year    = {Jan 4th 2022 - Nov 2023},
+  note    = {Now at GitHub \url{https://github.com/IsaFoL/IsaFoL/tree/master/Q0} but formerly at BitBucket \url{https://bitbucket.org/isafol/isafol/src/master/Q0/}.
+             Formal proof development}
+}
+
+
diff --git a/thys/Q0_Soundness/document/root.tex b/thys/Q0_Soundness/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Q0_Soundness/document/root.tex
@@ -0,0 +1,107 @@
+\documentclass[10pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{amssymb}
+\usepackage[left=15mm,right=15mm,top=20mm,bottom=27mm]{geometry}
+\usepackage{graphicx}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage{pdfsetup}
+
+\urlstyle{tt}
+\isabellestyle{tt}
+
+\renewcommand{\isacharunderscore}{\_}
+\renewcommand{\isachardoublequoteopen}{``}
+\renewcommand{\isachardoublequoteclose}{''}
+
+\begin{document}
+
+\title{Soundness of the Q0 proof system for higher-order logic}
+\author{Anders Schlichtkrull}
+\date{}
+
+\maketitle
+
+\begin{abstract}
+\noindent
+This entry formalizes the Q0 proof system for higher-order logic (also known as simple type theory) from
+the book ``An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof'' 
+by Peter B. Andrews \cite{andrews2013introduction} together with the system's soundness.
+Most of the used theorems and lemmas are also from his book.
+The soundness proof is with respect to general models and as a consequence also holds for standard models.
+Higher-order logic is given a semantics by porting to Isabelle/HOL the
+specification of set theory from the CakeML project \cite{DBLP:conf/itp/KumarAMO14,DBLP:journals/jar/KumarAMO16}.
+The independently developed AFP entry ``Metatheory of Q0'' by Javier D{\'i}az \cite{Q0_Metatheory-AFP} also formalizes Q0 in Isabelle/HOL. 
+I highly recommend the reader to also take a look at his formalization!
+\end{abstract}
+
+\tableofcontents
+
+\newpage
+
+% sane default for proof documents
+\parindent 0pt
+\parskip 0.5ex
+
+\section{Introduction}
+This entry formalizes the Q0 proof system for higher-order logic (also called simple type theory)
+and its soundness.
+Both the system and most of the proven lemmas and
+theorems are from Peter B. Andrews' book \cite{andrews2013introduction}.
+In the book's chapter on type theory, Andrews explains that type theory was invented by
+Russell \cite{russell1908mathematical} and that Whitehead and Russell \cite{whiteheadrussel} showed that fundamental
+parts of mathematics could be formalized in type theory.
+As influences on the type theory presented in Andrews' chapter he mentions Church \cite{church1940formulation}, Henkin \cite{henkin1950completeness,henkin1963b} and earlier works by himself \cite{andrews1963reduction,andrews1972general}.
+The present Isabelle formalization of higher-order logic is given a semantics by using a port to Isabelle/HOL of 
+CakeML's specification of set theory \cite{DBLP:journals/jar/KumarAMO16}.
+The specification is formalized as a locale that fixes a type of set theoretic sets
+and a number of functions (powerset, union, separation) and the set membership predicate.
+The soundness proof is with respect to general models and as a consequence it also holds for standard models.
+Variables are implemented simply using named variables rather than e.g.\ De Bruijn indices or nominal techniques.
+It is well-known that named variables require the definition of substitution to rename variables, but since
+substitution is derived in Q0 rather than built into the proof system this complication is essentially
+circumvented in the present formalization. 
+As a curiosity the present AFP entry also proves that the set theory specification is fulfilled
+by the sets axiomatized in Isabelle/HOLZF \cite{DBLP:conf/ictac/Obua06} and also by the sets axiomatized by the
+AFP entry on Zermelo Fraenkel Set Theory in Higher-Order Logic \cite{ZFC_in_HOL-AFP}.
+The theory files of the present entry appeared in the IsaFoL effort \cite{Q0IsaFoL}.
+
+In the literature we find other formalizations of the metatheory of higher-order logics and type theories.
+Independently from my work here, Javier Díaz also formalizes Q0 in Isabelle/HOL.
+His work is available in the AFP entry ``Metatheory of Q0'' \cite{Q0_Metatheory-AFP}. 
+I highly recommend the reader to take a look also at his very thorough formalization!
+Arthan specifies HOL \cite{arthan1993,arthan1991sem,arthan1991ded} in ProofPower but does not prove soundness.
+John Harrison formalizes the soundness of the proof system of HOL Light \cite{DBLP:conf/cade/Harrison06} in HOL Light
+and Kumar et al.\ \cite{DBLP:conf/itp/KumarAMO14,DBLP:journals/jar/KumarAMO16,DBLP:conf/itp/AbrahamssonMKS22,DBLP:conf/itp/AbrahamssonM23} formalize 
+it in HOL4 as part of the CakeML project including also definitions and a verified implementation.
+Ro{\ss}kopf and Nipkow \cite{DBLP:conf/cade/NipkowR21,Metalogic_ProofChecker-AFP,DBLP:journals/jar/RosskopfN23}
+formalize a proof system for terms in Isabelle's metalogic together with an implementation of a 
+proof checker and prove that the proof checker indeed implements this proof system.
+There are also a number of works using Coq to formalize metatheory of the calculus of constructions and
+the calculus of inductive constructions \cite{DBLP:conf/types/Barras96,barras:inria-00073667,coqincoqmanuscript,coqincoqcontribs,DBLP:journals/pacmpl/SozeauBFTW20}.
+Worth mentioning is also the formalization in Coq of second-order logic which also formalizes general models \cite{DBLP:conf/cpp/KochK22}.
+
+There are plenty of opportunities to go further with the present formalization.
+The present formalization proves soundness of Q0 theorems (i.e. $\vdash A$ implies $\models A$), but not 
+soundness of Q0 derivability (i.e. $M \models G$ and $G \vdash A$ implies $M \models A$).
+Other interesting lemmas and theorems from Andrews' book could also be proved such as e.g.\ derived inference rules and completeness.
+
+\begin{figure}
+\begin{center}
+  \includegraphics[width=0.4\textwidth,keepaspectratio]{session_graph}
+\end{center}
+\caption{Theory dependency graph}
+\label{fig:thys}
+\end{figure}
+
+\newpage
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+\bibliographystyle{alpha}
+\bibliography{root}
+
+\end{document}
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,786 +1,787 @@
 ABY3_Protocols
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AOT
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Ackermanns_not_PR
 Actuarial_Mathematics
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BD_Security_Compositional
 BNF_CC
 BNF_Operations
 BTree
 Balog_Szemeredi_Gowers
 Banach_Steinhaus
 Belief_Revision
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binary_Code_Imprimitive
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Birkhoff_Finite_Distributive_Lattices
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Boolos_Curious_Inference
 Boolos_Curious_Inference_Automated
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CHERI-C_Memory_Model
 CISC-Kernel
 CRDT
 CRYSTALS-Kyber
 CSP_RefTK
 CVP_Hardness
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cardinality_Continuum
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Catoids
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Ceva
 Chandy_Lamport
 Chebyshev_Polynomials
 Chord_Segments
 Circus
 Clean
 Clique_and_Monotone_Circuits
 ClockSynchInst
 Closest_Pair_Points
 CoCon
 CoSMeDis
 CoSMed
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinable_Wands
 Combinatorial_Enumeration_Algorithms
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 CommCSL
 Commuting_Hermitian
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 Cook_Levin
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
 Cotangent_PFD_Formula
 Count_Complex_Roots
 Coupledsim_Contrasim
 CryptHOL
 CryptoBasedCompositionalProperties
 Crypto_Standards
 Cubic_Quartic_Equations
 DCR-ExecutionEquivalence
 DFS_Framework
 DOM_Components
 DPRM_Theorem
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Dedekind_Real
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 DigitsInBase
 Digit_Expansions
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Directed_Sets
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 Disintegration
 DiskPaxos
 Distributed_Distinct_Elements
 Dominance_CHK
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Earley_Parser
 Echelon_Form
 EdmondsKarp_Maxflow
 Edwards_Elliptic_Curves_Group
 Efficient-Mergesort
 Efficient_Weighted_Path_Order
 Elimination_Of_Repeated_Factors
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Equivalence_Relation_Enumeration
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Euler_Polyhedron_Formula
 Eudoxus_Reals
 Eval_FO
 Example-Submission
 Executable_Randomized_Algorithms
 Expander_Graphs
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 FOL_Seq_Calc2
 FOL_Seq_Calc3
 FO_Theory_Rewriting
 FSM_Tests
 Factor_Algebraic_Polynomial
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finite_Fields
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Fishers_Inequality
 Fixed_Length_Vector
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Foundation_of_geometry
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 Frequency_Moments
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Gale_Shapley
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 Given_Clause_Loops
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Gray_Codes
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Hahn_Jordan_Decomposition
 Hales_Jewett
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 HoareForDivergence
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 HyperHoareLogic
 Hyperdual
 Hypergraph_Basics
 Hypergraph_Colourings
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IMP_Compiler_Reuse
 IO_Language_Conformance
 IP_Addresses
 Imperative_Insertion_Sort
 Implicational_Logic
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Independence_CH
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpolation_Polynomials_HOL_Algebra
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Involutions2Squares
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Irrationals_From_THEBOOK
 IsaGeoCoq
 IsaNet
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Khovanskii_Theorem
 Kleene_Algebra
 Kneser_Cauchy_Davenport
 Knights_Tour
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LP_Duality
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Logging_Independent_Anonymity
 Lovasz_Local
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 Lucas_Theorem
 MDP-Algorithms
 MDP-Rewards
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Maximum_Segment_Sum
 Median_Method
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MHComputation
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 MLSS_Decision_Proc
 ML_Unification
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Multirelations_Heterogeneous
 Multiset_Ordering_NPC
 Multitape_To_Singletape_TM
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nano_JSON
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 No_FTL_observers_Gen_Rel
 Nominal2
 Nominal_Myhill_Nerode
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Number_Theoretic_Transform
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PAL
 PAPP_Impossibility
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Package_logic
 Padic_Field
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect_Fields
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Pluennecke_Ruzsa_Inequality
 Poincare_Bendixson
 Poincare_Disc
 Polygonal_Number_Theorem
 Polylog
 Polynomial_Crit_Geometry
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Prefix_Free_Code_Combinators
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Probability_Inequality_Completeness
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Logic_Class
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 Public_Announcement_Logic
 Q0_Metatheory
+Q0_Soundness
 QHLProver
 QR_Decomposition
 Quantales
 Quantales_Converse
 Quantifier_Elimination_Hybrid
 Quasi_Borel_Spaces
 Quaternions
 Query_Optimization
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Real_Power
 Real_Time_Deque
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Registers
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Regular_Tree_Relations
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Cardinality
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rensets
 Rep_Fin_Groups
 ResiduatedTransitionSystem
 Residuated_Lattices
 Resolution_FOL
 Rewrite_Properties_Reduction
 Rewriting_Z
 Ribbon_Proofs
 Risk_Free_Lending
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Roth_Arithmetic_Progressions
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SCC_Bloemen_Sequential
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 S_Finite_Measure_Monad
 Safe_Distance
 Safe_OCL
 Safe_Range_RC
 Saturation_Framework
 Saturation_Framework_Extensions
 Sauer_Shelah_Lemma
 Schutz_Spacetime
 Schwartz_Zippel
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 Separation_Logic_Unbounded
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Clause_Learning
 Simple_Firewall
 Simplex
 Simplicial_complexes_and_boolean_functions
 SimplifiedOntologicalArgument
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Solidity
 Sophomores_Dream
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Stalnaker_Logic
 Standard_Borel_Spaces
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 StrictOmegaCategories
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Suppes_Theorem
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Synthetic_Completeness
 Szemeredi_Regularity
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Three_Squares
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 TsirelsonBound
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Transitive_Models
 Transport
 Treaps
 Tree-Automata
 Tree_Decomposition
 Tree_Enumeration
 Triangle
 Trie
 Turans_Graph_Theorem
 Twelvefold_Way
 Two_Generated_Word_Monoids_Intersection
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Undirected_Graph_Theory
 Universal_Hash_Families
 Universal_Turing_Machine
 UpDown_Scheme
 VYDRA_MDL
 Valuation
 Van_Emde_Boas_Trees
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Weighted_Arithmetic_Geometric_Mean
 Weighted_Path_Order
 Well_Quasi_Orders
 Wetzels_Problem
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 X86_Semantics
 XML
 Youngs_Inequality
 ZFC_in_HOL
 Zeckendorf
 Zeta_3_Irrational
 Zeta_Function
 pGCL
 Labeled_Transition_Systems
 Pushdown_Systems