Theory Elementary_Logic

section ‹Elementary Logic›

theory Elementary_Logic
  imports
    Proof_System
    Propositional_Wff
begin

no_notation funcset (infixr "" 60)
notation funcset (infixr "" 60)

subsection ‹Proposition 5200›

proposition prop_5200:
  assumes "A  wffs⇘α⇙"
  shows " A =⇘αA"
  using assms and equality_reflexivity and dv_thm by simp

corollary hyp_prop_5200:
  assumes "is_hyps " and "A  wffs⇘α⇙"
  shows "  A =⇘αA"
  using derivability_implies_hyp_derivability[OF prop_5200[OF assms(2)] assms(1)] .

subsection ‹Proposition 5201 (Equality Rules)›

proposition prop_5201_1:
  assumes "  A" and "  A 𝒬 B"
  shows "  B"
proof -
  from assms(2) have "  A =⇘oB"
    unfolding equivalence_def .
  with assms(1) show ?thesis
    by (rule rule_R'[where p = "[]"]) auto
qed

proposition prop_5201_2:
  assumes "  A =⇘αB"
  shows "  B =⇘αA"
proof -
  have "  A =⇘αA"
  proof (rule hyp_prop_5200)
    from assms show "is_hyps "
      by (blast elim: is_derivable_from_hyps.cases)
    show "A  wffs⇘α⇙"
      by (fact hyp_derivable_form_is_wffso[OF assms, THEN wffs_from_equality(1)])
  qed
  from this and assms show ?thesis
    by (rule rule_R'[where p = "[«,»]"]) (force+, fastforce dest: subforms_from_app)
qed

proposition prop_5201_3:
  assumes "  A =⇘αB" and "  B =⇘αC"
  shows "  A =⇘αC"
  using assms by (rule rule_R'[where p = "[»]"]) (force+, fastforce dest: subforms_from_app)

proposition prop_5201_4:
  assumes "  A =⇘αβB" and "  C =⇘αD"
  shows "  A · C =⇘βB · D"
proof -
  have "  A · C =⇘βA · C"
  proof (rule hyp_prop_5200)
    from assms show "is_hyps "
      by (blast elim: is_derivable_from_hyps.cases)
    from assms have "A  wffs⇘αβ⇙" and "C  wffs⇘α⇙"
      using hyp_derivable_form_is_wffso and wffs_from_equality by blast+
    then show "A · C  wffs⇘β⇙"
      by auto
  qed
  from this and assms(1) have "  A · C =⇘βB · C"
    by (rule rule_R'[where p = "[»,«]"]) (force+, fastforce dest: subforms_from_app)
  from this and assms(2) show ?thesis
    by (rule rule_R'[where p = "[»,»]"]) (force+, fastforce dest: subforms_from_app)
qed

proposition prop_5201_5:
  assumes "  A =⇘αβB" and "C  wffs⇘α⇙"
  shows "  A · C =⇘βB · C"
proof -
  have "  A · C =⇘βA · C"
  proof (rule hyp_prop_5200)
    from assms(1) show "is_hyps "
      by (blast elim: is_derivable_from_hyps.cases)
    have "A  wffs⇘αβ⇙"
      by (fact hyp_derivable_form_is_wffso[OF assms(1), THEN wffs_from_equality(1)])
    with assms(2) show "A · C  wffs⇘β⇙"
      by auto
  qed
  from this and assms(1) show ?thesis
    by (rule rule_R'[where p = "[»,«]"]) (force+, fastforce dest: subforms_from_app)
qed

proposition prop_5201_6:
  assumes "  C =⇘αD" and "A  wffs⇘αβ⇙"
  shows "  A · C =⇘βA · D"
proof -
  have "  A · C =⇘βA · C"
  proof (rule hyp_prop_5200)
    from assms(1) show "is_hyps "
      by (blast elim: is_derivable_from_hyps.cases)
    have "C  wffs⇘α⇙"
      by (fact hyp_derivable_form_is_wffso[OF assms(1), THEN wffs_from_equality(1)])
    with assms(2) show "A · C  wffs⇘β⇙"
      by auto
  qed
  from this and assms(1) show ?thesis
    by (rule rule_R'[where p = "[»,»]"]) (force+, fastforce dest: subforms_from_app)
qed

lemmas Equality_Rules = prop_5201_1 prop_5201_2 prop_5201_3 prop_5201_4 prop_5201_5 prop_5201_6

subsection ‹Proposition 5202 (Rule RR)›

proposition prop_5202:
  assumes " A =⇘αB   B =⇘αA"
  and "p  positions C" and "A ≼⇘pC" and "Cp  B  D"
  and "  C"
  shows "  D"
proof -
  from assms(5) have " C =⇘oC"
    using prop_5200 and hyp_derivable_form_is_wffso by blast
  moreover from assms(1) consider (a) " A =⇘αB" | (b) " B =⇘αA"
    by blast
  then have " A =⇘αB"
    by cases (assumption, fact Equality_Rules(2))
  ultimately have " C =⇘oD"
    by (rule rule_R[where p = "» # p"]) (use assms(2-4) in auto)
  then have "  C =⇘oD"
  proof -
    from assms(5) have "is_hyps "
      by (blast elim: is_derivable_from_hyps.cases)
    with  C =⇘oD show ?thesis
      by (fact derivability_implies_hyp_derivability)
  qed
  with assms(5) show ?thesis
    by (rule Equality_Rules(1)[unfolded equivalence_def])
qed

lemmas rule_RR = prop_5202 (* synonym *)

subsection ‹Proposition 5203›

proposition prop_5203:
  assumes "A  wffs⇘α⇙" and "B  wffs⇘β⇙"
  and "v  vars A. ¬ is_bound v B"
  shows " (λxα⇙. B) · A =⇘βS {(x, α)  A} B"
using assms(2,1,3) proof induction
  case (var_is_wff β y)
  then show ?case
  proof (cases "yβ= xα⇙")
    case True
    then have "α = β"
      by simp
    moreover from assms(1) have " (λxα⇙. xα) · A =⇘αA"
      using axiom_4_2 by (intro axiom_is_derivable_from_no_hyps)
    moreover have "S {(x, α)  A} (xα) = A"
      by force
    ultimately show ?thesis
      using True by (simp only:)
  next
    case False
    with assms(1) have " (λxα⇙. yβ) · A =⇘βyβ⇙"
      using axiom_4_1_var by (intro axiom_is_derivable_from_no_hyps)
    moreover from False have "S {(x, α)  A} (yβ) = yβ⇙"
      by auto
    ultimately show ?thesis
      by (simp only:)
  qed
next
  case (con_is_wff β c)
  from assms(1) have " (λxα⇙. c⦄⇘β) · A =⇘βc⦄⇘β⇙"
    using axiom_4_1_con by (intro axiom_is_derivable_from_no_hyps)
  moreover have "S {(x, α)  A} (c⦄⇘β) = c⦄⇘β⇙"
    by auto
  ultimately show ?case
    by (simp only:)
next
  case (app_is_wff γ β D C)
  from app_is_wff.prems(2) have not_bound_subforms: "v  vars A. ¬ is_bound v D  ¬ is_bound v C"
    using is_bound_in_app_homomorphism by fast
  from D  wffs⇘γβ⇙› have " (λxα⇙. D) · A =⇘γβS {(x, α)  A} D"
    using app_is_wff.IH(1)[OF assms(1)] and not_bound_subforms by simp
  moreover from C  wffs⇘γ⇙› have " (λxα⇙. C) · A =⇘γS {(x, α)  A} C"
    using app_is_wff.IH(2)[OF assms(1)] and not_bound_subforms by simp
  moreover have " (λxα⇙. D · C) · A =⇘β((λxα⇙. D) · A) · ((λxα⇙. C) · A)"
    using axiom_is_derivable_from_no_hyps[OF axiom_4_3[OF assms(1) D  wffs⇘γβ⇙› C  wffs⇘γ⇙›]] .
  ultimately show ?case
    using Equality_Rules(3,4) and substitute.simps(3) by presburger
next
  case (abs_is_wff β D γ y)
  then show ?case
  proof (cases "yγ= xα⇙")
    case True
    then have " (λxα⇙. λyγ⇙. D) · A =⇘γβλyγ⇙. D"
      using axiom_is_derivable_from_no_hyps[OF axiom_4_5[OF assms(1) abs_is_wff.hyps(1)]] by fast
    moreover from True have "S {(x, α)  A} (λyγ⇙. D) = λyγ⇙. D"
      using empty_substitution_neutrality
      by (simp add: singleton_substitution_simps(4) fmdrop_fmupd_same)
    ultimately show ?thesis
      by (simp only:)
  next
    case False
    have "binders_at (λyγ⇙. D) [«] = {(y, γ)}"
      by simp
    then have "is_bound (y, γ) (λyγ⇙. D)"
      by fastforce
    with abs_is_wff.prems(2) have "(y, γ)  vars A"
      by blast
    with yγ xα⇙› have " (λxα⇙. λyγ⇙. D) · A =⇘γβλyγ⇙. (λxα⇙. D) · A"
      using axiom_4_4[OF assms(1) abs_is_wff.hyps(1)] and axiom_is_derivable_from_no_hyps by blast
    moreover have " (λxα⇙. D) · A =⇘βS {(x, α)  A} D"
    proof -
      have "p. yγ⇙ ≼⇘« # pλyγ⇙. D  yγ⇙ ≼⇘pD"
        using subforms_from_abs by fastforce
      from abs_is_wff.prems(2) have "v  vars A. ¬ is_bound v D"
        using is_bound_in_abs_body by fast
      then show ?thesis
        by (fact abs_is_wff.IH[OF assms(1)])
    qed
    ultimately have " (λxα⇙. λyγ⇙. D) · A =⇘γβλyγ⇙. S {(x, α)  A} D"
      by (rule rule_R[where p = "[»,«]"]) force+
    with False show ?thesis
      by simp
  qed
qed

subsection ‹Proposition 5204›

proposition prop_5204:
  assumes "A  wffs⇘α⇙" and "B  wffs⇘β⇙" and "C  wffs⇘β⇙"
  and " B =⇘βC"
  and "v  vars A. ¬ is_bound v B  ¬ is_bound v C"
  shows " S {(x, α)  A} (B =⇘βC)"
proof -
  have " (λxα⇙. B) · A =⇘β(λxα⇙. B) · A"
  proof -
    have "(λxα⇙. B) · A  wffs⇘β⇙"
      using assms(1,2) by auto
    then show ?thesis
      by (fact prop_5200)
  qed
  from this and assms(4) have " (λxα⇙. B) · A =⇘β(λxα⇙. C) · A"
    by (rule rule_R[where p = "[»,«,«]"]) force+
  moreover from assms(1,2,5) have " (λxα⇙. B) · A =⇘βS {(x, α)  A} B"
    using prop_5203 by auto
  moreover from assms(1,3,5) have " (λxα⇙. C) · A =⇘βS {(x, α)  A} C"
    using prop_5203 by auto
  ultimately have " (S {(x, α)  A} B) =⇘β(S {(x, α)  A} C)"
    using Equality_Rules(2,3) by blast
  then show ?thesis
    by simp
qed

subsection ‹Proposition 5205 ($\eta$-conversion)›

proposition prop_5205:
  shows " 𝔣αβ⇙ =⇘αβ(λyα⇙. 𝔣αβ· yα)"
proof -
  {
  fix y
  assume "yα 𝔵α⇙"
  let ?A = "λyα⇙. 𝔣αβ· yα⇙"
  have " (𝔣αβ⇙ =⇘αβ?A) =⇘o𝔵α⇙. (𝔣αβ· 𝔵α⇙ =⇘β?A · 𝔵α)"
  proof -
    have " (𝔣αβ⇙ =⇘αβ𝔤αβ) =⇘o𝔵α⇙. (𝔣αβ· 𝔵α⇙ =⇘β𝔤αβ· 𝔵α)" (is " ?B =⇘o?C")
      using axiom_3[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
    have " S {(𝔤, αβ)  ?A} (?B =⇘o?C)"
    proof -
      have "?A  wffs⇘αβ⇙" and "?B  wffs⇘o⇙" and "?C  wffs⇘o⇙"
        by auto
      moreover have "v  vars ?A. ¬ is_bound v ?B  ¬ is_bound v ?C"
      proof
        fix v
        assume "v  vars ?A"
        have "vars ?B = {(𝔣, αβ), (𝔤, αβ)}" and "vars ?C = {(𝔣, αβ), (𝔵, α), (𝔤, αβ)}"
          by force+
        with yα 𝔵α⇙› have "(y, α)  vars ?B" and "(y, α)  vars ?C"
          by force+
        then have "¬ is_bound (y, α) ?B" and "¬ is_bound (y, α) ?C"
          using absent_var_is_not_bound by blast+
        moreover have "¬ is_bound (𝔣, αβ) ?B" and "¬ is_bound (𝔣, αβ) ?C"
          by code_simp+
        moreover from v  vars ?A have "v  {(y, α), (𝔣, αβ)}"
          by auto
        ultimately show "¬ is_bound v ?B  ¬ is_bound v ?C"
          by fast
      qed
      ultimately show ?thesis
        using  ?B =⇘o?C and prop_5204 by presburger
    qed
    then show ?thesis
      by simp
  qed
  moreover have " ?A · 𝔵α⇙ =⇘β𝔣αβ· 𝔵α⇙"
  proof -
    have "𝔵α wffs⇘α⇙" and "𝔣αβ· yα wffs⇘β⇙"
      by auto
    moreover have "v  vars (𝔵α). ¬ is_bound v (𝔣αβ· yα)"
      using yα 𝔵α⇙› by auto
    moreover have "S {(y, α)  𝔵α} (𝔣αβ· yα) =  𝔣αβ· 𝔵α⇙"
      by simp
    ultimately show ?thesis
      using prop_5203 by metis
  qed
  ultimately have " (𝔣αβ⇙ =⇘αβ?A) =⇘o𝔵α⇙. (𝔣αβ· 𝔵α⇙ =⇘β𝔣αβ· 𝔵α)"
    by (rule rule_R[where p = "[»,»,«,»]"]) force+
  moreover have " (𝔣αβ⇙ =⇘αβ𝔣αβ) =⇘o𝔵α⇙. (𝔣αβ· 𝔵α⇙ =⇘β𝔣αβ· 𝔵α)"
  proof -
    let ?A = "𝔣αβ⇙"
    have " (𝔣αβ⇙ =⇘αβ𝔤αβ) =⇘o𝔵α⇙. (𝔣αβ· 𝔵α⇙ =⇘β𝔤αβ· 𝔵α)" (is " ?B =⇘o?C")
      using axiom_3[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
    have " S {(𝔤, αβ)  ?A} (?B =⇘o?C)"
    proof -
      have "?A  wffs⇘αβ⇙" and "?B  wffs⇘o⇙" and "?C  wffs⇘o⇙"
        by auto
      moreover have "v  vars ?A. ¬ is_bound v ?B  ¬ is_bound v ?C"
      proof
        fix v
        assume "v  vars ?A"
        have "vars ?B = {(𝔣, αβ), (𝔤, αβ)}" and "vars ?C = {(𝔣, αβ), (𝔵, α), (𝔤, αβ)}"
          by force+
        with yα 𝔵α⇙› have "(y, α)  vars ?B" and "(y, α)  vars ?C"
          by force+
        then have "¬ is_bound (y, α) ?B" and "¬ is_bound (y, α) ?C"
          using absent_var_is_not_bound by blast+
        moreover have "¬ is_bound (𝔣, αβ) ?B" and "¬ is_bound (𝔣, αβ) ?C"
          by code_simp+
        moreover from v  vars ?Ahave "v  {(y, α), (𝔣, αβ)}"
          by auto
        ultimately show "¬ is_bound v ?B  ¬ is_bound v ?C"
          by fast
      qed
      ultimately show ?thesis
        using  ?B =⇘o?C and prop_5204 by presburger
    qed
    then show ?thesis
      by simp
  qed
  ultimately have " 𝔣αβ⇙ =⇘αβ(λyα⇙. 𝔣αβ· yα)"
    using Equality_Rules(1)[unfolded equivalence_def] and Equality_Rules(2) and prop_5200
    by (metis wffs_of_type_intros(1))
  }
  note x_neq_y = this
  then have "§6": " 𝔣αβ⇙ =⇘αβλ𝔶α⇙. 𝔣αβ· 𝔶α⇙" (is " ?B =⇘_?C")
    by simp
  then have "§7": " (λ𝔵α⇙. 𝔣αβ· 𝔵α) =⇘αβ(λ𝔶α⇙. (λ𝔵α⇙. 𝔣αβ· 𝔵α) · 𝔶α)"
  proof -
    let ?A = "λ𝔵α⇙. 𝔣αβ· 𝔵α⇙"
    have "?A  wffs⇘αβ⇙" and "?B  wffs⇘αβ⇙" and "?C  wffs⇘αβ⇙"
      by auto
    moreover have "v  vars ?A. ¬ is_bound v ?B  ¬ is_bound v ?C"
    proof
      fix v
      assume "v  vars ?A"
      have "¬ is_bound (𝔵, α) ?B" and "¬ is_bound (𝔵, α) ?C"
        by code_simp+
      moreover have "¬ is_bound (𝔣, αβ) ?B" and "¬ is_bound (𝔣, αβ) ?C"
        by code_simp+
      moreover from v  vars ?Ahave "v  {(𝔵, α), (𝔣, αβ)}"
        by auto
      ultimately show "¬ is_bound v ?B  ¬ is_bound v ?C"
        by fast
    qed
    ultimately have " S {(𝔣, αβ)  ?A} (?B =⇘αβ?C)"
      using "§6" and prop_5204 by presburger
    then show ?thesis
      by simp
  qed
  have " (λ𝔵α⇙. 𝔣αβ· 𝔵α) =⇘αβ(λ𝔶α⇙. 𝔣αβ· 𝔶α)"
  proof -
    have " (λ𝔵α⇙. 𝔣αβ· 𝔵α) · 𝔶α⇙ =⇘β𝔣αβ· 𝔶α⇙"
    proof -
      have "𝔶α wffs⇘α⇙" and "𝔣αβ· 𝔵α wffs⇘β⇙"
        by auto
      moreover have "v  vars (𝔶α). ¬ is_bound v (𝔣αβ· 𝔵α)"
        by simp
      moreover have "S {(𝔵, α)  𝔶α} (𝔣αβ· 𝔵α) = 𝔣αβ· 𝔶α⇙"
        by simp
      ultimately show ?thesis
        using prop_5203 by metis
    qed
    from "§7" and this show ?thesis
      by (rule rule_R [where p = "[»,«]"]) force+
  qed
  with "§6" and x_neq_y[of y] show ?thesis
    using Equality_Rules(2,3) by blast
qed

subsection ‹Proposition 5206 ($\alpha$-conversion)›

proposition prop_5206:
  assumes "A  wffs⇘α⇙"
  and "(z, β)  free_vars A"
  and "is_free_for (zβ) (x, β) A"
  shows " (λxβ⇙. A) =⇘βα(λzβ⇙. S {(x, β)  zβ} A)"
proof -
  have "is_substitution {(x, β)  zβ}"
    by auto
  from this and assms(1) have "S {(x, β)  zβ} A  wffs⇘α⇙"
    by (fact substitution_preserves_typing)
  obtain y where "(y, β)  {(x, β), (z, β)}  vars A"
  proof -
    have "finite ({(x, β), (z, β)}  vars A)"
      using vars_form_finiteness by blast
    with that show ?thesis
      using fresh_var_existence by metis
  qed
  then have "(y, β)  (x, β)" and "(y, β)  (z, β)" and "(y, β)  vars A" and "(y, β)  free_vars A"
    using free_vars_in_all_vars by auto
  have "§1": " (λxβ⇙. A) =⇘βα(λyβ⇙. (λxβ⇙. A) · yβ)"
  proof -
    let ?A = "λxβ⇙. A"
    have *: " 𝔣βα⇙ =⇘βα(λyβ⇙. 𝔣βα· yβ)" (is " ?B =⇘_?C")
      by (fact prop_5205)
    moreover have " S {(𝔣, βα)  ?A} (?B =⇘βα?C)"
    proof -
      from assms(1) have "?A  wffs⇘βα⇙" and "?B  wffs⇘βα⇙" and "?C  wffs⇘βα⇙"
        by auto
      moreover have "v  vars ?A. ¬ is_bound v ?B  ¬ is_bound v ?C"
      proof
        fix v
        assume "v  vars ?A"
        then consider (a) "v = (x, β)" | (b) "v  vars A"
          by fastforce
        then show "¬ is_bound v ?B  ¬ is_bound v ?C"
        proof cases
          case a
          then show ?thesis
            using (y, β)  (x, β) by force
        next
          case b
          then have "¬ is_bound v ?B"
            by simp
          moreover have "¬ is_bound v ?C"
            using b and (y, β)  vars A by code_simp force
          ultimately show ?thesis
            by blast
        qed
      qed
      ultimately show ?thesis
        using prop_5204 and * by presburger
    qed
    ultimately show ?thesis
      by simp
  qed
  then have "§2": " (λxβ⇙. A) =⇘βα(λyβ⇙. S {(x, β)  yβ} A)"
  proof -
    have " (λxβ⇙. A) · yβ⇙ =⇘αS {(x, β)  yβ} A" (is " (λxβ⇙. ?B) · ?A =⇘__")
    proof -
      have "?A  wffs⇘β⇙" and "?B  wffs⇘α⇙"
        by blast fact
      moreover have "v  vars ?A. ¬ is_bound v ?B"
        using (y, β)  vars A and absent_var_is_not_bound by auto
      ultimately show ?thesis
        by (fact prop_5203)
    qed
    with "§1" show ?thesis
      by (rule rule_R [where p = "[»,«]"]) force+
  qed
  moreover
  have "§3": " (λzβ⇙. S {(x, β)  zβ} A) =⇘βα(λyβ⇙. (λzβ⇙. S {(x, β)  zβ} A) · yβ)"
  proof -
    let ?A = "λzβ⇙. S {(x, β)  zβ} A"
    have *: " 𝔣βα⇙ =⇘βα(λyβ⇙. 𝔣βα· yβ)" (is " ?B =⇘_?C")
      by (fact prop_5205)
    moreover have " S {(𝔣, βα)  ?A} (?B =⇘βα?C)"
    proof -
      have "?A  wffs⇘βα⇙" and "?B  wffs⇘βα⇙" and "?C  wffs⇘βα⇙"
        using S {(x, β)  zβ} A  wffs⇘α⇙› by auto
      moreover have "v  vars ?A. ¬ is_bound v ?B  ¬ is_bound v ?C"
      proof
        fix v
        assume "v  vars ?A"
        then consider (a) "v = (z, β)" | (b) "v  vars (S {(x, β)  zβ} A)"
          by fastforce
        then show "¬ is_bound v ?B  ¬ is_bound v ?C"
        proof cases
          case a
          then show ?thesis
            using (y, β)  (z, β) by auto
        next
          case b
          then have "¬ is_bound v ?B"
            by simp
          moreover from b and (y, β)  vars A and (y, β)  (z, β) have "v  (y, β)"
            using renaming_substitution_minimal_change by blast
          then have "¬ is_bound v ?C"
            by code_simp simp
          ultimately show ?thesis
            by blast
        qed
      qed
      ultimately show ?thesis
        using prop_5204 and * by presburger
    qed
    ultimately show ?thesis
      by simp
  qed
  then have "§4": " (λzβ⇙. S {(x, β)  zβ} A) =⇘βα(λyβ⇙. S {(x, β)  yβ} A)"
  proof -
    have " (λzβ⇙. S {(x, β)  zβ} A) · yβ⇙ =⇘αS {(x, β)  yβ} A" (is " (λzβ⇙. ?B) · ?A =⇘__")
    proof -
      have "?A  wffs⇘β⇙" and "?B  wffs⇘α⇙"
        by blast fact
      moreover from (y, β)  vars A and (y, β)  (z, β) have "v  vars ?A. ¬ is_bound v ?B"
        using absent_var_is_not_bound and renaming_substitution_minimal_change by auto
      ultimately have " (λzβ⇙. S {(x, β)  zβ} A) · yβ⇙ =⇘αS {(z, β)  yβ} S {(x, β)  zβ} A"
        using prop_5203 by fast
      moreover have "S {(z, β)  yβ} S {(x, β)  zβ} A = S {(x, β)  yβ} A"
        by (fact renaming_substitution_composability[OF assms(2,3)])
      ultimately show ?thesis
        by (simp only:)
    qed
    with "§3" show ?thesis
      by (rule rule_R [where p = "[»,«]"]) auto
  qed
  ultimately show ?thesis
    using Equality_Rules(2,3) by blast
qed

lemmas "α" = prop_5206 (* synonym *)

subsection ‹Proposition 5207 ($\beta$-conversion)›

context
begin

private lemma bound_var_renaming_equality:
  assumes "A  wffs⇘α⇙"
  and "zγ yγ⇙"
  and "(z, γ)  vars A"
  shows " A =⇘αrename_bound_var (y, γ) z A"
using assms proof induction
  case (var_is_wff α x)
  then show ?case
    using prop_5200 by force
next
  case (con_is_wff α c)
  then show ?case
    using prop_5200 by force
next
  case (app_is_wff α β A B)
  then show ?case
    using Equality_Rules(4) by auto
next
  case (abs_is_wff β A α x)
  then show ?case
  proof (cases "(y, γ) = (x, α)")
    case True
    have " λyγ⇙. A =⇘γβλyγ⇙. A"
      by (fact abs_is_wff.hyps[THEN prop_5200[OF wffs_of_type_intros(4)]])
    moreover have " A =⇘βrename_bound_var (y, γ) z A"
      using abs_is_wff.IH[OF assms(2)] and abs_is_wff.prems(2) by fastforce
    ultimately have " λyγ⇙. A =⇘γβλyγ⇙. rename_bound_var (y, γ) z A"
      by (rule rule_R[where p = "[»,«]"]) force+
    moreover
    have "
       λyγ⇙. rename_bound_var (y, γ) z A
        =⇘γβλzγ⇙. S {(y, γ)  zγ} (rename_bound_var (y, γ) z A)"
    proof -
      have "rename_bound_var (y, γ) z A  wffs⇘β⇙"
        using hyp_derivable_form_is_wffso[OF  A =⇘βrename_bound_var (y, γ) z A]
        by (blast dest: wffs_from_equality)
      moreover from abs_is_wff.prems(2) have "(z, γ)  free_vars (rename_bound_var (y, γ) z A)"
        using rename_bound_var_free_vars[OF abs_is_wff.hyps assms(2)] by simp
      moreover from abs_is_wff.prems(2) have "is_free_for (zγ) (y, γ) (rename_bound_var (y, γ) z A)"
        using is_free_for_in_rename_bound_var[OF abs_is_wff.hyps assms(2)] by simp
      ultimately show ?thesis
        using "α" by fast
    qed
    ultimately have " λyγ⇙. A =⇘γβλzγ⇙. S {(y, γ)  zγ} (rename_bound_var (y, γ) z A)"
      by (rule Equality_Rules(3))
    then show ?thesis
      using True by auto
  next
    case False
    have " λxα⇙. A =⇘αβλxα⇙. A"
      by (fact abs_is_wff.hyps[THEN prop_5200[OF wffs_of_type_intros(4)]])
    moreover have " A =⇘βrename_bound_var (y, γ) z A"
      using abs_is_wff.IH[OF assms(2)] and abs_is_wff.prems(2) by fastforce
    ultimately have " λxα⇙. A =⇘αβλxα⇙. rename_bound_var (y, γ) z A"
      by (rule rule_R[where p = "[»,«]"]) force+
    then show ?thesis
      using False by auto
  qed
qed

proposition prop_5207:
  assumes "A  wffs⇘α⇙" and "B  wffs⇘β⇙"
  and "is_free_for A (x, α) B"
  shows " (λxα⇙. B) · A =⇘βS {(x, α)  A} B"
using assms proof (induction "form_size B" arbitrary: B β rule: less_induct)
  case less
  from less(3,1,2,4) show ?case
  proof (cases B rule: wffs_of_type_cases)
    case (var_is_wff y)
    then show ?thesis
    proof (cases "yβ= xα⇙")
      case True
      then have "α = β"
        by simp
      moreover from assms(1) have " (λxα⇙. xα) · A =⇘αA"
        using axiom_4_2 by (intro axiom_is_derivable_from_no_hyps)
      moreover have "S {(x, α)  A} (xα) = A"
        by force
      ultimately show ?thesis
        unfolding True and var_is_wff by simp
    next
      case False
      with assms(1) have " (λxα⇙. yβ) · A =⇘βyβ⇙"
        using axiom_4_1_var by (intro axiom_is_derivable_from_no_hyps)
      moreover from False have "S {(x, α)  A} (yβ) = yβ⇙"
        by auto
      ultimately show ?thesis
        unfolding False and var_is_wff by simp
    qed
  next
    case (con_is_wff c)
     from assms(1) have " (λxα⇙. c⦄⇘β) · A =⇘βc⦄⇘β⇙"
      using axiom_4_1_con by (intro axiom_is_derivable_from_no_hyps)
    moreover have "S {(x, α)  A} (c⦄⇘β) = c⦄⇘β⇙"
      by auto
    ultimately show ?thesis
      by (simp only: con_is_wff)
  next
    case (app_is_wff γ D C)
    have "form_size D < form_size B" and "form_size C < form_size B"
      unfolding app_is_wff(1) by simp_all
    from less(4)[unfolded app_is_wff(1)] have "is_free_for A (x, α) D" and "is_free_for A (x, α) C"
      using is_free_for_from_app by iprover+
    from is_free_for A (x, α) D have " (λxα⇙. D) · A =⇘γβS {(x, α)  A} D"
      by (fact less(1)[OF form_size D < form_size B assms(1) app_is_wff(2)])
    moreover from is_free_for A (x, α) C have " (λxα⇙. C) · A =⇘γS {(x, α)  A} C"
      by (fact less(1)[OF form_size C < form_size B assms(1) app_is_wff(3)])
    moreover have " (λxα⇙. D · C) · A =⇘β((λxα⇙. D) · A) · ((λxα⇙. C) · A)"
      by (fact axiom_4_3[OF assms(1) app_is_wff(2,3), THEN axiom_is_derivable_from_no_hyps])
    ultimately show ?thesis
      unfolding app_is_wff(1) using Equality_Rules(3,4) and substitute.simps(3) by presburger
  next
    case (abs_is_wff δ D γ y)
    then show ?thesis
    proof (cases "yγ= xα⇙")
      case True
      with abs_is_wff(1) have " (λxα⇙. λyγ⇙. D) · A =⇘βλyγ⇙. D"
        using axiom_4_5[OF assms(1) abs_is_wff(3)] by (simp add: axiom_is_derivable_from_no_hyps)
      moreover have "S {(x, α)  A} (λyγ⇙. D) = λyγ⇙. D"
        using True by (simp add: empty_substitution_neutrality fmdrop_fmupd_same)
      ultimately show ?thesis
        unfolding abs_is_wff(2) by (simp only:)
    next
      case False
      have "form_size D < form_size B"
        unfolding abs_is_wff(2) by simp
      have "is_free_for A (x, α) D"
        using is_free_for_from_abs[OF less(4)[unfolded abs_is_wff(2)]] and yγ xα⇙› by blast
      have " (λxα⇙. (λyγ⇙. D)) · A =⇘βλyγ⇙. S {(x, α)  A} D"
      proof (cases "(y, γ)  vars A")
        case True
        with yγ xα⇙› have " (λxα⇙. λyγ⇙. D) · A =⇘γδλyγ⇙. (λxα⇙. D) · A"
          using axiom_4_4[OF assms(1) abs_is_wff(3)] and axiom_is_derivable_from_no_hyps by auto
        moreover have " (λxα⇙. D) · A =⇘δS {(x, α)  A} D"
          by
            (
              fact less(1)
                [OF form_size D < form_size B assms(1) D  wffs⇘δ⇙› is_free_for A (x, α) D]
            )
        ultimately show ?thesis
          unfolding abs_is_wff(1) by (rule rule_R[where p = "[»,«]"]) force+
      next
        case False
        have "finite (vars {A, D})"
          using vars_form_finiteness and vars_form_set_finiteness by simp
        then obtain z where "(z, γ)  ({(x, α), (y, γ)}  vars {A, D})"
          using fresh_var_existence by (metis Un_insert_left finite.simps insert_is_Un)
        then have "zγ xα⇙" and "zγ yγ⇙" and "(z, γ)  vars {A, D}"
          by simp_all
        then show ?thesis
        proof (cases "(x, α)  free_vars D")
          case True
          define D' where "D' = S {(y, γ)  zγ} D"
          have "is_substitution {(y, γ)  zγ}"
            by auto
          with D  wffs⇘δ⇙› and D'_def have "D'  wffs⇘δ⇙"
            using substitution_preserves_typing by blast
          then have " (λxα⇙. λzγ⇙. D') · A =⇘γδλzγ⇙. (λxα⇙. D') · A"
            using zγ xα⇙› and (z, γ)  vars {A, D} and axiom_4_4[OF assms(1)]
            and axiom_is_derivable_from_no_hyps
            by auto
          moreover have "§2": " (λxα⇙. D') · A =⇘δD'"
          proof -
            have "form_size D' = form_size D"
              unfolding D'_def by (fact renaming_substitution_preserves_form_size)
            then have "form_size D' < form_size B"
              using form_size D < form_size B by simp
            moreover from zγ xα⇙› have "is_free_for A (x, α) D'"
              unfolding D'_def and is_free_for_def
              using substitution_preserves_freeness[OF True] and is_free_at_in_free_vars
              by fast
            ultimately have " (λxα⇙. D') · A =⇘δS {(x, α)  A} D'"
              using less(1) and assms(1) and D'  wffs⇘δ⇙› by simp
            moreover from zγ xα⇙› have "(x, α)  free_vars D'"
              unfolding D'_def using substitution_preserves_freeness[OF True] by fast
            then have "S {(x, α)  A} D' = D'"
              by (fact free_var_singleton_substitution_neutrality)
            ultimately show ?thesis
              by (simp only:)
          qed
          ultimately have "§3": " (λxα⇙. λzγ⇙. D') · A =⇘γδλzγ⇙. D'" (is  ?A3)
            by (rule rule_R[where p = "[»,«]"]) force+
          moreover have "§4": " (λyγ⇙. D) =⇘γδλzγ⇙. D'"
          proof -
            have "(z, γ)  free_vars D"
              using (z, γ)  vars {A, D} and free_vars_in_all_vars_set by auto
            moreover have "is_free_for (zγ) (y, γ) D"
              using (z, γ)  vars {A, D} and absent_var_is_free_for by force
            ultimately have " λyγ⇙. D =⇘γδλzγ⇙. S {(y, γ)  zγ} D"
              using "α"[OF D  wffs⇘δ⇙›] by fast
            then show ?thesis
              using D'_def by blast
          qed
          ultimately have "§5": " (λxα⇙. λyγ⇙. D) · A =⇘γδλyγ⇙. D"
          proof -
            note rule_RR' = rule_RR[OF disjI2]
            have "§51": " (λxα⇙. λyγ⇙. D) · A =⇘γδλzγ⇙. D'" (is  ?A51)
              by (rule rule_RR'[OF "§4", where p = "[«,»,«,«]" and C = "?A3"]) (use "§3" in force+)
            show ?thesis
              by (rule rule_RR'[OF "§4", where p = "[»]" and C = "?A51"]) (use "§51" in force+)
          qed
          then show ?thesis
            using free_var_singleton_substitution_neutrality[OF (x, α)  free_vars D]
            by (simp only: β = γδ)
        next
          case False
          have "(y, γ)  free_vars A"
          proof (rule ccontr)
            assume "¬ (y, γ)  free_vars A"
            moreover from ¬ (x, α)  free_vars D obtain p
              where "p  positions D" and "is_free_at (x, α) p D"
              using free_vars_in_is_free_at by blast
            then have "« # p  positions (λyγ⇙. D)" and "is_free_at (x, α) (« # p) (λyγ⇙. D)"
              using is_free_at_to_abs[OF is_free_at (x, α) p D] and yγ xα⇙› by (simp, fast)
            moreover have "in_scope_of_abs (y, γ) (« # p) (λyγ⇙. D)"
              by force
            ultimately have "¬ is_free_for A (x, α) (λyγ⇙. D)"
              by blast
            with is_free_for A (x, α) B[unfolded abs_is_wff(2)] show False
              by contradiction
          qed
          define A' where "A' = rename_bound_var (y, γ) z A"
          have "A'  wffs⇘α⇙"
            unfolding A'_def by (fact rename_bound_var_preserves_typing[OF assms(1)])
          from (z, γ)  vars {A, D} have "(y, γ)  vars A'"
            using
              old_var_not_free_not_occurring_after_rename
              [
                OF assms(1) zγ yγ⇙› (y, γ)  free_vars A
              ]
            unfolding A'_def by simp
          from A'_def have "§6": " A =⇘αA'"
            using bound_var_renaming_equality[OF assms(1) zγ yγ⇙›] and (z, γ)  vars {A, D}
            by simp
          moreover have "§7": " (λxα⇙. λyγ⇙. D) · A' =⇘γδλyγ⇙. (λxα⇙. D) · A'" (is  ?A7)
            using axiom_4_4[OF A'  wffs⇘α⇙› D  wffs⇘δ⇙›]
            and (y, γ)  vars A' and yγ xα⇙› and axiom_is_derivable_from_no_hyps
            by auto
          ultimately have "§8": " (λxα⇙. λyγ⇙. D) · A =⇘γδλyγ⇙. (λxα⇙. D) · A"
          proof -
            note rule_RR' = rule_RR[OF disjI2]
            have "§81": " (λxα⇙. λyγ⇙. D) · A =⇘γδλyγ⇙. (λxα⇙. D) · A'" (is  ?A81)
              by (rule rule_RR'[OF "§6", where p = "[«,»,»]" and C = "?A7"]) (use "§7" in force+)
            show ?thesis
              by (rule rule_RR'[OF "§6", where p = "[»,«,»]" and C = "?A81"]) (use "§81" in force+)
          qed
          moreover have "form_size D < form_size B"
            unfolding abs_is_wff(2) by (simp only: form_size.simps(4) lessI)
          with assms(1) have "§9": " (λxα⇙. D) · A =⇘δS {(x, α)  A} D"
            using less(1) and D  wffs⇘δ⇙› and is_free_for A (x, α) D by (simp only:)
          ultimately show ?thesis
            unfolding β = γδ by (rule rule_R[where p = "[»,«]"]) force+
        qed
      qed
      then show ?thesis
        unfolding abs_is_wff(2) using False and singleton_substitution_simps(4) by simp
    qed
  qed
qed

end

subsection ‹Proposition 5208›

proposition prop_5208:
  assumes "vs  []" and "B  wffs⇘β⇙"
  shows " ·𝒬 (λ𝒬 vs B) (map FVar vs) =⇘βB"
using assms(1) proof (induction vs rule: list_nonempty_induct)
  case (single v)
  obtain x and α where "v = (x, α)"
    by fastforce
  then have "·𝒬 (λ𝒬 [v] B) (map FVar [v]) = (λxα⇙. B) · xα⇙"
    by simp
  moreover have " (λxα⇙. B) · xα⇙ =⇘βB"
  proof -
    have "is_free_for (xα) (x, α) B"
      by fastforce
    then have " (λxα⇙. B) · xα⇙ =⇘βS {(x, α)  xα} B"
      by (rule prop_5207 [OF wffs_of_type_intros(1) assms(2)])
    then show ?thesis
      using identity_singleton_substitution_neutrality by (simp only:)
  qed
  ultimately show ?case
    by (simp only:)
next
  case (cons v vs)
  obtain x and α where "v = (x, α)"
    by fastforce
  have " ·𝒬 (λ𝒬 (v # vs) B) (map FVar (v # vs)) =⇘β·𝒬 (λ𝒬 vs B) (map FVar vs)"
  proof -
    have "·𝒬 (λ𝒬 (v # vs) B) (map FVar (v # vs))  wffs⇘β⇙"
    proof -
      have "λ𝒬 (v # vs) B  wffs⇘foldr (→) (map snd (v # vs)) β⇙"
        using generalized_abs_wff [OF assms(2)] by blast
      moreover
      have "k < length (map FVar (v # vs)). map FVar (v # vs) ! k  wffs⇘map snd (v # vs) ! k⇙"
      proof safe
        fix k
        assume *: "k < length (map FVar (v # vs))"
        moreover obtain x and α where "(v # vs) ! k = (x, α)"
          by fastforce
        with * have "map FVar (v # vs) ! k = xα⇙" and "map snd (v # vs) ! k = α"
          by (metis length_map nth_map snd_conv)+
        ultimately show "map FVar (v # vs) ! k  wffs⇘map snd (v # vs) ! k⇙"
          by fastforce
      qed
      ultimately show ?thesis
        using generalized_app_wff[where As = "map FVar (v # vs)" and ts = "map snd (v # vs)"] by simp
    qed
    then have "
       ·𝒬 (λ𝒬 (v # vs) B) (map FVar (v # vs)) =⇘β·𝒬 (λ𝒬 (v # vs) B) (map FVar (v # vs))"
      by (fact prop_5200)
    then have "
       ·𝒬 (λ𝒬 (v # vs) B) (map FVar (v # vs)) =⇘β·𝒬 ((λ𝒬 (v # vs) B) · FVar v) (map FVar vs)"
      by simp
    moreover have " (λ𝒬 (v # vs) B) · FVar v =⇘foldr (→) (map snd vs) β(λ𝒬 vs B)"
    proof -
      have " (λ𝒬 (v # vs) B) · FVar v =⇘foldr (→) (map snd vs) βS {v  FVar v} (λ𝒬 vs B)"
      proof -
        from v = (x, α) have "λ𝒬 (v # vs) B = λxα⇙. λ𝒬 vs B"
          by simp
        have "λ𝒬 vs B  wffs⇘foldr (→) (map snd vs) β⇙"
          using generalized_abs_wff[OF assms(2)] by blast
        moreover have "is_free_for (xα) (x, α) (λ𝒬 vs B)"
          by fastforce
        ultimately
        have " (λxα⇙. λ𝒬 vs B) · xα⇙ =⇘foldr (→) (map snd vs) βS {(x, α)  xα} λ𝒬 vs B"
          by (rule prop_5207 [OF wffs_of_type_intros(1)])
        with v = (x, α) show ?thesis
          by simp
      qed
    then show ?thesis
      using identity_singleton_substitution_neutrality by (simp only:)
    qed
    ultimately show ?thesis
    proof (induction rule: rule_R [where p = "[»] @ replicate (length vs) «"])
      case occ_subform
      then show ?case
        unfolding equality_of_type_def using leftmost_subform_in_generalized_app
        by (metis append_Cons append_Nil is_subform_at.simps(3) length_map)
    next
      case replacement
      then show ?case
        unfolding equality_of_type_def using leftmost_subform_in_generalized_app_replacement
        and is_subform_implies_in_positions and leftmost_subform_in_generalized_app
        by (metis append_Cons append_Nil length_map replace_right_app)
    qed
  qed
  moreover have " ·𝒬 (λ𝒬 vs B) (map FVar vs) =⇘βB"
    by (fact cons.IH)
  ultimately show ?case
    by (rule rule_R [where p = "[»]"]) auto
qed

subsection ‹Proposition 5209›

proposition prop_5209:
  assumes "A  wffs⇘α⇙" and "B  wffs⇘β⇙" and "C  wffs⇘β⇙"
  and " B =⇘βC"
  and "is_free_for A (x, α) (B =⇘βC)"
  shows " S {(x, α)  A} (B =⇘βC)"
proof -
  have " (λxα⇙. B) · A =⇘β(λxα⇙. B) · A"
  proof -
    have "(λxα⇙. B) · A  wffs⇘β⇙"
      using assms(1,2) by blast
    then show ?thesis
      by (fact prop_5200)
  qed
  from this and assms(4) have " (λxα⇙. B) · A =⇘β(λxα⇙. C) · A"
    by (rule rule_R [where p = "[»,«,«]"]) force+
  moreover have " (λxα⇙. B) · A =⇘βS {(x, α)  A} B"
  proof -
    from assms(5)[unfolded equality_of_type_def] have "is_free_for A (x, α) (Q⇘β· B)"
      by (rule is_free_for_from_app)
    then have "is_free_for A (x, α) B"
      by (rule is_free_for_from_app)
    with assms(1,2) show ?thesis
      by (rule prop_5207)
  qed
  moreover have " (λxα⇙. C) · A =⇘βS {(x, α)  A} C"
  proof -
    from assms(5)[unfolded equality_of_type_def] have "is_free_for A (x, α) C"
      by (rule is_free_for_from_app)
    with assms(1,3) show ?thesis
      by (rule prop_5207)
  qed
  ultimately have " (S {(x, α)  A} B) =⇘β(S {(x, α)  A} C)"
    using Equality_Rules(2,3) by blast
  then show ?thesis
    by simp
qed

subsection ‹Proposition 5210›

proposition prop_5210:
  assumes "B  wffs⇘β⇙"
  shows " T⇘o⇙ =⇘o(B =⇘βB)"
proof -
  have "§1": "
    
      ((λ𝔶β⇙. 𝔶β) =⇘ββ(λ𝔶β⇙. 𝔶β))
      =⇘o𝔵β⇙. ((λ𝔶β⇙. 𝔶β) · 𝔵β⇙ =⇘β(λ𝔶β⇙. 𝔶β) · 𝔵β)"
  proof -
    have " (𝔣ββ⇙ =⇘ββ𝔤ββ) =⇘o𝔵β⇙. (𝔣ββ· 𝔵β⇙ =⇘β𝔤ββ· 𝔵β)" (is " ?B =⇘o?C")
      using axiom_3[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
    moreover have "(λ𝔶β⇙. 𝔶β)  wffs⇘ββ⇙" and "?B  wffs⇘o⇙" and "?C  wffs⇘o⇙"
      by auto
    moreover have "is_free_for (λ𝔶β⇙. 𝔶β) (𝔣, ββ) (?B =⇘o?C)"
      by simp
    ultimately have " S {(𝔣, ββ)  (λ𝔶β⇙. 𝔶β)} (?B =⇘o?C)" (is " ?S")
      using prop_5209 by presburger
    moreover have "?S =
      (
        (λ𝔶β⇙. 𝔶β) =⇘ββ𝔤ββ) =⇘o𝔵β⇙. ((λ𝔶β⇙. 𝔶β) · 𝔵β⇙ =⇘β𝔤ββ· 𝔵β)" (is "_ = ?B' =⇘o?C'")
      by simp
    ultimately have " ?B' =⇘o?C'"
      by (simp only:)
    moreover from (λ𝔶β⇙. 𝔶β)  wffs⇘ββ⇙› have "?B'  wffs⇘o⇙" and "?C'  wffs⇘o⇙"
      by auto
    moreover have "is_free_for (λ𝔶β⇙. 𝔶β) (𝔤, ββ) (?B' =⇘o?C')"
      by simp
    ultimately have " S {(𝔤, ββ)  (λ𝔶β⇙. 𝔶β)} (?B' =⇘o?C')" (is " ?S'")
      using prop_5209[OF (λ𝔶β⇙. 𝔶β)  wffs⇘ββ⇙›] by blast
    then show ?thesis
      by simp
  qed
  then have " (λ𝔵β⇙. T⇘o⇙) =⇘βo(λ𝔵β⇙. (𝔵β⇙ =⇘β𝔵β))"
  proof -
    have "λ𝔶β⇙. 𝔶β wffs⇘ββ⇙"
      by blast
    then have " λ𝔶β⇙. 𝔶β⇙ =⇘ββλ𝔶β⇙. 𝔶β⇙"
      by (fact prop_5200)
    with "§1" have " 𝔵β⇙. ((λ𝔶β⇙. 𝔶β) · 𝔵β⇙ =⇘β(λ𝔶β⇙. 𝔶β) · 𝔵β)"
      using rule_R and is_subform_at.simps(1) by blast
    moreover have " (λ𝔶β⇙. 𝔶β) · 𝔵β⇙ =⇘β𝔵β⇙"
      using axiom_4_2[OF wffs_of_type_intros(1)] by (rule axiom_is_derivable_from_no_hyps)
    ultimately have " 𝔵β⇙. (𝔵β⇙ =⇘β(λ𝔶β⇙. 𝔶β) · 𝔵β)"
      by (rule rule_R[where p = "[»,«,«,»]"]) auto
    from this and  (λ𝔶β⇙. 𝔶β) · 𝔵β⇙ =⇘β𝔵β⇙› have " 𝔵β⇙. (𝔵β⇙ =⇘β𝔵β)"
      by (rule rule_R[where p = "[»,«,»]"]) auto
    then show ?thesis
      unfolding forall_def and PI_def by (fold equality_of_type_def)
  qed
  from this and assms have 3: " (λ𝔵β⇙. T⇘o⇙) · B =⇘o(λ𝔵β⇙. (𝔵β⇙ =⇘β𝔵β)) · B"
    by (rule Equality_Rules(5))
  then show ?thesis
  proof -
    have " (λ𝔵β⇙. T⇘o⇙) · B =⇘o⇙ T⇘o⇙"
      using prop_5207[OF assms true_wff] by fastforce
    from 3 and this have " T⇘o⇙ =⇘o(λ𝔵β⇙. (𝔵β⇙ =⇘β𝔵β)) · B"
      by (rule rule_R[where p = "[«,»]"]) auto
    moreover have " (λ𝔵β⇙. (𝔵β⇙ =⇘β𝔵β)) · B =⇘o(B =⇘βB)"
    proof -
      have "𝔵β⇙ =⇘β𝔵β wffs⇘o⇙" and "is_free_for B (𝔵, β) (𝔵β⇙ =⇘β𝔵β)"
        by (blast, intro is_free_for_in_equality is_free_for_in_var)
      moreover have "S {(𝔵, β)  B} (𝔵β⇙ =⇘β𝔵β) = (B =⇘βB)"
        by simp
      ultimately show ?thesis
        using prop_5207[OF assms] by metis
    qed
    ultimately show ?thesis
      by (rule rule_R [where p = "[»]"]) auto
  qed
qed

subsection ‹Proposition 5211›

proposition prop_5211:
  shows " (To 𝒬 To) =⇘o⇙ T⇘o⇙"
proof -
  have const_T_wff: "(λxo⇙. T⇘o⇙)  wffs⇘oo⇙" for x
   by blast
  have "§1": " (λ𝔶o⇙. T⇘o⇙) · To 𝒬 (λ𝔶o⇙. T⇘o⇙) · F⇘o⇙ =⇘o𝔵o⇙. (λ𝔶o⇙. T⇘o⇙) · 𝔵o⇙"
  proof -
    have " 𝔤oo· To 𝒬 𝔤oo· F⇘o⇙ =⇘o𝔵o⇙. 𝔤oo· 𝔵o⇙" (is " ?B =⇘o?C")
      using axiom_1[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
    moreover have "?B  wffs⇘o⇙" and "?C  wffs⇘o⇙"
      by auto
    moreover have "is_free_for (λ𝔶o⇙. T⇘o⇙) (𝔤, oo) (?B =⇘o?C)"
      by simp
    ultimately have " S {(𝔤, oo)  (λ𝔶o⇙. T⇘o⇙)} (?B =⇘o?C)"
      using const_T_wff and prop_5209 by presburger
    then show ?thesis
      by simp
  qed
  then have " To 𝒬 T⇘o⇙ =⇘o𝔵o⇙. T⇘o⇙"
  proof -
    have T_β_redex: " (λ𝔶o⇙. T⇘o⇙) · A =⇘o⇙ T⇘o⇙" if "A  wffs⇘o⇙" for A
      using that and prop_5207[OF that true_wff] by fastforce
    from "§1" and T_β_redex[OF true_wff]
    have " To 𝒬 (λ𝔶o⇙. T⇘o⇙) · F⇘o⇙ =⇘o𝔵o⇙. (λ𝔶o⇙. T⇘o⇙) · 𝔵o⇙"
      by (rule rule_R[where p = "[«,»,«,»]"]) force+
    from this and T_β_redex[OF false_wff] have " To 𝒬 T⇘o⇙ =⇘o𝔵o⇙. (λ𝔶o⇙. T⇘o⇙) · 𝔵o⇙"
      by (rule rule_R[where p = "[«,»,»]"]) force+
    from this and T_β_redex[OF wffs_of_type_intros(1)] show ?thesis
      by (rule rule_R[where p = "[»,»,«]"]) force+
  qed
  moreover have " T⇘o⇙ =⇘o𝔵o⇙. T⇘o⇙"
    using prop_5210[OF const_T_wff] by simp
  ultimately show ?thesis
    using Equality_Rules(2,3) by blast
qed

lemma true_is_derivable:
  shows " To"
  unfolding true_def using Q_wff by (rule prop_5200)

subsection ‹Proposition 5212›

proposition prop_5212:
  shows " To 𝒬 To"
proof -
  have " To"
    by (fact true_is_derivable)
  moreover have " (To 𝒬 To) =⇘o⇙ T⇘o⇙"
    by (fact prop_5211)
  then have " To 𝒬 (To 𝒬 To)"
    unfolding equivalence_def by (fact Equality_Rules(2))
  ultimately show ?thesis
    by (rule Equality_Rules(1))
qed

subsection ‹Proposition 5213›

proposition prop_5213:
  assumes " A =⇘αB" and " C =⇘βD"
  shows " (A =⇘αB) 𝒬 (C =⇘βD)"
proof -
  from assms have "A  wffs⇘α⇙" and "C  wffs⇘β⇙"
    using hyp_derivable_form_is_wffso and wffs_from_equality by blast+
  have " T⇘o⇙ =⇘o(A =⇘αA)"
    by (fact prop_5210[OF A  wffs⇘α⇙›])
  moreover have " A =⇘αB"
    by fact
  ultimately have " T⇘o⇙ =⇘o(A =⇘αB)"
    by (rule rule_R[where p = "[»,»]"]) force+
  have " T⇘o⇙ =⇘o(C =⇘βC)"
    by (fact prop_5210[OF C  wffs⇘β⇙›])
  moreover have " C =⇘βD"
    by fact
  ultimately have " T⇘o⇙ =⇘o(C =⇘βD)"
    by (rule rule_R[where p = "[»,»]"]) force+
  then show ?thesis
  proof -
    have " To 𝒬 To"
      by (fact prop_5212)
    from this and  T⇘o⇙ =⇘o(A =⇘αB) have " (A =⇘αB) 𝒬 To"
      by (rule rule_R[where p = "[«,»]"]) force+
    from this and  T⇘o⇙ =⇘o(C =⇘βD) show ?thesis
      by (rule rule_R[where p = "[»]"]) force+
  qed
qed

subsection ‹Proposition 5214›

proposition prop_5214:
  shows " To 𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙"
proof -
  have id_on_o_is_wff: "(λ𝔵o⇙. 𝔵o)  wffs⇘oo⇙"
    by blast
  have "§1": " (λ𝔵o⇙. 𝔵o) · To 𝒬 (λ𝔵o⇙. 𝔵o) · F⇘o⇙ =⇘o𝔵o⇙. (λ𝔵o⇙. 𝔵o) · 𝔵o⇙"
  proof -
    have " 𝔤oo· To 𝒬 𝔤oo· F⇘o⇙ =⇘o𝔵o⇙. 𝔤oo· 𝔵o⇙" (is " ?B =⇘o?C")
      using axiom_1[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
    moreover have "?B  wffs⇘o⇙" and "?C  wffs⇘o⇙" and "is_free_for (λ𝔵o⇙. 𝔵o) (𝔤, oo) (?B =⇘o?C)"
      by auto
    ultimately have " S {(𝔤, oo)  (λ𝔵o⇙. 𝔵o)} (?B =⇘o?C)"
      using id_on_o_is_wff and prop_5209 by presburger
    then show ?thesis
      by simp
  qed
  then have " To 𝒬 F⇘o⇙ =⇘o𝔵o⇙. 𝔵o⇙"
  proof -
    have id_β_redex: " (λ𝔵o⇙. 𝔵o) · A =⇘oA" if "A  wffs⇘o⇙" for A
      by (fact axiom_is_derivable_from_no_hyps[OF axiom_4_2[OF that]])
    from "§1" and id_β_redex[OF true_wff]
    have " To 𝒬 (λ𝔵o⇙. 𝔵o) · F⇘o⇙ =⇘o𝔵o⇙. (λ𝔵o⇙. 𝔵o) · 𝔵o⇙"
      by (rule rule_R[where p = "[«,»,«,»]"]) force+
    from this and id_β_redex[OF false_wff] have " To 𝒬 F⇘o⇙ =⇘o𝔵o⇙. (λ𝔵o⇙. 𝔵o) · 𝔵o⇙"
      by (rule rule_R[where p = "[«,»,»]"]) force+
    from this and id_β_redex[OF wffs_of_type_intros(1)] show ?thesis
      by (rule rule_R[where p = "[»,»,«]"]) force+
  qed
  then show ?thesis
    by simp
qed

subsection ‹Proposition 5215 (Universal Instantiation)›

proposition prop_5215:
  assumes "  xα⇙. B" and "A  wffs⇘α⇙"
  and "is_free_for A (x, α) B"
  shows "  S {(x, α)  A} B"
proof -
  from assms(1) have "is_hyps "
    by (blast elim: is_derivable_from_hyps.cases)
  from assms(1) have "  (λ𝔵α⇙. T⇘o⇙) =⇘αo(λxα⇙. B)"
    by simp
  with assms(2) have "  (λ𝔵α⇙. T⇘o⇙) · A =⇘o(λxα⇙. B) · A"
    by (intro Equality_Rules(5))
  then have "  T⇘o⇙ =⇘oS {(x, α)  A} B"
  proof -
    have "  (λ𝔵α⇙. T⇘o⇙) · A =⇘o⇙ T⇘o⇙"
    proof -
      have " (λ𝔵α⇙. T⇘o⇙) · A =⇘o⇙ T⇘o⇙"
        using prop_5207[OF assms(2) true_wff is_free_for_in_true] and derived_substitution_simps(1)
        by (simp only:)
      from this and is_hyps  show ?thesis
        by (rule derivability_implies_hyp_derivability)
    qed
    moreover have "  (λxα⇙. B) · A =⇘oS {(x, α)  A} B"
    proof -
      have "B  wffs⇘o⇙"
        using hyp_derivable_form_is_wffso[OF assms(1)] by (fastforce elim: wffs_from_forall)
      with assms(2,3) have " (λxα⇙. B) · A =⇘oS {(x, α)  A} B"
        using prop_5207 by (simp only:)
      from this and is_hyps  show ?thesis
        by (rule derivability_implies_hyp_derivability)
    qed
    ultimately show ?thesis
      using   (λ𝔵α⇙. T⇘o⇙) · A =⇘o(λxα⇙. B) · A and Equality_Rules(2,3) by meson
  qed
  then show ?thesis
  proof -
    have "  To"
      by (fact derivability_implies_hyp_derivability[OF true_is_derivable is_hyps ])
    from this and   T⇘o⇙ =⇘oS {(x, α)  A} B show ?thesis
      by (rule Equality_Rules(1)[unfolded equivalence_def])
  qed
qed

lemmas "∀I" = prop_5215 (* synonym *)

subsection ‹Proposition 5216›

proposition prop_5216:
  assumes "A  wffs⇘o⇙"
  shows " (To 𝒬 A) =⇘oA"
proof -
  let ?B = "λ𝔵o⇙. (To 𝒬 𝔵o⇙ =⇘o𝔵o)"
  have B_is_wff: "?B  wffs⇘oo⇙"
    by auto
  have "§1": " ?B · To 𝒬 ?B · F⇘o⇙ =⇘o𝔵o⇙. ?B · 𝔵o⇙"
  proof -
    have " 𝔤oo· To 𝒬 𝔤oo· F⇘o⇙ =⇘o𝔵o⇙. 𝔤oo· 𝔵o⇙" (is " ?C =⇘o?D")
      using axiom_1[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
    moreover have "?C  wffs⇘o⇙" and "?D  wffs⇘o⇙" and "is_free_for ?B (𝔤, oo) (?C =⇘o?D)"
      by auto
    ultimately have " S {(𝔤, oo)  ?B} (?C =⇘o?D)"
      using B_is_wff and prop_5209 by presburger
    then show ?thesis
      by simp
  qed
  have *: "is_free_for A (𝔵, o) (To 𝒬 𝔵o⇙ =⇘o𝔵o)" for A
    by (intro is_free_for_in_conj is_free_for_in_equality is_free_for_in_true is_free_for_in_var)
  have " (To 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙) 𝒬 (To 𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙)"
    by (fact prop_5213[OF prop_5211 prop_5214])
  moreover
  have " (To 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙) 𝒬 (To 𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o𝔵o⇙. (To 𝒬 𝔵o⇙ =⇘o𝔵o)"
  proof -
    have B_β_redex: " ?B · A =⇘o(To 𝒬 A =⇘oA)" if "A  wffs⇘o⇙" for A
    proof -
      have "To 𝒬 𝔵o⇙ =⇘o𝔵o wffs⇘o⇙"
        by blast
      moreover have "S {(𝔵, o)  A} (To 𝒬 𝔵o⇙ =⇘o𝔵o) = (To 𝒬 A =⇘oA)"
        by simp
      ultimately show ?thesis
        using * and prop_5207[OF that] by metis
    qed
    from "§1" and B_β_redex[OF true_wff]
    have " (To 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙) 𝒬 ?B · F⇘o⇙ =⇘o𝔵o⇙. ?B · 𝔵o⇙"
      by (rule rule_R[where p = "[«,»,«,»]"]) force+
    from this and B_β_redex[OF false_wff]
    have " (To 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙) 𝒬 (To 𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o𝔵o⇙. ?B · 𝔵o⇙"
      by (rule rule_R[where p = "[«,»,»]"]) force+
    from this and B_β_redex[OF wffs_of_type_intros(1)] show ?thesis
      by (rule rule_R[where p = "[»,»,«]"]) force+
  qed
  ultimately have " 𝔵o⇙. (To 𝒬 𝔵o⇙ =⇘o𝔵o)"
    by (rule rule_R[where p = "[]"]) fastforce+
  show ?thesis
    using "∀I"[OF  𝔵o⇙. (To 𝒬 𝔵o⇙ =⇘o𝔵o) assms *] by simp
qed

subsection ‹Proposition 5217›

proposition prop_5217:
  shows " (T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o⇙ F⇘o⇙"
proof -
  let ?B = "λ𝔵o⇙. (T⇘o⇙ =⇘o𝔵o)"
  have B_is_wff: "?B  wffs⇘oo⇙"
    by auto
  have *: "is_free_for A (𝔵, o) (T⇘o⇙ =⇘o𝔵o)" for A
    by (intro is_free_for_in_equality is_free_for_in_true is_free_for_in_var)
  have "§1": " ?B · To 𝒬 ?B · F⇘o⇙ =⇘o𝔵o⇙. ?B · 𝔵o⇙"
  proof -
    have " 𝔤oo· To 𝒬 𝔤oo· F⇘o⇙ =⇘o𝔵o⇙. 𝔤oo· 𝔵o⇙" (is " ?C =⇘o?D")
      using axiom_1[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
    moreover have "?C  wffs⇘o⇙" and "?D  wffs⇘o⇙" and "is_free_for ?B (𝔤, oo) (?C =⇘o?D)"
      by auto
    ultimately have " S {(𝔤, oo)  ?B} (?C =⇘o?D)"
      using B_is_wff and prop_5209 by presburger
    then show ?thesis
      by simp
  qed
  then have " (T⇘o⇙ =⇘o⇙ T⇘o⇙) 𝒬 (T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o𝔵o⇙. (T⇘o⇙ =⇘o𝔵o)" (is " ?A")
  proof -
    have B_β_redex: " ?B · A =⇘o(T⇘o⇙ =⇘oA)" if "A  wffs⇘o⇙" for A
    proof -
      have "T⇘o⇙ =⇘o𝔵o wffs⇘o⇙"
        by auto
      moreover have "S {(𝔵, o)  A} (T⇘o⇙ =⇘o𝔵o) = (T⇘o⇙ =⇘oA)"
        by simp
      ultimately show ?thesis
        using * and prop_5207[OF that] by metis
    qed
    from "§1" and B_β_redex[OF true_wff] have " (T⇘o⇙ =⇘o⇙ T⇘o⇙) 𝒬 ?B · F⇘o⇙ =⇘o𝔵o⇙. ?B · 𝔵o⇙"
      by (rule rule_R[where p = "[«,»,«,»]"]) force+
    from this and B_β_redex[OF false_wff]
    have " (T⇘o⇙ =⇘o⇙ T⇘o⇙) 𝒬 (T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o𝔵o⇙. ?B · 𝔵o⇙"
      by (rule rule_R[where p = "[«,»,»]"]) force+
    from this and B_β_redex[OF wffs_of_type_intros(1)] show ?thesis
      by (rule rule_R[where p = "[»,»,«]"]) force+
  qed
  from prop_5210[OF true_wff] have " To 𝒬 (T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o𝔵o⇙. (T⇘o⇙ =⇘o𝔵o)"
    by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A]) (force+, fact)
  from this and prop_5216[where A = "T⇘o⇙ =⇘o⇙ F⇘o⇙"]
  have " (T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o𝔵o⇙. (T⇘o⇙ =⇘o𝔵o)"
    by (rule rule_R [where p = "[«,»]"]) force+
  moreover have "§5": "
     ((λ𝔵o⇙. T⇘o⇙) =⇘oo(λ𝔵o⇙. 𝔵o)) =⇘o𝔵o⇙. ((λ𝔵o⇙. T⇘o⇙) · 𝔵o⇙ =⇘o(λ𝔵o⇙. 𝔵o) · 𝔵o)"
  proof -
    have " (𝔣oo⇙ =⇘oo𝔤oo) =⇘o𝔵o⇙. (𝔣oo· 𝔵o⇙ =⇘o𝔤oo· 𝔵o)" (is " ?C =⇘o?D")
      using axiom_3[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
    moreover have "is_free_for ((λ𝔵o⇙. T⇘o⇙)) (𝔣, oo) (?C =⇘o?D)"
      by fastforce
    moreover have "(λ𝔵o⇙. T⇘o⇙)  wffs⇘oo⇙" and "?C  wffs⇘o⇙" and "?D  wffs⇘o⇙"
      by auto
    ultimately have " S {(𝔣, oo)  (λ𝔵o⇙. T⇘o⇙)} (?C =⇘o?D)"
      using prop_5209 by presburger
    then have " ((λ𝔵o⇙. T⇘o⇙) =⇘oo𝔤oo) =⇘o𝔵o⇙. ((λ𝔵o⇙. T⇘o⇙) · 𝔵o⇙ =⇘o𝔤oo· 𝔵o)"
      (is " ?C' =⇘o?D'")
      by simp
    moreover have "is_free_for ((λ𝔵o⇙. 𝔵o)) (𝔤, oo) (?C' =⇘o?D')"
      by fastforce
    moreover have "(λ𝔵o⇙. 𝔵o)  wffs⇘oo⇙" and "?C'  wffs⇘o⇙" and "?D'  wffs⇘o⇙"
      using (λ𝔵o⇙. T⇘o⇙)  wffs⇘oo⇙› by auto
    ultimately have " S {(𝔤, oo)  (λ𝔵o⇙. 𝔵o)} (?C' =⇘o?D')"
      using prop_5209 by presburger
    then show ?thesis
      by simp
  qed
  then have " F⇘o⇙ =⇘o𝔵o⇙. (T⇘o⇙ =⇘o𝔵o)"
  proof -
    have " (λ𝔵o⇙. T⇘o⇙) · 𝔵o⇙ =⇘o⇙ T⇘o⇙"
      using prop_5208[where vs = "[(𝔵, o)]"] and true_wff by simp
    with "§5" have *: "
       ((λ𝔵o⇙. T⇘o⇙) =⇘oo(λ𝔵o⇙. 𝔵o)) =⇘o𝔵o⇙. (T⇘o⇙ =⇘o(λ𝔵o⇙. 𝔵o) · 𝔵o)"
      by (rule rule_R[where p = "[»,»,«,«,»]"]) force+
    have " (λ𝔵o⇙. 𝔵o) · 𝔵o⇙ =⇘o𝔵o⇙"
      using prop_5208[where vs = "[(𝔵, o)]"] by fastforce
    with * have " ((λ𝔵o⇙. T⇘o⇙) =⇘oo(λ𝔵o⇙. 𝔵o)) =⇘o𝔵o⇙. (T⇘o⇙ =⇘o𝔵o)"
      by (rule rule_R[where p = "[»,»,«,»]"]) force+
    then show ?thesis
      by simp
  qed
  ultimately show ?thesis
    using Equality_Rules(2,3) by blast
qed

subsection ‹Proposition 5218›

proposition prop_5218:
  assumes "A  wffs⇘o⇙"
  shows " (T⇘o⇙ =⇘oA) =⇘oA"
proof -
  let ?B = "λ𝔵o⇙. ((T⇘o⇙ =⇘o𝔵o) =⇘o𝔵o)"
  have B_is_wff: "?B  wffs⇘oo⇙"
    by auto
  have "§1": " ?B · To 𝒬 ?B · F⇘o⇙ =⇘o𝔵o⇙. ?B · 𝔵o⇙"
  proof -
    have " 𝔤oo· To 𝒬 𝔤oo· F⇘o⇙ =⇘o𝔵o⇙. 𝔤oo· 𝔵o⇙" (is " ?C =⇘o?D")
      using axiom_1[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
    moreover have "?C  wffs⇘o⇙" and "?D  wffs⇘o⇙" and "is_free_for ?B (𝔤, oo) (?C =⇘o?D)"
      by auto
    ultimately have " S {(𝔤, oo)  ?B} (?C =⇘o?D)"
      using prop_5209[OF B_is_wff] by presburger
    then show ?thesis
      by simp
  qed
  have *: "is_free_for A (𝔵, o) ((T⇘o⇙ =⇘o𝔵o) =⇘o𝔵o)" for A
    by (intro is_free_for_in_equality is_free_for_in_true is_free_for_in_var)
  have "§2": "
    
      ((T⇘o⇙ =⇘o⇙ T⇘o⇙) =⇘o⇙ T⇘o⇙) 𝒬 ((T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o⇙ F⇘o⇙)
      =⇘o𝔵o⇙. ((T⇘o⇙ =⇘o𝔵o) =⇘o𝔵o)"
  proof -
    have B_β_redex: " ?B · A =⇘o((T⇘o⇙ =⇘oA) =⇘oA)" if "A  wffs⇘o⇙" for A
    proof -
      have "(T⇘o⇙ =⇘o𝔵o) =⇘o𝔵o wffs⇘o⇙"
        by auto
      moreover have "S {(𝔵, o)  A} ((T⇘o⇙ =⇘o𝔵o) =⇘o𝔵o) = ((T⇘o⇙ =⇘oA) =⇘oA)"
        by simp
      ultimately show ?thesis
        using * and prop_5207[OF that] by metis
    qed
    from "§1" and B_β_redex[OF true_wff]
    have " ((T⇘o⇙ =⇘o⇙ T⇘o⇙) =⇘o⇙ T⇘o⇙) 𝒬 ?B · F⇘o⇙ =⇘o𝔵o⇙. ?B · 𝔵o⇙"
      by (rule rule_R[where p = "[«,»,«,»]"]) force+
    from this and B_β_redex[OF false_wff]
    have " ((T⇘o⇙ =⇘o⇙ T⇘o⇙) =⇘o⇙ T⇘o⇙) 𝒬 ((T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o⇙ F⇘o⇙) =⇘o𝔵o⇙. ?B · 𝔵o⇙"
      by (rule rule_R[where p = "[«,»,»]"]) force+
    from this and B_β_redex[OF wffs_of_type_intros(1)] show ?thesis
      by (rule rule_R[where p = "[»,»,«]"]) force+
  qed
  have "§3": " (T⇘o⇙ =⇘o⇙ T⇘o⇙) =⇘o⇙ T⇘o⇙"
    by (fact Equality_Rules(2)[OF prop_5210 [OF true_wff]])
  have " ((T⇘o⇙ =⇘o⇙ T⇘o⇙) =⇘o⇙ T⇘o⇙) 𝒬 ((T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o⇙ F⇘o⇙)"
    by (fact prop_5213[OF "§3" prop_5217])
  from this and "§2" have "§4": " 𝔵o⇙. ((T⇘o⇙ =⇘o𝔵o) =⇘o𝔵o)"
    by (rule rule_R[where p = "[]"]) fastforce+
  then show ?thesis
    using "∀I"[OF "§4" assms *] by simp
qed

subsection ‹Proposition 5219 (Rule T)›

proposition prop_5219_1:
  assumes "A  wffs⇘o⇙"
  shows "  A    T⇘o⇙ =⇘oA"
proof safe
  assume "  A"
  then have "is_hyps "
    by (blast dest: is_derivable_from_hyps.cases)
  then have "  (T⇘o⇙ =⇘oA) =⇘oA"
    by (fact derivability_implies_hyp_derivability[OF prop_5218[OF assms]])
  with   A show "  T⇘o⇙ =⇘oA"
    using Equality_Rules(1)[unfolded equivalence_def] and Equality_Rules(2) by blast
next
  assume "  T⇘o⇙ =⇘oA"
  then have "is_hyps "
    by (blast dest: is_derivable_from_hyps.cases)
  then have "  (T⇘o⇙ =⇘oA) =⇘oA"
    by (fact derivability_implies_hyp_derivability[OF prop_5218[OF assms]])
  with   T⇘o⇙ =⇘oA show "  A"
    by (rule Equality_Rules(1)[unfolded equivalence_def])
qed

proposition prop_5219_2:
  assumes "A  wffs⇘o⇙"
  shows "  A    A =⇘o⇙ T⇘o⇙"
  using prop_5219_1[OF assms] and Equality_Rules(2) by blast

lemmas rule_T = prop_5219_1 prop_5219_2

subsection ‹Proposition 5220 (Universal Generalization)›

context
begin

private lemma const_true_α_conversion:
  shows " (λxα⇙. T⇘o⇙) =⇘αo(λzα⇙. T⇘o⇙)"
proof -
  have "(z, α)  free_vars To" and "is_free_for (zα) (x, α) To"
    by auto
  then have " (λxα⇙. T⇘o⇙) =⇘αoλzα⇙. S {(x, α)  zα} To"
    by (rule prop_5206[OF true_wff])
  then show ?thesis
    by simp
qed

proposition prop_5220:
  assumes "  A"
  and "(x, α)  free_vars "
  shows "  xα⇙. A"
proof -
  from   A have "is_hyps "
    by (blast dest: is_derivable_from_hyps.cases)
  have "  A"
    by fact
  then have "§2": "  T⇘o⇙ =⇘oA"
    using rule_T(1)[OF hyp_derivable_form_is_wffso[OF   A]] by simp
  have "§3": "  (λ𝔵α⇙. T⇘o⇙) =⇘αo(λxα⇙. T⇘o⇙)"
    by (fact derivability_implies_hyp_derivability[OF const_true_α_conversion is_hyps ])
  from "§3" and "§2" have "  λ𝔵α⇙. T⇘o⇙ =⇘αoλxα⇙. A"
  proof (induction rule: rule_R'[where p = "[», «]"])
    case no_capture
    have *: "[»,«]  positions (λ𝔵α⇙. T⇘o⇙ =⇘αoλxα⇙. T⇘o⇙)"
      by simp
    show ?case
      unfolding rule_R'_side_condition_def and capture_exposed_vars_at_alt_def[OF *] using assms(2)
      by simp
  qed force+
  then show ?thesis
    unfolding forall_def[unfolded PI_def, folded equality_of_type_def] .
qed

end

lemmas Gen = prop_5220 (* synonym *)

proposition generalized_Gen:
  assumes "  A"
  and "lset vs  free_vars  = {}"
  shows "  𝒬 vs A"
using assms(2) proof (induction vs)
  case Nil
  then show ?case
    using assms(1) by simp
next
  case (Cons v vs)
  obtain x and α where "v = (x, α)"
    by fastforce
  with Cons.prems have "lset vs  free_vars  = {}" and "(x, α)  free_vars "
    by simp_all
  from lset vs  free_vars  = {} have "  𝒬 vs A"
    by (fact Cons.IH)
  with (x, α)  free_vars  and v = (x, α) show ?case
    using Gen by simp
qed

subsection ‹Proposition 5221 (Substitution)›

context
begin

private lemma prop_5221_aux:
  assumes "  B"
  and "(x, α)  free_vars "
  and "is_free_for A (x, α) B"
  and "A  wffs⇘α⇙"
  shows "  S {(x, α)  A} B"
proof -
  have "  B"
    by fact
  from this and assms(2) have "  xα⇙. B"
    by (rule Gen)
  from this and assms(4,3) show ?thesis
    by (rule "∀I")
qed

proposition prop_5221:
  assumes "  B"
  and "is_substitution θ"
  and "v  fmdom' θ. var_name v  free_var_names   is_free_for (θ $$! v) v B"
  and "θ  {$$}"
  shows "  S θ B"
proof -
  obtain xs and As
    where "lset xs = fmdom' θ" ― ‹i.e., $x^1_{\alpha_1},\dots,x^n_{\alpha_n}$›
    and "As = map (($$!) θ) xs" ― ‹i.e., $A^1_{\alpha_1},\dots,A^n_{\alpha_n}$›
    and "length xs = card (fmdom' θ)"
    by (metis distinct_card finite_distinct_list finite_fmdom')
  then have "distinct xs"
    by (simp add: card_distinct)
  from lset xs = fmdom' θ and As = map (($$!) θ) xs have "lset As = fmran' θ"
    by (intro subset_antisym subsetI) (force simp add: fmlookup_dom'_iff fmlookup_ran'_iff)+
  from assms(1) have "finite (var_name ` (vars B  vars (lset As)  vars ))"
    by (cases rule: is_derivable_from_hyps.cases) (simp_all add: finite_Domain vars_form_finiteness)
  then obtain ys ― ‹i.e., $y^1_{\alpha_1},\dots,y^n_{\alpha_n}$›
    where "length ys = length xs"
    and "distinct ys"
    and ys_fresh: "
      (var_name ` lset ys)  (var_name ` (vars B  vars (lset As)  vars   lset xs)) = {}"
    and "map var_type ys = map var_type xs"
    using fresh_var_list_existence by (metis image_Un)
  have "length xs = length As"
    by (simp add: As = map (($$!) θ) xs)
  ― ‹$\mathcal{H}\;\vdash\;\d{\textsf{S}}\;
      ^{x^1_{\alpha_1}\;\dots\;x^k_{\alpha_k} x^{k+1}_{\alpha_{k+1}}\;\dots\;x^n_{\alpha_n}}
      _{A^1_{\alpha_1}\;\dots\;A^k_{\alpha_k} y^{k+1}_{\alpha_{k+1}}\;\dots\;y^n_{\alpha_n}} B$›
  have "  S (fmap_of_list (zip xs (take k As @ drop k (map FVar ys)))) B" if "k  length xs" for k
  using that proof (induction k)
    case 0
    have "  S (fmap_of_list (zip xs (map FVar ys))) B"
      using length ys = length xs
      and length xs = length As
      and (var_name ` lset ys)  (var_name ` (vars B  vars (lset As)  vars   lset xs)) = {}
      and lset xs = fmdom' θ
      and distinct ys
      and assms(3)
      and map var_type ys = map var_type xs
      and distinct xs
      and length xs = card (fmdom' θ)
    proof (induction ys xs As arbitrary: θ rule: list_induct3)
      case Nil
      with assms(1) show ?case
        using empty_substitution_neutrality by auto
    next
      ― ‹In the following:
        \begin{itemize}
        \item $\vartheta =
          \{x^1_{\alpha_1} \rightarrowtail y^1_{\alpha_1},\dots,x^n_{\alpha_n} \rightarrowtail y^n_{\alpha_n}\}$
        \item \emph?$\vartheta =
          \{x^2_{\alpha_2} \rightarrowtail y^2_{\alpha_2},\dots,x^n_{\alpha_n} \rightarrowtail y^n_{\alpha_n}\}$
        \item $v_x = x^1_{\alpha_1}$, and $v_y = y^1_{\alpha_1}$
        \end{itemize}
      ›
      case (Cons vy ys vx xs A' As')
      let  = "fmap_of_list (zip xs (map FVar ys))"
      from Cons.hyps(1) have "lset xs = fmdom' "
        by simp
      from Cons.hyps(1) and Cons.prems(6) have "fmran'  = FVar ` lset ys"
        by force
      have "is_substitution "
      unfolding is_substitution_def proof
        fix v
        assume "v  fmdom' "
        with lset xs = fmdom'  obtain k where "v = xs ! k" and "k < length xs"
          by (metis in_set_conv_nth)
        moreover obtain α where "var_type v = α"
          by blast
        moreover from k < length xs and v = xs ! k have " $$! v = (map FVar ys) ! k"
          using Cons.hyps(1) and Cons.prems(6) by auto
        moreover from this and k < length xs obtain y and β where " $$! v = yβ⇙"
          using Cons.hyps(1) by force
        ultimately have "α = β"
          using Cons.hyps(1) and Cons.prems(5)
          by (metis form.inject(1) list.inject list.simps(9) nth_map snd_conv)
        then show "case v of (x, α)   $$! (x, α)  wffs⇘α⇙"
          using  $$! v = yβ⇙› and var_type v = α by fastforce
      qed
      have "vx  fmdom' "
        using Cons.prems(6) and lset xs = fmdom'  by auto
      obtain x and α where "vx = (x, α)"
        by fastforce
      have "FVar vy  wffs⇘α⇙"
        using Cons.prems(5) and surj_pair[of vy] unfolding vx = (x, α) by fastforce
      have "distinct xs"
        using Cons.prems(6) by fastforce
      moreover have ys_fresh': "
        (var_name ` lset ys)  (var_name ` (vars B  vars (lset As')  vars   lset xs)) = {}"
      proof -
        have "vars (lset (A' # As')) = vars {A'}  vars (lset As')"
          by simp
        moreover have "var_name ` (lset (vx # xs)) = {var_name vx}  var_name ` (lset xs)"
          by simp
        moreover from Cons.prems(1) have "
          var_name ` lset ys
          
          (
            var_name ` (vars B)  var_name ` (vars (lset (A' # As')))  var_name ` (vars )
             var_name ` (lset (vx # xs))
          )
          = {}"
          by (simp add: image_Un)
        ultimately have "
          var_name ` lset ys
          
          (
            var_name ` (vars B)  var_name ` (vars (lset As'))  var_name ` (vars )
             var_name ` (lset (vx # xs))
          )
          = {}"
          by fast
        then show ?thesis
          by (simp add: image_Un)
      qed
      moreover have "distinct ys"
        using Cons.prems(3) by auto
      moreover have "v  fmdom' . var_name v  free_var_names   is_free_for ( $$! v) v B"
      proof
        fix v
        assume "v  fmdom' "
        with Cons.hyps(1) obtain y where " $$! v = FVar y" and "y  lset ys"
          by (metis (mono_tags, lifting) fmap_of_zipped_list_range image_iff length_map list.set_map)
        moreover from Cons.prems(2,4) have "var_name v  free_var_names "
          using lset xs = fmdom'  and v  fmdom'  by auto
        moreover from y  lset ys have "y  vars B"
          using ys_fresh' by blast
        then have "is_free_for (FVar y) v B"
          by (intro absent_var_is_free_for)
        ultimately show "var_name v  free_var_names   is_free_for ( $$! v) v B"
          by simp
      qed
      moreover have "map var_type ys = map var_type xs"
        using Cons.prems(5) by simp
      moreover have "length xs = card (fmdom' )"
        by (fact distinct_card[OF distinct xs, unfolded lset xs = fmdom' , symmetric])
      ― ‹$\mathcal{H}\;\vdash\;\d{\textsf{S}}\;
          ^{x^2_{\alpha_2}\;\dots\;x^n_{\alpha_n}}
          _{y^2_{\alpha_2}\;\dots\;y^n_{\alpha_n}} B$›
      ultimately have "  S  B"
        using Cons.IH and lset xs = fmdom'  by blast
      moreover from Cons.prems(2,4) have "(x, α)  free_vars "
        using vx = (x, α) by auto
      moreover have "is_free_for (FVar vy) (x, α) (S  B)"
      proof -
        have "vy  fmdom' "
          using Cons.prems(1) and lset xs = fmdom'  by force
        moreover have "fmran'  = lset (map FVar ys)"
          using Cons.hyps(1) and distinct xs by simp
        then have "vy  vars (fmran' )"
          using Cons.prems(3) by force
        moreover have "vy  vars B"
          using Cons.prems(1) by fastforce
        ultimately have "vy  vars (S  B)"
          by (rule excluded_var_from_substitution[OF is_substitution ])
        then show ?thesis
          by (fact absent_var_is_free_for)
      qed
      ― ‹$\mathcal{H}\;\vdash\;\d{\textsf{S}}\;^{x^1_{\alpha_1}}_{y^1_{\alpha_1}}\;\d{\textsf{S}}\;
          ^{x^2_{\alpha_2}\;\dots\;x^n_{\alpha_n}}_{y^2_{\alpha_2}\;\dots\;y^n_{\alpha_n}} B$›
      ultimately have "  S {(x, α)  FVar vy} (S  B)"
        using FVar vy  wffs⇘α⇙› by (rule prop_5221_aux)
      ― ‹$\d{\textsf{S}}\;^{x^1_{\alpha_1}}_{y^1_{\alpha_1}}\;\d{\textsf{S}}\;
          ^{x^2_{\alpha_2}\;\dots\;x^n_{\alpha_n}}_{y^2_{\alpha_2}\;\dots\;y^n_{\alpha_n}} B =
          \d{\textsf{S}}\;^{x^1_{\alpha_1}\;\dots\;x^n_{\alpha_n}}_{y^1_{\alpha_1}\;\dots\;y^n_{\alpha_n}} B$›
      moreover have "S {vx  FVar vy} S  B = S ({vx  FVar vy} ++f ) B"
      proof -
        have "vx  lset ys"
          using Cons.prems(1) by fastforce
        then have "S {vx  FVar vy} (FVar y) = FVar y" if "y  lset ys" for y
          using that and free_var_singleton_substitution_neutrality and surj_pair[of y] by fastforce
        with fmran'  = FVar ` lset ys have "fmmap (λA'. S {vx  FVar vy} A')  = "
          by (fastforce intro: fmap.map_ident_strong)
        with vx  fmdom'  show ?thesis
          using v  fmdom' . var_name v  free_var_names   is_free_for ( $$! v) v B
          and substitution_consolidation by auto
      qed
      ― ‹$\mathcal{H}\;\vdash\;\d{\textsf{S}}\;
          ^{x^1_{\alpha_1}\;\dots\;x^n_{\alpha_n}}_{y^1_{\alpha_1}\;\dots\;y^n_{\alpha_n}} B$›
      ultimately show ?case
        using vx = (x, α) and vx  fmdom'  and fmap_singleton_comm by fastforce
    qed
    with 0 and that show ?case
      by auto
  next
    case (Suc k)
    let ?ps = "λk. zip xs (take k As @ drop k (map FVar ys))"
    let ?y = "ys ! k" and ?A = "As ! k"
    let  = "λk. fmap_of_list (?ps k)"
    let ?θ' = "λk. fmap_of_list (map (λ(v', A'). (v', S {?y  ?A} A')) (?ps k))"
    have "fmdom' ( k') = lset xs" for k'
      by (simp add: length xs = length As length ys = length xs)
    have "fmdom' (?θ' k') = lset xs" for k'
      using length xs = length As and length ys = length xs and fmdom'_fmap_of_list by simp
    have "?y  lset ys"
      using Suc.prems length ys = length xs by simp
    have "j < length ys. ys ! j  vars (::form set)  ys ! j  vars B"
      using (var_name ` lset ys)  (var_name ` (vars B  vars (lset As)  vars   lset xs)) = {}
      by force
    obtain ny and αy where "(ny, αy) = ?y"
      using surj_pair[of ?y] by fastforce
    moreover have "?A  wffs⇘αy⇙"
    proof -
      from Suc.prems and (ny, αy) = ?y have "var_type (xs ! k) = αy"
        using length ys = length xs and map var_type ys = map var_type xs and Suc_le_lessD
        by (metis nth_map snd_conv)
      with Suc.prems and assms(2) and lset xs = fmdom' θ and As = map (($$!) θ) xs show ?thesis
        using less_eq_Suc_le and nth_mem by fastforce
    qed
    ultimately have "is_substitution {?y  ?A}"
      by auto
    have wfs: "is_substitution ( k)" for k
    unfolding is_substitution_def proof
      fix v
      assume "v  fmdom' ( k)"
      with fmdom' ( k) = lset xs obtain j where "v = xs ! j" and "j < length xs"
        by (fastforce simp add: in_set_conv_nth)
      obtain α where "var_type v = α"
        by blast
      show "case v of (x, α)  ( k) $$! (x, α)  wffs⇘α⇙"
      proof (cases "j < k")
        case True
        with j < length xs and v = xs ! j have "( k) $$! v = As ! j"
          using distinct xs and length xs = length As and length ys = length xs by force
        with assms(2) v = xs ! j and v  fmdom' ( k) and var_type v = α and j < length xs
        have "( k) $$! v  wffs⇘α⇙"
          using As = map (($$!) θ) xs and fmdom' ( k) = lset xs and lset xs = fmdom' θ
          by auto
        then show ?thesis
          using var_type v = α by force
      next
        case False
        with j < length xs and v = xs ! j have "( k) $$! v = FVar (ys ! j)"
          using distinct xs and length xs = length As and length ys = length xs by force
        with j < length xs and v = xs ! j and var_type v = α and length ys = length xs
        have "( k) $$! v  wffs⇘α⇙"
          using map var_type ys = map var_type xs and surj_pair[of "ys ! j"]
          by (metis nth_map snd_conv wffs_of_type_intros(1))
        then show ?thesis
          using var_type v = α by force
      qed
    qed
    have θ'_alt_def: "?θ' k = fmap_of_list
      (zip xs
        (take k (map (λA'. S {?y  ?A} A') As)
        @
        (drop k (map (λA'. S {?y  ?A} A') (map FVar ys)))))"
    proof -
      have "
        fmap_of_list (zip xs (map (λA'. S {?y  ?A} A') (take k As @ drop k (map FVar ys))))
        =
        fmap_of_list
          (zip xs
            (map (λA'. S {?y  ?A} A') (take k As)
            @
            (drop k (map (λA'. S {?y  ?A} A') (map FVar ys)))))"
        by (simp add: drop_map)
      then show ?thesis
        by (metis take_map zip_map2)
    qed
    ― ‹$\mathcal{H}\;\vdash\;\d{\textsf{S}}\;
        ^{x^1_{\alpha_1}\;\dots\;x^k_{\alpha_k} x^{k+1}_{\alpha_{k+1}}\;\dots\;x^n_{\alpha_n}}
        _{A^1_{\alpha_1}\;\dots\;A^k_{\alpha_k} y^{k+1}_{\alpha_{k+1}}\;\dots\;y^n_{\alpha_n}} B$›
    have "  S ( k) B"
      by (fact Suc.IH[OF Suc_leD[OF Suc.prems]])
    ― ‹$\mathcal{H}\;\vdash\;\d{\textsf{S}}\;^{y^{k+1}_{\alpha_{k+1}}}_{A^{k+1}_{\alpha_{k+1}}}\;
        \d{\textsf{S}}\;
        ^{x^1_{\alpha_1}\;\dots\;x^k_{\alpha_k} x^{k+1}_{\alpha_{k+1}}\;\dots\;x^n_{\alpha_n}}
        _{A^1_{\alpha_1}\;\dots\;A^k_{\alpha_k} y^{k+1}_{\alpha_{k+1}}\;\dots\;y^n_{\alpha_n}} B$›
    then have "  S {?y  ?A} S ( k) B"
    proof -
      from (ny, αy) = ?y and length ys = length xs have "(ny, αy)  free_vars "
        using j < length ys. ys ! j  vars (::form set)  ys ! j  vars B
        and free_vars_in_all_vars_set and Suc_le_lessD[OF Suc.prems] by fastforce
      moreover have "is_free_for ?A (ny, αy) (S ( k) B)"
      proof -
        have "is_substitution (fmdrop (xs ! k) ( k))"
          using wfs and fmdom' ( k) = lset xs by force
        moreover from Suc_le_lessD[OF Suc.prems] have "var_type (xs ! k) = var_type (ys ! k)"
          using length ys = length xs and map var_type ys = map var_type xs by (metis nth_map)
        then have "is_substitution {xs ! k  FVar ?y}"
          unfolding is_substitution_def using (ny, αy) = ?y
          by (intro ballI) (clarsimp, metis snd_eqD wffs_of_type_intros(1))
        moreover have "(xs ! k)  fmdom' (fmdrop (xs ! k) ( k))"
          by simp
        moreover have "
          v  fmdom' (fmdrop (xs ! k) ( k)). ?y  vars (fmdrop (xs ! k) ( k) $$! v)"
        proof
          fix v
          assume "v  fmdom' (fmdrop (xs ! k) ( k))"
          then have "v  fmdom' ( k)"
            by simp
          with fmdom' ( k) = lset xs obtain j where "v = xs ! j" and "j < length xs" and "j  k"
            using v  fmdom' (fmdrop (xs ! k) ( k))
            and (xs ! k)  fmdom' (fmdrop (xs ! k) ( k)) by (metis in_set_conv_nth)
          then show "?y  vars ((fmdrop (xs ! k) ( k)) $$! v)"
          proof (cases "j < k")
            case True
            with j < length xs and v = xs ! j have "( k) $$! v = As ! j"
              using distinct xs and length xs = length As and length ys = length xs by force
            moreover from j < length xs and length xs = length As have "?y  vars (As ! j)"
              using ?y  lset ys and ys_fresh by fastforce
            ultimately show ?thesis
              using v  fmdom' (fmdrop (xs ! k) ( k)) by auto
          next
            case False
            with j < length xs and v = xs ! j have "( k) $$! v = FVar (ys ! j)"
              using distinct xs and length xs = length As and length ys = length xs by force
            moreover from Suc_le_lessD[OF Suc.prems] and j  k have "?y  ys ! j"
              by (simp add: distinct ys j < length xs length ys = length xs nth_eq_iff_index_eq)
            ultimately show ?thesis
              using v  fmdom' (fmdrop (xs ! k) ( k))
              and xs ! k  fmdom' (fmdrop (xs ! k) ( k)) and surj_pair[of "ys ! j"] by fastforce
          qed
        qed
        moreover from k < length xs and length ys = length xs have "?y  vars B"
          by (simp add: j < length ys. ys ! j  vars   ys ! j  vars B)
        moreover have "is_free_for ?A (xs ! k) B"
        proof -
          from Suc_le_lessD[OF Suc.prems] and lset xs = fmdom' θ have "xs ! k  fmdom' θ"
            using nth_mem by blast
          moreover from Suc.prems and As = map (($$!) θ) xs have "θ $$! (xs ! k) = ?A"
            by fastforce
          ultimately show ?thesis
            using assms(3) by simp
        qed
        moreover
        have "v  fmdom' (fmdrop (xs ! k) ( k)). is_free_for (fmdrop (xs ! k) ( k) $$! v) v B"
        proof
          fix v
          assume "v  fmdom' (fmdrop (xs ! k) ( k))"
          then have "v  fmdom' ( k)"
            by simp
          with fmdom' ( k) = lset xs obtain j where "v = xs ! j" and "j < length xs" and "j  k"
            using v  fmdom' (fmdrop (xs ! k) ( k))
            and (xs ! k)  fmdom' (fmdrop (xs ! k) ( k)) by (metis in_set_conv_nth)
          then show "is_free_for (fmdrop (xs ! k) ( k) $$! v) v B"
          proof (cases "j < k")
            case True
            with j < length xs and v = xs ! j have "( k) $$! v = As ! j"
              using distinct xs and length xs = length As and length ys = length xs by force
            moreover have "is_free_for (As ! j) v B"
            proof -
              from j < length xs and lset xs = fmdom' θ and v = xs ! j have "v  fmdom' θ"
                using nth_mem by blast
              moreover have "θ $$! v = As ! j"
                by (simp add: As = map (($$!) θ) xs j < length xs v = xs ! j)
              ultimately show ?thesis
                using assms(3) by simp
              qed
            ultimately show ?thesis
              using v  fmdom' (fmdrop (xs ! k) ( k)) by auto
          next
            case False
            with j < length xs and v = xs ! j have "( k) $$! v = FVar (ys ! j)"
              using distinct xs and length xs = length As and length ys = length xs by force
            moreover from j < length xs and length ys = length xs have "ys ! j  vars B"
              using j < length ys. ys ! j  vars   ys ! j  vars B by simp
            then have "is_free_for (FVar (ys ! j)) v B"
              by (fact absent_var_is_free_for)
            ultimately show ?thesis
              using v  fmdom' (fmdrop (xs ! k) ( k)) by auto
          qed
        qed
        ultimately have "is_free_for ?A (ys ! k) S ({xs ! k  FVar ?y} ++f fmdrop (xs ! k) ( k)) B"
          using is_free_for_with_renaming_substitution by presburger
        moreover have "S ({xs ! k  FVar ?y} ++f fmdrop (xs ! k) ( k)) B = S ( k) B"
          using length xs = length As and length ys = length xs and Suc_le_eq and Suc.prems
          and distinct xs by simp
        ultimately show ?thesis
          unfolding (ny, αy) = ?y by simp
      qed
      ultimately show ?thesis
        using prop_5221_aux[OF   S ( k) B] and ?A  wffs⇘αy⇙› and (ny, αy) = ?y by metis
    qed
    ― ‹$\d{\textsf{S}}\;^{y^{k+1}_{\alpha_{k+1}}}_{A^{k+1}_{\alpha_{k+1}}}\;
        \d{\textsf{S}}\;
        ^{x^1_{\alpha_1}\;\dots\;x^k_{\alpha_k} x^{k+1}_{\alpha_{k+1}}\;\dots\;x^n_{\alpha_n}}
        _{A^1_{\alpha_1}\;\dots\;A^k_{\alpha_k} y^{k+1}_{\alpha_{k+1}}\;\dots\;y^n_{\alpha_n}} B =
        \d{\textsf{S}}\;
        ^{x^1_{\alpha_1}\;\dots\;x^k_{\alpha_k} x^{k+1}_{\alpha_{k+1}} x^{k+2}_{\alpha_{k+2}}
         \;\dots\;x^n_{\alpha_n}}
        _{A^1_{\alpha_1}\;\dots\;A^k_{\alpha_k} A^{k+1}_{\alpha_{k+1}} y^{k+2}_{\alpha_{k+2}}
         \;\dots\;y^n_{\alpha_n}} B$›
    moreover have "S {?y  ?A} S ( k) B = S ( (Suc k)) B"
    proof -
      have "S {?y  ?A} S ( k) B = S {?y  ?A} ++f (?θ' k) B"
      proof -
        have "?y  fmdom' ( k)"
          using ?y  lset ys and fmdom' ( k) = lset xs and ys_fresh by blast
        moreover have "(?θ' k) = fmmap (λA'. S {?y  ?A} A') ( k)"
          using length xs = length As and length ys = length xs by simp
        moreover have "v'  fmdom' ( k). is_free_for ( k $$! v') v' B"
        proof
          fix v'
          assume "v'  fmdom' ( k)"
          with fmdom' ( k) = lset xs obtain j where "v' = xs ! j" and "j < length xs"
            by (metis in_set_conv_nth)
          obtain α where "var_type v' = α"
            by blast
          show "is_free_for ( k $$! v') v' B"
          proof (cases "j < k")
            case True
            with j < length xs and v' = xs ! j have "( k) $$! v' = As ! j"
              using distinct xs and length xs = length As and length ys = length xs by force
            moreover from lset xs = fmdom' θ and assms(3) have "is_free_for (As ! j) (xs ! j) B"
              by (metis As = map (($$!) θ) xs j < length xs nth_map nth_mem)
            ultimately show ?thesis
              using v' = xs ! j by (simp only:)
          next
            case False
            with j < length xs and v' = xs ! j have "( k) $$! v' = FVar (ys ! j)"
              using distinct xs and length xs = length As and length ys = length xs by force
            moreover from j < length xs have "is_free_for (FVar (ys ! j)) (xs ! j) B"
              using j < length ys. ys ! j  vars   ys ! j  vars B and length ys = length xs
              and absent_var_is_free_for by presburger
            ultimately show ?thesis
              using v' = xs ! j by (simp only:)
          qed
        qed
        ultimately show ?thesis
          using substitution_consolidation by simp
      qed
      also have " = S {?y  ?A} ++f ( (Suc k)) B"
      proof -
        have "?θ' k =  (Suc k)"
        proof (intro fsubset_antisym[unfolded fmsubset_alt_def] fmpredI)
          {
            fix v' and A'
            assume "?θ' k $$ v' = Some A'"
            then have "v'  fmdom' (?θ' k)"
              by (intro fmdom'I)
            then obtain j where "j < length xs" and "xs ! j = v'"
              using fmdom' (?θ' k) = lset xs by (metis in_set_conv_nth)
            then consider (a) "j < k" | (b) "j = k" | (c) "j  {k<..< length xs}"
              by fastforce
            then show " (Suc k) $$ v' = Some A'"
            proof cases
              case a
              with θ'_alt_def and distinct xs and j < length xs
              have "?θ' k $$ (xs ! j) = Some (take k (map (λA'. S {?y  ?A} A') As) ! j)"
                using length xs = length As and length ys = length xs by auto
              also from a and Suc.prems have " = Some (S {?y  ?A} (As ! j))"
                using length xs = length As by auto
              also have " = Some (As ! j)"
              proof -
                from Suc.prems and length ys = length xs have "Suc k  length ys"
                  by (simp only:)
                moreover have "j < length As"
                  using j < length xs and length xs = length As by (simp only:)
                ultimately have "?y  vars (As ! j)"
                  using ys_fresh by force
                then show ?thesis
                  using free_var_singleton_substitution_neutrality and free_vars_in_all_vars by blast
              qed
              also from a and xs ! j = v' and distinct xs have " =  (Suc k) $$ v'"
                using j < length xs and length xs = length As and length ys = length xs
                by fastforce
              finally show ?thesis
                using ?θ' k $$ v' = Some A' and xs ! j = v' by simp
            next
              case b
              then have "
                ?θ' k $$ (xs ! k) = Some (drop k (map (λA'. S {?y  ?A} A') (map FVar ys)) ! 0)"
                using distinct xs and j < length xs and length xs = length As
                and length ys = length xs and fmap_of_list_nth_split by simp
              also from Suc.prems have " = Some (S {?y  ?A} (FVar ?y))"
                using length ys = length xs by simp
              also from (ny, αy) = ys ! k have " = Some ?A"
                by (metis singleton_substitution_simps(1))
              also from b and xs ! j = v' and distinct xs have " =  (Suc k) $$ v'"
                using j < length xs and length xs = length As and length ys = length xs
                by fastforce
              finally show ?thesis
                using b and ?θ' k $$ v' = Some A' and xs ! j = v' by force
            next
              case c
              then have "j > k"
                by simp
              with θ'_alt_def and distinct xs and j < length xs have "
                ?θ' k $$ (xs ! j) = Some (drop k (map (λA'. S {?y  ?A} A') (map FVar ys)) ! (j - k))"
                using fmap_of_list_nth_split and length xs = length As and length ys = length xs
                by simp
              also from Suc.prems and c have " = Some (S {?y  ?A} (FVar (ys ! j)))"
                using length ys = length xs by simp
              also from Suc_le_lessD[OF Suc.prems] and distinct ys have " = Some (FVar (ys ! j))"
                using j < length xs and k < j and length ys = length xs
                by (metis nless_le nth_eq_iff_index_eq prod.exhaust_sel singleton_substitution_simps(1))
              also from c and distinct xs have " =  (Suc k) $$ v'"
                using xs ! j = v' and length xs = length As and length ys = length xs by force
              finally show ?thesis
                using ?θ' k $$ v' = Some A' and xs ! j = v' by force
            qed
          }
          note θ_k_in_Sub_k = this
          {
            fix v' and A'
            assume " (Suc k) $$ v' = Some A'"
            then have "v'  fmdom' ( (Suc k))"
              by (intro fmdom'I)
            then obtain j where "j < length xs" and "xs ! j = v'"
              using fmdom' ( (Suc k)) = lset xs by (metis in_set_conv_nth)
            then consider (a) "j < k" | (b) "j = k" | (c) "j  {k<..< length xs}"
              by fastforce
            with j < length xs and xs ! j = v' and θ_k_in_Sub_k show "?θ' k $$ v' = Some A'"
              using k'. fmdom' (?θ' k') = lset xs and  (Suc k) $$ v' = Some A'
              by (metis (mono_tags, lifting) fmlookup_dom'_iff nth_mem)+
          }
        qed
        then show ?thesis
          by presburger
      qed
      also have " = S ( (Suc k)) B"
      proof -
        have " (Suc k) $$ ?y = None"
          using ?y  lset ys k'. fmdom' ( k') = lset xs and ys_fresh by blast
        moreover from Suc_le_lessD[OF Suc.prems] have "?y  vars B"
          using j < length ys. ys ! j  vars   ys ! j  vars B and length ys = length xs
          by auto
        ultimately show ?thesis
          by (rule substitution_absorption)
      qed
      finally show ?thesis .
    qed
    ― ‹$\mathcal{H}\;\vdash\;\d{\textsf{S}}\;
        ^{x^1_{\alpha_1}\;\dots\;x^k_{\alpha_k} x^{k+1}_{\alpha_{k+1}} x^{k+2}_{\alpha_{k+2}}
         \;\dots\;x^n_{\alpha_n}}
        _{A^1_{\alpha_1}\;\dots\;A^k_{\alpha_k} A^{k+1}_{\alpha_{k+1}} y^{k+2}_{\alpha_{k+2}}
         \;\dots\;y^n_{\alpha_n}} B$›
    ultimately show ?case
      by (simp only:)
  qed
  ― ‹$\mathcal{H}\;\vdash\;\d{\textsf{S}}\;
      ^{x^1_{\alpha_1}\;\dots\;x^n_{\alpha_n}} _{A^1_{\alpha_1}\;\dots\;A^n_{\alpha_n}} B$›
  then have "  S (fmap_of_list (zip xs As)) B"
    using length xs = length As and length ys = length xs by force
  moreover have "fmap_of_list (zip xs As) = θ"
  proof (intro fsubset_antisym[unfolded fmsubset_alt_def] fmpredI)
    fix v and A
    assume "fmap_of_list (zip xs As) $$ v = Some A"
    with lset xs = fmdom' θ have "v  fmdom' θ"
      by (fast dest: fmap_of_list_SomeD set_zip_leftD)
    with fmap_of_list (zip xs As) $$ v = Some A and As = map (($$!) θ) xs show "θ $$ v = Some A"
      by
        (simp add: map_of_zip_map fmap_of_list.rep_eq split: if_splits)
        (meson fmdom'_notI option.exhaust_sel)
  next
    fix v and A
    assume "θ $$ v = Some A"
    with As = map (($$!) θ) xs show "fmap_of_list (zip xs As) $$ v = Some A"
      using lset xs = fmdom' θ by (simp add: fmap_of_list.rep_eq fmdom'I map_of_zip_map)
  qed
  ultimately show ?thesis
    by (simp only:)
qed

end

lemmas Sub = prop_5221 (* synonym *)

subsection ‹Proposition 5222 (Rule of Cases)›

lemma forall_α_conversion:
  assumes "A  wffs⇘o⇙"
  and "(z, β)  free_vars A"
  and "is_free_for (zβ) (x, β) A"
  shows " xβ⇙. A =⇘ozβ⇙. S {(x, β)  zβ} A"
proof -
  from assms(1) have "xβ⇙. A  wffs⇘o⇙"
    by (intro forall_wff)
  then have " xβ⇙. A =⇘oxβ⇙. A"
    by (fact prop_5200)
  moreover from assms have " (λxβ⇙. A) =⇘βo(λzβ⇙. S {(x, β)  zβ} A)"
    by (rule prop_5206)
  ultimately show ?thesis
    unfolding forall_def and PI_def by (rule rule_R [where p = "[»,»]"]) force+
qed

proposition prop_5222:
  assumes "  S {(x, o)  To} A" and "  S {(x, o)  Fo} A"
  and "A  wffs⇘o⇙"
  shows "  A"
proof -
  from assms(1) have "is_hyps "
    by (blast elim: is_derivable_from_hyps.cases)
  have "§1": "  T⇘o⇙ =⇘o(λxo⇙. A) · To"
  proof -
    have " (λxo⇙. A) · T⇘o⇙ =⇘oS {(x, o)  To} A"
      using prop_5207[OF true_wff assms(3) closed_is_free_for] by simp
    from this and assms(1) have "  (λxo⇙. A) · To"
      using rule_RR[OF disjI2, where p = "[]"] by fastforce
    moreover have "(λxo⇙. A) · To  wffs⇘o⇙"
      by (fact hyp_derivable_form_is_wffso[OF   (λxo⇙. A) · To])
    ultimately show ?thesis
      using rule_T(1) by blast
  qed
  moreover have "§2": "  T⇘o⇙ =⇘o(λxo⇙. A) · Fo"
  proof -
    have " (λxo⇙. A) · F⇘o⇙ =⇘oS {(x, o)  Fo} A"
      using prop_5207[OF false_wff assms(3) closed_is_free_for] by simp
    from this and assms(2) have "  (λxo⇙. A) · Fo"
      using rule_RR[OF disjI2, where p = "[]"] by fastforce
    moreover have "(λxo⇙. A) · Fo  wffs⇘o⇙"
      by (fact hyp_derivable_form_is_wffso[OF   (λxo⇙. A) · Fo])
    ultimately show ?thesis
      using rule_T(1) by blast
  qed
  moreover from prop_5212 and is_hyps  have "§3": "  To 𝒬 To"
    by (rule derivability_implies_hyp_derivability)
  ultimately have "  (λxo⇙. A) · To 𝒬 (λxo⇙. A) · Fo"
  proof -
    from "§3" and "§1" have "  (λxo⇙. A) · To 𝒬 To"
      by (rule rule_R'[where p = "[«,»]"]) (force+, fastforce dest: subforms_from_app)
    from this and "§2" show ?thesis
      by (rule rule_R'[where p = "[»]"]) (force+, fastforce dest: subforms_from_app)
  qed
  moreover have " (λxo⇙. A) · To 𝒬 (λxo⇙. A) · F⇘o⇙ =⇘oxo⇙. A"
  proof -
    have "𝔤oo· 𝔵o wffs⇘o⇙"
      by blast
    have " 𝔤oo· To 𝒬 𝔤oo· F⇘o⇙ =⇘o𝔵o⇙. 𝔤oo· 𝔵o⇙"
      using axiom_1[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
    ― ‹By $\alpha$-conversion›
    then have " 𝔤oo· To 𝒬 𝔤oo· F⇘o⇙ =⇘oxo⇙. 𝔤oo· xo⇙" (is " ?B =⇘o?C")
    proof -
      have " 𝔵o⇙. 𝔤oo· 𝔵o⇙ =⇘oxo⇙. 𝔤oo· xo⇙"
      proof (cases "x = 𝔵")
        case True
        from 𝔤oo· 𝔵o wffs⇘o⇙› have " 𝔵o⇙. 𝔤oo· 𝔵o⇙ =⇘o𝔵o⇙. 𝔤oo· 𝔵o⇙"
          by (fact prop_5200[OF forall_wff])
        with True show ?thesis
          using identity_singleton_substitution_neutrality by simp
      next
        case False
        from 𝔤oo· 𝔵o wffs⇘o⇙›
        have " 𝔵o⇙. 𝔤oo· 𝔵o⇙ =⇘oxo⇙. S {(𝔵, o)  xo} (𝔤oo· 𝔵o)"
          by
            (rule forall_α_conversion)
            (simp add: False, intro is_free_for_to_app is_free_for_in_var)
        then show ?thesis
          by force
      qed
      with  𝔤oo· To 𝒬 𝔤oo· F⇘o⇙ =⇘o𝔵o⇙. 𝔤oo· 𝔵o⇙› show ?thesis
        using Equality_Rules(3) by blast
    qed
    ― ‹By Sub›
    then have *: " (λxo⇙. A) · To 𝒬 (λxo⇙. A) · F⇘o⇙ =⇘oxo⇙. (λxo⇙. A) · xo⇙"
    proof -
      let  = "{(𝔤, oo)  λxo⇙. A}"
      from assms(3) have "is_substitution "
        by auto
      moreover have "
        v  fmdom' .
          var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v (?B =⇘o?C)"
        by (code_simp, (unfold atomize_conj[symmetric])?, simp)+ blast
      moreover have "  {$$}"
        by simp
      ultimately have " S  (?B =⇘o?C)"
        by (rule Sub [OF  ?B =⇘o?C])
      then show ?thesis
        by simp
    qed
    ― ‹By $\lambda$-conversion›
    then show ?thesis
    proof -
      have " (λxo⇙. A) · xo⇙ =⇘oA"
        using prop_5208[where vs = "[(x, o)]"] and assms(3) by simp
      from * and this show ?thesis
        by (rule rule_R[where p = "[»,»,«]"]) force+
    qed
  qed
  ultimately have "  xo⇙. A"
    using rule_RR and is_subform_at.simps(1) by (blast intro: empty_is_position)
  then show ?thesis
  proof -
    have "is_free_for (xo) (x, o) A"
      by fastforce
    from   xo⇙. A and wffs_of_type_intros(1) and this show ?thesis
      by (rule "∀I"[of  x o A "xo⇙", unfolded identity_singleton_substitution_neutrality])
  qed
qed

lemmas Cases = prop_5222 (* synonym *)

subsection ‹Proposition 5223›

proposition prop_5223:
  shows " (To 𝒬 𝔶o) =⇘o𝔶o⇙"
proof -
  have " (To 𝒬 𝔶o) =⇘o(T⇘o⇙ =⇘o(To 𝒬 𝔶o))"
  proof -
    let ?A = "(λ𝔵o⇙. λ𝔶o⇙. (𝔵o𝒬 𝔵o𝒬 𝔶o)) · To · 𝔶o⇙"
    have "?A  wffs⇘o⇙"
      by force
    then have " ?A =⇘o?A"
      by (fact prop_5200)
    then have " (To 𝒬 𝔶o) =⇘o?A"
      unfolding imp_fun_def and imp_op_def .
    moreover
    have " (λ𝔵o⇙. λ𝔶o⇙. (𝔵o𝒬 𝔵o𝒬 𝔶o)) · T⇘o⇙ =⇘ooλ𝔶o⇙. (To 𝒬 To 𝒬 𝔶o)"
    proof -
      have "λ𝔶o⇙. (𝔵o𝒬 𝔵o𝒬 𝔶o)  wffs⇘oo⇙"
        by auto
      moreover
      have "is_free_for To (𝔵, o) (λ𝔶o⇙. (𝔵o𝒬 𝔵o𝒬 𝔶o))"
        by fastforce
      moreover
      have "S {(𝔵, o)  To} (λ𝔶o⇙. (𝔵o𝒬 𝔵o𝒬 𝔶o)) = (λ𝔶o⇙. (To 𝒬 To 𝒬 𝔶o))"
        by simp
      ultimately show ?thesis
        using prop_5207[OF true_wff] by metis
    qed
    ultimately have *: " (To 𝒬 𝔶o) =⇘o(λ𝔶o⇙. (To 𝒬 To 𝒬 𝔶o)) · 𝔶o⇙"
      by (rule rule_R [where p = "[»,«]"]) force+
    have "To 𝒬 To 𝒬 𝔶o wffs⇘o⇙"
      by auto
    then have " (λ𝔶o⇙. (To 𝒬 To 𝒬 𝔶o)) · 𝔶o⇙ =⇘o(To 𝒬 To 𝒬 𝔶o)"
      using prop_5208[where vs = "[(𝔶, o)]"] by simp
    from * and this show ?thesis
      by (rule rule_R[where p = "[»]"]) force+
  qed
  with prop_5218 have " (To 𝒬 𝔶o) =⇘o(To 𝒬 𝔶o)"
    using rule_R and Equality_Rules(3) by (meson conj_op_wff true_wff wffs_of_type_intros(1))
  with prop_5216 show ?thesis
    using rule_R and Equality_Rules(3) by (meson conj_op_wff true_wff wffs_of_type_intros(1))
qed

corollary generalized_prop_5223:
  assumes "A  wffs⇘o⇙"
  shows " (To 𝒬 A) =⇘oA"
proof -
  have "To 𝒬 𝔶o wffs⇘o⇙" and "is_free_for A (𝔶, o) ((To 𝒬 𝔶o) =⇘o𝔶o)"
   by (blast, intro is_free_for_in_equality is_free_for_in_imp is_free_for_in_true is_free_for_in_var)
  from this(2) have " S {(𝔶, o)  A} ((To 𝒬 𝔶o) =⇘o𝔶o)"
    by (rule prop_5209[OF assms ‹To 𝒬 𝔶o wffs⇘o⇙› wffs_of_type_intros(1) prop_5223])
  then show ?thesis
    by simp
qed

subsection ‹Proposition 5224 (Modus Ponens)›

proposition prop_5224:
  assumes "  A" and "  A 𝒬 B"
  shows "  B"
proof -
  have "  A 𝒬 B"
    by fact
  moreover from assms(1) have "A  wffs⇘o⇙"
    by (fact hyp_derivable_form_is_wffso)
  from this and assms(1) have "  A =⇘o⇙ T⇘o⇙"
    using rule_T(2) by blast
  ultimately have "  To 𝒬 B"
    by (rule rule_R'[where p = "[«,»]"]) (force+, fastforce dest: subforms_from_app)
  have " (To 𝒬 B) =⇘oB"
  proof -
    let  = "{(𝔶, o)  B}"
    have "B  wffs⇘o⇙"
      by (fact hyp_derivable_form_is_wffso[OF assms(2), THEN wffs_from_imp_op(2)])
    then have "is_substitution "
      by simp
    moreover have "
      v  fmdom' .
        var_name v  free_var_names ({}::form set) 
        is_free_for ( $$! v) v ((To 𝒬 𝔶o) =⇘o𝔶o)"
      by (code_simp, (unfold atomize_conj[symmetric])?, simp)+ blast
    moreover have "  {$$}"
      by simp
    ultimately have " S  ((To 𝒬 𝔶o) =⇘o𝔶o)"
      by (rule Sub[OF prop_5223])
    then show ?thesis
      by simp
  qed
  then show ?thesis
    by (rule rule_RR[OF disjI1, where p = "[]"]) (use   To 𝒬 B in force+)
qed

lemmas MP = prop_5224 (* synonym *)

corollary generalized_modus_ponens:
  assumes "  hs 𝒬 B" and "H  lset hs.   H"
  shows "  B"
using assms proof (induction hs arbitrary: B rule: rev_induct)
  case Nil
  then show ?case
    by simp
next
  case (snoc H' hs)
  from H  lset (hs @ [H']).   H have "  H'"
    by simp
  moreover have "  H' 𝒬 B"
  proof -
    from   (hs @ [H']) 𝒬 B have "  hs 𝒬 (H' 𝒬 B)"
      by simp
    moreover from H  lset (hs @ [H']).   H have "H  lset hs.   H"
      by simp
    ultimately show ?thesis
      by (elim snoc.IH)
  qed
  ultimately show ?case
    by (rule MP)
qed

subsection ‹Proposition 5225›

proposition prop_5225:
  shows " ∏⇘α· 𝔣αo𝒬 𝔣αo· 𝔵α⇙"
proof -
  have "𝔣αo· 𝔵α wffs⇘o⇙"
    by blast
  have "§1": "
    
      ∏⇘α· 𝔣αo𝒬 (((λ𝔣αo⇙. 𝔣αo· 𝔵α) · (λ𝔵α⇙. T⇘o⇙))
      =⇘o((λ𝔣αo⇙. 𝔣αo· 𝔵α) · 𝔣αo))"
  proof -
    let  = "{(𝔥, (αo)o)  λ𝔣αo⇙. 𝔣αo· 𝔵α, (𝔵, αo)  λ𝔵α⇙. T⇘o⇙, (𝔶, αo)  𝔣αo}"
      and ?A = "(𝔵αo⇙ =⇘αo𝔶αo) 𝒬 (𝔥(αo)o· 𝔵αo𝒬 𝔥(αo)o· 𝔶αo)"
    have " ?A"
      by (fact axiom_is_derivable_from_no_hyps[OF axiom_2])
    moreover have "λ𝔣αo⇙. 𝔣αo· 𝔵α wffs⇘(αo)o⇙" and "λ𝔵α⇙. T⇘o⇙  wffs⇘αo⇙"
      and "𝔣αo wffs⇘αo⇙"
      by blast+
    then have "is_substitution "
      by simp
    moreover have "
      v  fmdom' . var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v ?A"
      by (code_simp, (unfold atomize_conj[symmetric])?, simp)+ blast
    moreover have "  {$$}"
      by simp
    ultimately have " S  ?A"
      by (rule Sub)
    then show ?thesis
      by simp
  qed
  have " ∏⇘α· 𝔣αo𝒬 (T⇘o⇙ =⇘o𝔣αo· 𝔵α)"
  proof -
    have "
       (λ𝔣αo⇙. 𝔣αo· 𝔵α) · (λ𝔵α⇙. T⇘o⇙) =⇘o(λ𝔵α⇙. T⇘o⇙) · 𝔵α⇙"
      (is " (λ?x⇙. ?B) · ?A =⇘o?C")
    proof -
      have " (λ?x⇙. ?B) · ?A =⇘oS {(?x, )  ?A} ?B"
        using prop_5207[OF wffs_of_type_intros(4)[OF true_wff] ?B  wffs⇘o⇙›] by fastforce
      then show ?thesis
        by simp
    qed
    moreover have " (λ𝔵α⇙. T⇘o⇙) · 𝔵α⇙ =⇘o⇙ T⇘o⇙"
      using prop_5208[where vs = "[(𝔵, α)]"] and true_wff by simp
    ultimately have " (λ𝔣αo⇙. 𝔣αo· 𝔵α) · (λ𝔵α⇙. T⇘o⇙) =⇘o⇙ T⇘o⇙"
      by (rule Equality_Rules(3))
    from "§1" and this have " ∏⇘α· 𝔣αo𝒬 (T⇘o⇙ =⇘o((λ𝔣αo⇙. 𝔣αo· 𝔵α) · 𝔣αo))"
      by (rule rule_R[where p = "[»,«,»]"]) force+
    moreover have " (λ𝔣αo⇙. 𝔣αo· 𝔵α) · 𝔣αo⇙ =⇘o𝔣αo· 𝔵α⇙"
      using prop_5208[where vs = "[(𝔣, αo)]"] by force
    ultimately show ?thesis
      by (rule rule_R[where p = "[»,»]"]) force+
  qed
  from this and prop_5218[OF 𝔣αo· 𝔵α wffs⇘o⇙›] show ?thesis
    by (rule rule_R[where p = "[»]"]) auto
qed

subsection ‹Proposition 5226›

proposition prop_5226:
  assumes "A  wffs⇘α⇙" and "B  wffs⇘o⇙"
  and "is_free_for A (x, α) B"
  shows " xα⇙. B 𝒬 S {(x, α)  A} B"
proof -
  have " ∏⇘α· (λxα⇙. B) 𝒬 (λxα⇙. B) · A"
  proof -
    let  = "{(𝔣, αo)  λxα⇙. B, (𝔵, α)  A}"
    have " ∏⇘α· 𝔣αo𝒬 𝔣αo· 𝔵α⇙" (is " ?C")
      by (fact prop_5225)
    moreover from assms have "is_substitution "
      by auto
    moreover have "
      v  fmdom' . var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v ?C"
      by (code_simp, (unfold atomize_conj[symmetric])?, fastforce)+ blast
    moreover have "  {$$}"
      by simp
    ultimately have " S  ?C"
      by (rule Sub)
    moreover have "S  ?C = ∏⇘α· (λxα⇙. B) 𝒬 (λxα⇙. B) · A"
      by simp
    ultimately show ?thesis
      by (simp only:)
  qed
  moreover from assms have " (λxα⇙. B) · A =⇘oS {(x, α)  A} B"
    by (rule prop_5207)
  ultimately show ?thesis
    by (rule rule_R [where p = "[»]"]) force+
qed

subsection ‹Proposition 5227›

corollary prop_5227:
  shows " Fo 𝒬 𝔵o⇙"
proof -
  have " 𝔵o⇙. 𝔵o𝒬 S {(𝔵, o)  𝔵o} (𝔵o)"
    by (rule prop_5226) auto
  then show ?thesis
    using identity_singleton_substitution_neutrality by simp
qed

corollary generalized_prop_5227:
  assumes "A  wffs⇘o⇙"
  shows " Fo 𝒬 A"
proof -
  let  = "{(𝔵, o)  A}" and ?B = "Fo 𝒬 𝔵o⇙"
  from assms have "is_substitution "
    by simp
  moreover have "is_free_for A (𝔵, o) ?B"
    by (intro is_free_for_in_false is_free_for_in_imp is_free_for_in_var)
  then have "
    v  fmdom' . var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v ?B"
    by force
  ultimately have " S {(𝔵, o)  A} (Fo 𝒬 𝔵o)"
    using Sub[OF prop_5227, where θ = ] by fastforce
  then show ?thesis
    by simp
qed

subsection ‹Proposition 5228›

proposition prop_5228:
  shows " (To 𝒬 To) =⇘o⇙ T⇘o⇙"
  and " (To 𝒬 Fo) =⇘o⇙ F⇘o⇙"
  and " (Fo 𝒬 To) =⇘o⇙ T⇘o⇙"
  and " (Fo 𝒬 Fo) =⇘o⇙ T⇘o⇙"
proof -
  show " (To 𝒬 To) =⇘o⇙ T⇘o⇙" and " (To 𝒬 Fo) =⇘o⇙ F⇘o⇙"
    using generalized_prop_5223 by blast+
next
  have " Fo 𝒬 Fo" and " Fo 𝒬 To"
    using generalized_prop_5227 by blast+
  then show " (Fo 𝒬 To) =⇘o⇙ T⇘o⇙" and " (Fo 𝒬 Fo) =⇘o⇙ T⇘o⇙"
    using rule_T(2) by blast+
qed

subsection ‹Proposition 5229›

lemma false_in_conj_provability:
  assumes "A  wffs⇘o⇙"
  shows " Fo 𝒬 A 𝒬 Fo"
proof -
  have " (λ𝔵o⇙. λ𝔶o⇙. (𝔵o𝒬 𝔵o𝒬 𝔶o)) · Fo · A"
    by (intro generalized_prop_5227[OF assms, unfolded imp_op_def imp_fun_def])
  moreover have "
    
      (λ𝔵o⇙. λ𝔶o⇙. (𝔵o𝒬 𝔵o𝒬 𝔶o)) · F⇘o⇙
      =⇘ooλ𝔶o⇙. (Fo 𝒬 Fo 𝒬 𝔶o)"
    (is " (λ?x⇙. ?A) · ?B =⇘?C")
  proof -
    have "?B  wffs⇘⇙" and "?A  wffs⇘⇙" and "is_free_for ?B (?x, ) ?A"
      by auto
    then have " (λ?x⇙. ?A) · ?B =⇘S {(?x, )  ?B} ?A"
      by (rule prop_5207)
    moreover have "S {(?x, )  ?B} ?A = ?C"
      by simp
    ultimately show ?thesis
      by (simp only:)
  qed
  ultimately have " (λ𝔶o⇙. (Fo 𝒬 Fo 𝒬 𝔶o)) · A"
    by (rule rule_R[where p = "[«]"]) auto
  moreover have "
    
      (λ𝔶o⇙. (Fo 𝒬 Fo 𝒬 𝔶o)) · A
      =⇘o(Fo 𝒬 Fo 𝒬 A)"
    (is " (λ?x⇙. ?A) · ?B =⇘o?C")
  proof -
    have "?B  wffs⇘⇙" and "?A  wffs⇘o⇙"
      using assms by auto
    moreover have "is_free_for ?B (?x, ) ?A"
      by (intro is_free_for_in_equivalence is_free_for_in_conj is_free_for_in_false) fastforce
    ultimately have " (λ?x⇙. ?A) · ?B =⇘oS {(?x, )  ?B} ?A"
      by (rule prop_5207)
    moreover
    have "S {(?x, )  ?B} ?A = ?C"
      by simp
    ultimately show ?thesis
      by (simp only:)
  qed
  ultimately have " Fo 𝒬 Fo 𝒬 A"
    by (rule rule_R[where p = "[]"]) auto
  then show ?thesis
    unfolding equivalence_def by (rule Equality_Rules(2))
qed

proposition prop_5229:
  shows " (To 𝒬 To) =⇘o⇙ T⇘o⇙"
  and " (To 𝒬 Fo) =⇘o⇙ F⇘o⇙"
  and " (Fo 𝒬 To) =⇘o⇙ F⇘o⇙"
  and " (Fo 𝒬 Fo) =⇘o⇙ F⇘o⇙"
proof -
  show " (To 𝒬 To) =⇘o⇙ T⇘o⇙" and " (To 𝒬 Fo) =⇘o⇙ F⇘o⇙"
    using prop_5216 by blast+
next
  show " (Fo 𝒬 To) =⇘o⇙ F⇘o⇙" and " (Fo 𝒬 Fo) =⇘o⇙ F⇘o⇙"
    using false_in_conj_provability and true_wff and false_wff by simp_all
qed

subsection ‹Proposition 5230›

proposition prop_5230:
  shows " (To 𝒬 To) =⇘o⇙ T⇘o⇙"
  and " (To 𝒬 Fo) =⇘o⇙ F⇘o⇙"
  and " (Fo 𝒬 To) =⇘o⇙ F⇘o⇙"
  and " (Fo 𝒬 Fo) =⇘o⇙ T⇘o⇙"
proof -
  show " (To 𝒬 To) =⇘o⇙ T⇘o⇙" and " (To 𝒬 Fo) =⇘o⇙ F⇘o⇙"
    unfolding equivalence_def using prop_5218 by blast+
next
  show " (Fo 𝒬 Fo) =⇘o⇙ T⇘o⇙"
    unfolding equivalence_def by (rule Equality_Rules(2)[OF prop_5210[OF false_wff]])
next
  have "§1": " (Fo 𝒬 To) 𝒬 ((λ𝔵o⇙. (𝔵o𝒬 Fo)) · Fo 𝒬 (λ𝔵o⇙. (𝔵o𝒬 Fo)) · To)"
  proof -
    let  = "{(𝔥, oo)  λ𝔵o⇙. (𝔵o𝒬 Fo), (𝔵, o)  Fo, (𝔶, o)  To}"
      and ?A = "(𝔵o⇙ =⇘o𝔶o) 𝒬 (𝔥oo· 𝔵o𝒬 𝔥oo· 𝔶o)"
    have " ?A"
      by (fact axiom_is_derivable_from_no_hyps[OF axiom_2])
    moreover have "is_substitution "
      by auto
    moreover have "
      v  fmdom' . var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v ?A"
      by (code_simp, unfold atomize_conj[symmetric], simp, force)+ blast
    moreover have "  {$$}"
      by simp
    ultimately have " S  ?A"
      by (rule Sub)
    then show ?thesis
      by simp
  qed
  then have "§2": " (Fo 𝒬 To) 𝒬 ((Fo 𝒬 Fo) 𝒬 (To 𝒬 Fo))" (is " ?A2")
  proof -
    have "is_free_for A (𝔵, o) (𝔵o𝒬 Fo)" for A
      by code_simp blast
    have β_reduction: " (λ𝔵o⇙. (𝔵o𝒬 Fo)) · A =⇘o(A 𝒬 Fo)" if "A  wffs⇘o⇙" for A
      using
        prop_5207
        [
          OF that equivalence_wff[OF wffs_of_type_intros(1) false_wff]
          is_free_for A (𝔵, o) (𝔵o𝒬 Fo)
        ]
      by simp
    from "§1" and β_reduction[OF false_wff] have "
       (F⇘o⇙ =⇘o⇙ T⇘o⇙) 𝒬 ((Fo 𝒬 Fo) 𝒬 (λ𝔵o⇙. (𝔵o𝒬 Fo)) · To)"
      by (rule rule_R[where p = "[»,«,»]"]) force+
    from this and β_reduction[OF true_wff] show ?thesis
      by (rule rule_R[where p = "[»,»]"]) force+
  qed
  then have "§3": " (Fo 𝒬 To) 𝒬 Fo"
  proof -
    note r1 = rule_RR[OF disjI1] and r2 = rule_RR[OF disjI2]
    have "§31": " (Fo 𝒬 To) 𝒬 ((Fo 𝒬 Fo) 𝒬 Fo)" (is  ?A31)
      by (rule r1[OF prop_5218[OF false_wff], where p = "[»,»]" and C = ?A2]) (use "§2" in force+)
    have "§32": " (Fo 𝒬 To) 𝒬 (To 𝒬 Fo)" (is  ?A32)
      by (rule r2[OF prop_5210[OF false_wff], where p = "[»,«,»]" and C = ?A31]) (use "§31" in force+)
    show ?thesis
      by (rule r1[OF prop_5218[OF false_wff], where p = "[»]" and C = ?A32]) (use "§32" in force+)
  qed
  then have " (Fo 𝒬 To) 𝒬 ((Fo 𝒬 To) 𝒬 Fo)"
  proof -
    have "
      
        (λ𝔵o⇙. λ𝔶o⇙. (𝔵o𝒬 𝔵o𝒬 𝔶o)) · (Fo 𝒬 To)
        =⇘ooS {(𝔵, o)  Fo 𝒬 To} (λ𝔶o⇙. (𝔵o𝒬 𝔵o𝒬 𝔶o))"
      by (rule prop_5207) auto
    from "§3"[unfolded imp_op_def imp_fun_def] and this
    have " (λ𝔶o⇙. ((Fo 𝒬 To) 𝒬 (Fo 𝒬 To) 𝒬 𝔶o)) · Fo"
      by (rule rule_R[where p = "[«]"]) force+
    moreover have "
      
        (λ𝔶o⇙. ((Fo 𝒬 To) 𝒬 (Fo 𝒬 To) 𝒬 𝔶o)) · F⇘o⇙
        =⇘oS {(𝔶, o)  Fo} ((Fo 𝒬 To) 𝒬 (Fo 𝒬 To) 𝒬 𝔶o)"
      by (rule prop_5207) auto
    ultimately show ?thesis
      by (rule rule_R[where p = "[]"]) force+
  qed
  moreover have "§5": " 𝔵o𝒬 Fo 𝒬 Fo"
  proof -
    from prop_5229(2,4) have "
       S {(𝔵, o)  To} (𝔵o𝒬 Fo 𝒬 Fo)" and " S {(𝔵, o)  Fo} (𝔵o𝒬 Fo 𝒬 Fo)"
      by simp_all
    moreover have "𝔵o𝒬 Fo 𝒬 Fo  wffs⇘o⇙"
      by auto
    ultimately show ?thesis
      by (rule Cases)
  qed
  then have " (Fo 𝒬 To) 𝒬 Fo 𝒬 Fo"
  proof -
    let  = "{(𝔵, o)  Fo 𝒬 To}"
    have "is_substitution "
      by auto
    moreover have "v  fmdom' .
      var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v (𝔵o𝒬 Fo 𝒬 Fo)"
      by simp
    moreover have "  {$$}"
      by simp
    ultimately have " S  (𝔵o𝒬 Fo 𝒬 Fo)"
      by (rule Sub[OF  𝔵o𝒬 Fo 𝒬 Fo])
    then show ?thesis
      by simp
  qed
  ultimately show " (Fo 𝒬 To) =⇘o⇙ F⇘o⇙"
    unfolding equivalence_def by (rule Equality_Rules(3))
qed

subsection ‹Proposition 5231›

proposition prop_5231:
  shows " 𝒬 T⇘o⇙ =⇘o⇙ F⇘o⇙"
  and " 𝒬 F⇘o⇙ =⇘o⇙ T⇘o⇙"
  using prop_5230(3,4) unfolding neg_def and equivalence_def and equality_of_type_def .

subsection ‹Proposition 5232›

lemma disj_op_alt_def_provability:
  assumes "A  wffs⇘o⇙" and "B  wffs⇘o⇙"
  shows " A 𝒬 B =⇘o𝒬 (𝒬 A 𝒬 𝒬 B)"
proof -
  let ?C = "(λ𝔵o⇙. λ𝔶o⇙. 𝒬 (𝒬 𝔵o𝒬 𝒬 𝔶o)) · A · B"
  from assms have "?C  wffs⇘o⇙"
    by blast
  have "(𝒬 (𝒬 𝔵o𝒬 𝒬 𝔶o))  wffs⇘o⇙"
    by auto
  moreover obtain z where "(z, o)  {(𝔵, o), (𝔶, o)}" and "(z, o)  free_vars A"
    using free_vars_form_finiteness and fresh_var_existence
    by (metis Un_iff Un_insert_right free_vars_form.simps(1,3) inf_sup_aci(5) sup_bot_left)
  then have "(z, o)  free_vars (𝒬 (𝒬 𝔵o𝒬 𝒬 𝔶o))"
    by simp
  moreover have "is_free_for (zo) (𝔶, o) (𝒬 (𝒬 𝔵o𝒬 𝒬 𝔶o))"
    by (intro is_free_for_in_conj is_free_for_in_neg is_free_for_in_var)
  ultimately have "
     (λ𝔶o⇙. 𝒬 (𝒬 𝔵o𝒬 𝒬 𝔶o)) =⇘oo(λzo⇙. S {(𝔶, o)  zo} 𝒬 (𝒬 𝔵o𝒬 𝒬 𝔶o))"
    by (rule "α")
  then have " (λ𝔶o⇙. 𝒬 (𝒬 𝔵o𝒬 𝒬 𝔶o)) =⇘oo(λzo⇙. 𝒬 (𝒬 𝔵o𝒬 𝒬 zo))"
    by simp
  from prop_5200[OF ?C  wffs⇘o⇙›] and this have "
    
      (λ𝔵o⇙. λzo⇙. 𝒬 (𝒬 𝔵o𝒬 𝒬 zo)) · A · B
      =⇘o(λ𝔵o⇙. λ𝔶o⇙. 𝒬 (𝒬 𝔵o𝒬 𝒬 𝔶o)) · A · B"
    by (rule rule_R[where p = "[«,»,«,«,«]"]) force+
  moreover have "λzo⇙. 𝒬 (𝒬 𝔵o𝒬 𝒬 zo)  wffs⇘oo⇙"
    by blast
  have "
    
      (λ𝔵o⇙. λzo⇙. 𝒬 (𝒬 𝔵o𝒬 𝒬 zo)) · A
      =⇘ooS {(𝔵, o)  A} (λzo⇙. 𝒬 (𝒬 𝔵o𝒬 𝒬 zo))"
    by
      (rule prop_5207)
      (
        fact, blast, intro is_free_for_in_neg is_free_for_in_conj is_free_for_to_abs,
        (fastforce simp add: (z, o)  free_vars A)+
      )
  then have " (λ𝔵o⇙. λzo⇙. 𝒬 (𝒬 𝔵o𝒬 𝒬 zo)) · A =⇘oo(λzo⇙. 𝒬 (𝒬 A 𝒬 𝒬 zo))"
    using (z, o)  free_vars (𝒬 (𝒬 𝔵o𝒬 𝒬 𝔶o)) by simp
  ultimately have "
     (λzo⇙. 𝒬 (𝒬 A 𝒬 𝒬 zo)) · B =⇘o(λ𝔵o⇙. λ𝔶o⇙. 𝒬 (𝒬 𝔵o𝒬 𝒬 𝔶o)) · A · B"
    by (rule rule_R[where p = "[«,»,«]"]) force+
  moreover have " (λzo⇙. 𝒬 (𝒬 A 𝒬 𝒬 zo)) · B =⇘oS {(z, o)  B} (𝒬 (𝒬 A 𝒬 𝒬 zo))"
    by
      (rule prop_5207)
      (
        fact, blast intro: assms(1), intro is_free_for_in_neg is_free_for_in_conj,
        use (z, o)  free_vars A is_free_at_in_free_vars in fastforce+
      )
  moreover have "S {(z, o)  B} (𝒬 (𝒬 A 𝒬 𝒬 zo)) = 𝒬 (𝒬 A 𝒬 𝒬 B)"
    using free_var_singleton_substitution_neutrality[OF (z, o)  free_vars A] by simp
  ultimately have " (λ𝔵o⇙. λ𝔶o⇙. 𝒬 (𝒬 𝔵o𝒬 𝒬 𝔶o)) · A · B =⇘o𝒬 (𝒬 A 𝒬 𝒬 B)"
    using Equality_Rules(2,3) by metis
  then show ?thesis
    by simp
qed

context begin

private lemma prop_5232_aux:
  assumes " 𝒬 (A 𝒬 B) =⇘oC"
  and " 𝒬 A' =⇘oA" and " 𝒬 B' =⇘oB"
  shows " A' 𝒬 B' =⇘oC"
proof -
  let ?D = "𝒬 (A 𝒬 B) =⇘oC"
  from assms(2) have " 𝒬 (𝒬 A' 𝒬 B) =⇘oC" (is  ?A1)
    by (rule rule_RR[OF disjI2, where p = "[«,»,»,«,»]" and C = ?D]) (use assms(1) in force+)
  from assms(3) have " 𝒬 (𝒬 A' 𝒬 𝒬 B') =⇘oC"
    by (rule rule_RR[OF disjI2, where p = "[«,»,»,»]" and C = ?A1]) (use  ?A1 in force+)
  moreover from assms(2,3) have "A'  wffs⇘o⇙" and "B'  wffs⇘o⇙"
    using hyp_derivable_form_is_wffso by (blast dest: wffs_from_equality wffs_from_neg)+
  then have " A' 𝒬 B' =⇘o𝒬 (𝒬 A' 𝒬 𝒬 B')"
    by (rule disj_op_alt_def_provability)
  ultimately show ?thesis
    using prop_5201_3 by blast
qed

proposition prop_5232:
  shows " (To 𝒬 To) =⇘o⇙ T⇘o⇙"
  and " (To 𝒬 Fo) =⇘o⇙ T⇘o⇙"
  and " (Fo 𝒬 To) =⇘o⇙ T⇘o⇙"
  and " (Fo 𝒬 Fo) =⇘o⇙ F⇘o⇙"
proof -
  from prop_5231(2) have " 𝒬 F⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A) .
  from prop_5229(4) have " 𝒬 (Fo 𝒬 Fo) =⇘o⇙ T⇘o⇙"
    by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A]) (use  ?A in force+)
  from prop_5232_aux[OF this prop_5231(1) prop_5231(1)] show " (To 𝒬 To) =⇘o⇙ T⇘o⇙" .
  from prop_5229(3) have " 𝒬 (Fo 𝒬 To) =⇘o⇙ T⇘o⇙"
    by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A]) (use  ?A in force+)
  from prop_5232_aux[OF this prop_5231(1) prop_5231(2)] show " (To 𝒬 Fo) =⇘o⇙ T⇘o⇙" .
  from prop_5229(2) have " 𝒬 (To 𝒬 Fo) =⇘o⇙ T⇘o⇙"
    by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A]) (use  ?A in force+)
  from prop_5232_aux[OF this prop_5231(2) prop_5231(1)] show " (Fo 𝒬 To) =⇘o⇙ T⇘o⇙" .
next
  from prop_5231(1) have " 𝒬 T⇘o⇙ =⇘o⇙ F⇘o⇙" (is  ?A) .
  from prop_5229(1) have " 𝒬 (To 𝒬 To) =⇘o⇙ F⇘o⇙"
    by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A]) (use  ?A in force+)
  from prop_5232_aux[OF this prop_5231(2) prop_5231(2)] show " (Fo 𝒬 Fo) =⇘o⇙ F⇘o⇙" .
qed

end

subsection ‹Proposition 5233›

context begin

private lemma lem_prop_5233_no_free_vars:
  assumes "A  pwffs" and "free_vars A = {}"
  shows "(φ. is_tv_assignment φ  𝒱B φ A = T)   A =⇘o⇙ T⇘o⇙" (is "?AT  _")
  and "(φ. is_tv_assignment φ  𝒱B φ A = F)   A =⇘o⇙ F⇘o⇙" (is "?AF  _")
proof -
  from assms have "(?AT   A =⇘o⇙ T⇘o⇙)  (?AF   A =⇘o⇙ F⇘o⇙)"
  proof induction
    case T_pwff
    have " T⇘o⇙ =⇘o⇙ T⇘o⇙"
      by (rule prop_5200[OF true_wff])
    moreover have "φ. is_tv_assignment φ  𝒱B φ To = T"
      using 𝒱B_T by blast
    then have "¬ (φ. is_tv_assignment φ  𝒱B φ To = F)"
      by (auto simp: inj_eq)
    ultimately show ?case
      by blast
  next
    case F_pwff
    have " F⇘o⇙ =⇘o⇙ F⇘o⇙"
      by (rule prop_5200[OF false_wff])
    moreover have "φ. is_tv_assignment φ  𝒱B φ Fo = F"
      using 𝒱B_F by blast
    then have "¬ (φ. is_tv_assignment φ  𝒱B φ Fo = T)"
      by (auto simp: inj_eq)
    ultimately show ?case
      by blast
  next
    case (var_pwff p) ― ‹impossible case›
    then show ?case
      by simp
  next
    case (neg_pwff B)
    from neg_pwff.hyps have "𝒬 B  pwffs" and "free_vars B = {}"
      using neg_pwff.prems by (force, auto elim: free_vars_form.elims)
    consider
      (a) "φ. is_tv_assignment φ  𝒱B φ B = T"
    | (b) "φ. is_tv_assignment φ  𝒱B φ B = F"
      using closed_pwff_denotation_uniqueness[OF neg_pwff.hyps free_vars B = {}]
      and neg_pwff.hyps[THEN 𝒱B_graph_denotation_is_truth_value[OF 𝒱B_graph_𝒱B]]
      by (auto dest: tv_cases) metis
    then show ?case
    proof cases
      case a
      with free_vars B = {} have " T⇘o⇙ =⇘oB"
        using neg_pwff.IH and Equality_Rules(2) by blast
      from prop_5231(1)[unfolded neg_def, folded equality_of_type_def] and this
      have " 𝒬 B =⇘o⇙ F⇘o⇙"
        unfolding neg_def[folded equality_of_type_def] by (rule rule_R[where p = "[«,»,»]"]) force+
      moreover from a have "φ. is_tv_assignment φ  𝒱B φ (𝒬 B) = F"
        using 𝒱B_neg[OF neg_pwff.hyps] by simp
      ultimately show ?thesis
        by (auto simp: inj_eq)
    next
      case b
      with free_vars B = {} have " F⇘o⇙ =⇘oB"
        using neg_pwff.IH and Equality_Rules(2) by blast
      then have " 𝒬 B =⇘o⇙ T⇘o⇙"
        unfolding neg_def[folded equality_of_type_def]
        using rule_T(2)[OF hyp_derivable_form_is_wffso] by blast
      moreover from b have "φ. is_tv_assignment φ  𝒱B φ (𝒬 B) = T"
        using 𝒱B_neg[OF neg_pwff.hyps] by simp
      ultimately show ?thesis
        by (auto simp: inj_eq)
    qed
  next
    case (conj_pwff B C)
    from conj_pwff.prems have "free_vars B = {}" and "free_vars C = {}"
      by simp_all
    with conj_pwff.hyps obtain b and b'
      where B_den: "φ. is_tv_assignment φ  𝒱B φ B = b"
      and C_den: "φ. is_tv_assignment φ  𝒱B φ C = b'"
      using closed_pwff_denotation_uniqueness by metis
    then have "b  elts 𝔹" and "b'  elts 𝔹"
      using closed_pwff_denotation_uniqueness[OF conj_pwff.hyps(1) free_vars B = {}]
      and closed_pwff_denotation_uniqueness[OF conj_pwff.hyps(2) free_vars C = {}]
      and conj_pwff.hyps[THEN 𝒱B_graph_denotation_is_truth_value[OF 𝒱B_graph_𝒱B]]
      by force+
    with conj_pwff.hyps consider
      (a) "b = T" and "b' = T"
    | (b) "b = T" and "b' = F"
    | (c) "b = F" and "b' = T"
    | (d) "b = F" and "b' = F"
      by auto
    then show ?case
    proof cases
      case a
      from prop_5229(1) have " To 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A1) .
      from B_den[unfolded a(1)] and free_vars B = {} have " B =⇘o⇙ T⇘o⇙"
        using conj_pwff.IH(1) by simp
      then have " B 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙"  (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded a(2)] and free_vars C = {} have " C =⇘o⇙ T⇘o⇙"
        using conj_pwff.IH(2) by simp
      then have " B 𝒬 C =⇘o⇙ T⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = T)   B 𝒬 C =⇘o⇙ T⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  F"
        using 𝒱B_conj[OF conj_pwff.hyps] and B_den[unfolded a(1)] and C_den[unfolded a(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    next
      case b
      from prop_5229(2) have " To 𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙" (is  ?A1) .
      from B_den[unfolded b(1)] and free_vars B = {} have " B =⇘o⇙ T⇘o⇙"
        using conj_pwff.IH(1) by simp
      then have " B 𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙"  (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded b(2)] and free_vars C = {} have " C =⇘o⇙ F⇘o⇙"
        using conj_pwff.IH(2) by simp
      then have " B 𝒬 C =⇘o⇙ F⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = F)   B 𝒬 C =⇘o⇙ F⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  T"
        using 𝒱B_conj[OF conj_pwff.hyps] and B_den[unfolded b(1)] and C_den[unfolded b(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    next
      case c
      from prop_5229(3) have " Fo 𝒬 T⇘o⇙ =⇘o⇙ F⇘o⇙" (is  ?A1) .
      from B_den[unfolded c(1)] and free_vars B = {} have " B =⇘o⇙ F⇘o⇙"
        using conj_pwff.IH(1) by simp
      then have " B 𝒬 T⇘o⇙ =⇘o⇙ F⇘o⇙"  (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded c(2)] and free_vars C = {} have " C =⇘o⇙ T⇘o⇙"
        using conj_pwff.IH(2) by simp
      then have " B 𝒬 C =⇘o⇙ F⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = F)   B 𝒬 C =⇘o⇙ F⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  T"
        using 𝒱B_conj[OF conj_pwff.hyps] and B_den[unfolded c(1)] and C_den[unfolded c(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    next
      case d
      from prop_5229(4) have " Fo 𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙" (is  ?A1) .
      from B_den[unfolded d(1)] and free_vars B = {} have " B =⇘o⇙ F⇘o⇙"
        using conj_pwff.IH(1) by simp
      then have " B 𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙"  (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded d(2)] and free_vars C = {} have " C =⇘o⇙ F⇘o⇙"
        using conj_pwff.IH(2) by simp
      then have " B 𝒬 C =⇘o⇙ F⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = F)   B 𝒬 C =⇘o⇙ F⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  T"
        using 𝒱B_conj[OF conj_pwff.hyps] and B_den[unfolded d(1)] and C_den[unfolded d(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    qed
  next
    case (disj_pwff B C)
    from disj_pwff.prems have "free_vars B = {}" and "free_vars C = {}"
      by simp_all
    with disj_pwff.hyps obtain b and b'
      where B_den: "φ. is_tv_assignment φ  𝒱B φ B = b"
      and C_den: "φ. is_tv_assignment φ  𝒱B φ C = b'"
      using closed_pwff_denotation_uniqueness by metis
    then have "b  elts 𝔹" and "b'  elts 𝔹"
      using closed_pwff_denotation_uniqueness[OF disj_pwff.hyps(1) free_vars B = {}]
      and closed_pwff_denotation_uniqueness[OF disj_pwff.hyps(2) free_vars C = {}]
      and disj_pwff.hyps[THEN 𝒱B_graph_denotation_is_truth_value[OF 𝒱B_graph_𝒱B]]
      by force+
    with disj_pwff.hyps consider
      (a) "b = T" and "b' = T"
    | (b) "b = T" and "b' = F"
    | (c) "b = F" and "b' = T"
    | (d) "b = F" and "b' = F"
      by auto
    then show ?case
    proof cases
      case a
      from prop_5232(1) have " To 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A1) .
      from B_den[unfolded a(1)] and free_vars B = {} have " B =⇘o⇙ T⇘o⇙"
        using disj_pwff.IH(1) by simp
      then have " B 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded a(2)] and free_vars C = {} have " C =⇘o⇙ T⇘o⇙"
        using disj_pwff.IH(2) by simp
      then have " B 𝒬 C =⇘o⇙ T⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = T)   B 𝒬 C =⇘o⇙ T⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  F"
        using 𝒱B_disj[OF disj_pwff.hyps] and B_den[unfolded a(1)] and C_den[unfolded a(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    next
      case b
      from prop_5232(2) have " To 𝒬 F⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A1) .
      from B_den[unfolded b(1)] and free_vars B = {} have " B =⇘o⇙ T⇘o⇙"
        using disj_pwff.IH(1) by simp
      then have " B 𝒬 F⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded b(2)] and free_vars C = {} have " C =⇘o⇙ F⇘o⇙"
        using disj_pwff.IH(2) by simp
      then have " B 𝒬 C =⇘o⇙ T⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = T)   B 𝒬 C =⇘o⇙ T⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  F"
        using 𝒱B_disj[OF disj_pwff.hyps] and B_den[unfolded b(1)] and C_den[unfolded b(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    next
      case c
      from prop_5232(3) have " Fo 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A1) .
      from B_den[unfolded c(1)] and free_vars B = {} have " B =⇘o⇙ F⇘o⇙"
        using disj_pwff.IH(1) by simp
      then have " B 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙"  (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded c(2)] and free_vars C = {} have " C =⇘o⇙ T⇘o⇙"
        using disj_pwff.IH(2) by simp
      then have " B 𝒬 C =⇘o⇙ T⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = T)   B 𝒬 C =⇘o⇙ T⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  F"
        using 𝒱B_disj[OF disj_pwff.hyps] and B_den[unfolded c(1)] and C_den[unfolded c(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    next
      case d
      from prop_5232(4) have " Fo 𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙" (is  ?A1) .
      from B_den[unfolded d(1)] and free_vars B = {} have " B =⇘o⇙ F⇘o⇙"
        using disj_pwff.IH(1) by simp
      then have " B 𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙" (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded d(2)] and free_vars C = {} have " C =⇘o⇙ F⇘o⇙"
        using disj_pwff.IH(2) by simp
      then have " B 𝒬 C =⇘o⇙ F⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = T)   B 𝒬 C =⇘o⇙ F⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  T"
        using 𝒱B_disj[OF disj_pwff.hyps] and B_den[unfolded d(1)] and C_den[unfolded d(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        using  B 𝒬 C =⇘o⇙ F⇘o⇙› by auto
    qed
  next
    case (imp_pwff B C)
    from imp_pwff.prems have "free_vars B = {}" and "free_vars C = {}"
      by simp_all
    with imp_pwff.hyps obtain b and b'
      where B_den: "φ. is_tv_assignment φ  𝒱B φ B = b"
      and C_den: "φ. is_tv_assignment φ  𝒱B φ C = b'"
      using closed_pwff_denotation_uniqueness by metis
    then have "b  elts 𝔹" and "b'  elts 𝔹"
      using closed_pwff_denotation_uniqueness[OF imp_pwff.hyps(1) free_vars B = {}]
      and closed_pwff_denotation_uniqueness[OF imp_pwff.hyps(2) free_vars C = {}]
      and imp_pwff.hyps[THEN 𝒱B_graph_denotation_is_truth_value[OF 𝒱B_graph_𝒱B]]
      by force+
    with imp_pwff.hyps consider
      (a) "b = T" and "b' = T"
    | (b) "b = T" and "b' = F"
    | (c) "b = F" and "b' = T"
    | (d) "b = F" and "b' = F"
      by auto
    then show ?case
    proof cases
      case a
      from prop_5228(1) have " To 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A1) .
      from B_den[unfolded a(1)] and free_vars B = {} have " B =⇘o⇙ T⇘o⇙"
        using imp_pwff.IH(1) by simp
      then have " B 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded a(2)] and free_vars C = {} have " C =⇘o⇙ T⇘o⇙"
        using imp_pwff.IH(2) by simp
      then have " B 𝒬 C =⇘o⇙ T⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = T)   B 𝒬 C =⇘o⇙ T⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  F"
        using 𝒱B_imp[OF imp_pwff.hyps] and B_den[unfolded a(1)] and C_den[unfolded a(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    next
      case b
      from prop_5228(2) have " To 𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙" (is  ?A1) .
      from B_den[unfolded b(1)] and free_vars B = {} have " B =⇘o⇙ T⇘o⇙"
        using imp_pwff.IH(1) by simp
      then have " B 𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙" (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded b(2)] and free_vars C = {} have " C =⇘o⇙ F⇘o⇙"
        using imp_pwff.IH(2) by simp
      then have " B 𝒬 C =⇘o⇙ F⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = F)   B 𝒬 C =⇘o⇙ F⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  T"
        using 𝒱B_imp[OF imp_pwff.hyps] and B_den[unfolded b(1)] and C_den[unfolded b(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    next
      case c
      from prop_5228(3) have " Fo 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A1) .
      from B_den[unfolded c(1)] and free_vars B = {} have " B =⇘o⇙ F⇘o⇙"
        using imp_pwff.IH(1) by simp
      then have " B 𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded c(2)] and free_vars C = {} have " C =⇘o⇙ T⇘o⇙"
        using imp_pwff.IH(2) by simp
      then have " B 𝒬 C =⇘o⇙ T⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = T)   B 𝒬 C =⇘o⇙ T⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  F"
        using 𝒱B_imp[OF imp_pwff.hyps] and B_den[unfolded c(1)] and C_den[unfolded c(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    next
      case d
      from prop_5228(4) have " Fo 𝒬 F⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A1) .
      from B_den[unfolded d(1)] and free_vars B = {} have " B =⇘o⇙ F⇘o⇙"
        using imp_pwff.IH(1) by simp
      then have " B 𝒬 F⇘o⇙ =⇘o⇙ T⇘o⇙" (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded d(2)] and free_vars C = {} have " C =⇘o⇙ F⇘o⇙"
        using imp_pwff.IH(2) by simp
      then have " B 𝒬 C =⇘o⇙ T⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = T)   B 𝒬 C =⇘o⇙ T⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  F"
        using 𝒱B_imp[OF imp_pwff.hyps] and B_den[unfolded d(1)] and C_den[unfolded d(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    qed
  next
    case (eqv_pwff B C)
    from eqv_pwff.prems have "free_vars B = {}" and "free_vars C = {}"
      by simp_all
    with eqv_pwff.hyps obtain b and b'
      where B_den: "φ. is_tv_assignment φ  𝒱B φ B = b"
      and C_den: "φ. is_tv_assignment φ  𝒱B φ C = b'"
      using closed_pwff_denotation_uniqueness by metis
    then have "b  elts 𝔹" and "b'  elts 𝔹"
      using closed_pwff_denotation_uniqueness[OF eqv_pwff.hyps(1) free_vars B = {}]
      and closed_pwff_denotation_uniqueness[OF eqv_pwff.hyps(2) free_vars C = {}]
      and eqv_pwff.hyps[THEN 𝒱B_graph_denotation_is_truth_value[OF 𝒱B_graph_𝒱B]]
      by force+
    with eqv_pwff.hyps consider
      (a) "b = T" and "b' = T"
    | (b) "b = T" and "b' = F"
    | (c) "b = F" and "b' = T"
    | (d) "b = F" and "b' = F"
      by auto
    then show ?case
    proof cases
      case a
      from prop_5230(1) have " (To 𝒬 To) =⇘o⇙ T⇘o⇙" (is  ?A1) .
      from B_den[unfolded a(1)] and free_vars B = {} have " B =⇘o⇙ T⇘o⇙"
        using eqv_pwff.IH(1) by simp
      then have " (B 𝒬 To) =⇘o⇙ T⇘o⇙" (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded a(2)] and free_vars C = {} have " C =⇘o⇙ T⇘o⇙"
        using eqv_pwff.IH(2) by simp
      then have " (B 𝒬 C) =⇘o⇙ T⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = T)   (B 𝒬 C) =⇘o⇙ T⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  F"
        using 𝒱B_eqv[OF eqv_pwff.hyps] and B_den[unfolded a(1)] and C_den[unfolded a(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    next
      case b
      from prop_5230(2) have " (To 𝒬 Fo) =⇘o⇙ F⇘o⇙" (is  ?A1) .
      from B_den[unfolded b(1)] and free_vars B = {} have " B =⇘o⇙ T⇘o⇙"
        using eqv_pwff.IH(1) by simp
      then have " (B 𝒬 Fo) =⇘o⇙ F⇘o⇙" (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded b(2)] and free_vars C = {} have " C =⇘o⇙ F⇘o⇙"
        using eqv_pwff.IH(2) by simp
      then have " (B 𝒬 C) =⇘o⇙ F⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = F)   (B 𝒬 C) =⇘o⇙ F⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  T"
        using 𝒱B_eqv[OF eqv_pwff.hyps] and B_den[unfolded b(1)] and C_den[unfolded b(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    next
      case c
      from prop_5230(3) have " (Fo 𝒬 To) =⇘o⇙ F⇘o⇙" (is  ?A1) .
      from B_den[unfolded c(1)] and free_vars B = {} have " B =⇘o⇙ F⇘o⇙"
        using eqv_pwff.IH(1) by simp
      then have " (B 𝒬 To) =⇘o⇙ F⇘o⇙" (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded c(2)] and free_vars C = {} have " C =⇘o⇙ T⇘o⇙"
        using eqv_pwff.IH(2) by simp
      then have " (B 𝒬 C) =⇘o⇙ F⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = F)   (B 𝒬 C) =⇘o⇙ F⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  T"
        using 𝒱B_eqv[OF eqv_pwff.hyps] and B_den[unfolded c(1)] and C_den[unfolded c(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    next
      case d
      from prop_5230(4) have " (Fo 𝒬 Fo) =⇘o⇙ T⇘o⇙" (is  ?A1) .
      from B_den[unfolded d(1)] and free_vars B = {} have " B =⇘o⇙ F⇘o⇙"
        using eqv_pwff.IH(1) by simp
      then have " (B 𝒬 Fo) =⇘o⇙ T⇘o⇙" (is  ?A2)
        by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A1]) (use  ?A1 in force+)
      from C_den[unfolded d(2)] and free_vars C = {} have " C =⇘o⇙ F⇘o⇙"
        using eqv_pwff.IH(2) by simp
      then have " (B 𝒬 C) =⇘o⇙ T⇘o⇙"
        by (rule rule_RR[OF disjI2, where p = "[«,»,»]" and C = ?A2]) (use  ?A2 in force+)
      then have "(φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C) = T)   (B 𝒬 C) =⇘o⇙ T⇘o⇙"
        by blast
      moreover have "φ. is_tv_assignment φ  𝒱B φ (B 𝒬 C)  F"
        using 𝒱B_eqv[OF eqv_pwff.hyps] and B_den[unfolded d(1)] and C_den[unfolded d(2)]
        by (auto simp: inj_eq)
      ultimately show ?thesis
        by force
    qed
  qed
  then show "?AT   A =⇘o⇙ T⇘o⇙" and "?AF   A =⇘o⇙ F⇘o⇙"
    by blast+
qed

proposition prop_5233:
  assumes "is_tautology A"
  shows " A"
proof -
  have "finite (free_vars A)"
    using free_vars_form_finiteness by presburger
  from this and assms show ?thesis
  proof (induction "free_vars A" arbitrary: A)
    case empty
    from empty(2) have "A  pwffs" and "φ. is_tv_assignment φ  𝒱B φ A = T"
      unfolding is_tautology_def by blast+
    with empty(1) have " A =⇘o⇙ T⇘o⇙"
      using lem_prop_5233_no_free_vars(1) by (simp only:)
    then show ?case
      using rule_T(2)[OF tautology_is_wffo[OF empty(2)]] by (simp only:)
  next
    case (insert v F)
    from insert.prems have "A  pwffs"
      by blast
    with insert.hyps(4) obtain p where "v = (p, o)"
      using pwffs_free_vars_are_propositional by blast
    from v = (p, o) and insert.hyps(4) have "
      is_tautology (S {(p, o)  To} A)" and "is_tautology (S {(p, o)  Fo} A)"
      using pwff_substitution_tautology_preservation [OF insert.prems] by blast+
    moreover from insert.hyps(2,4) and v = (p, o) and A  pwffs
    have "free_vars (S {(p, o)  To} A) = F" and "free_vars (S {(p, o)  Fo} A) = F"
      using closed_pwff_substitution_free_vars and T_pwff and F_pwff and T_fv and F_fv
      by (metis Diff_insert_absorb insertI1)+
    ultimately have " S {(p, o)  To} A" and " S {(p, o)  Fo} A"
      using insert.hyps(3) by (simp_all only:)
    from this and tautology_is_wffo[OF insert.prems] show ?case
      by (rule Cases)
  qed
qed

end

subsection ‹Proposition 5234 (Rule P)›

text ‹
  According to the proof in cite"andrews:2002", if $[A^1 \wedge \dots \wedge A^n] \supset B$ is
  tautologous, then clearly $A^1 \supset (\dots (A^n \supset B) \dots)$ is also tautologous.
  Since this is not clear to us, we prove instead the version of Rule P found in cite"andrews:1965":
›

proposition tautologous_horn_clause_is_hyp_derivable:
  assumes "is_hyps " and "is_hyps 𝒢"
  and "A  𝒢.   A"
  and "lset hs = 𝒢"
  and "is_tautologous (hs 𝒬 B)"
  shows "  B"
proof -
  from assms(5) obtain θ and C
    where "is_tautology C"
    and "is_substitution θ"
    and "(x, α)  fmdom' θ. α = o"
    and "hs 𝒬 B = S θ C"
    by blast
  then have " hs 𝒬 B"
  proof (cases "θ = {$$}")
    case True
    with hs 𝒬 B = S θ C have "C = hs 𝒬 B"
      using empty_substitution_neutrality by simp
    with hs 𝒬 B = S θ C and is_tautology C show ?thesis
      using prop_5233 by (simp only:)
  next
    case False
    from is_tautology C have " C" and "C  pwffs"
      using prop_5233 by simp_all
    moreover have "
      v  fmdom' θ. var_name v  free_var_names ({}::form set)  is_free_for (θ $$! v) v C"
    proof
      fix v
      assume "v  fmdom' θ"
      then show "var_name v  free_var_names ({}::form set)  is_free_for (θ $$! v) v C"
      proof (cases "v  free_vars C")
        case True
        with C  pwffs show ?thesis
          using is_free_for_in_pwff by simp
      next
        case False
        then have "is_free_for (θ $$! v) v C"
          unfolding is_free_for_def using is_free_at_in_free_vars by blast
        then show ?thesis
          by simp
      qed
    qed
    ultimately show ?thesis
      using False and is_substitution θ and Sub
      by (simp add: hs 𝒬 B = S θ C[unfolded generalized_imp_op_def])
  qed
  from this and assms(1) have "  hs 𝒬 B"
    by (rule derivability_implies_hyp_derivability)
  with assms(3,4) show ?thesis
    using generalized_modus_ponens by blast
qed

corollary tautologous_is_hyp_derivable:
  assumes "is_hyps "
  and "is_tautologous B"
  shows "  B"
  using assms and tautologous_horn_clause_is_hyp_derivable[where 𝒢 = "{}"] by simp

lemmas prop_5234 = tautologous_horn_clause_is_hyp_derivable tautologous_is_hyp_derivable

lemmas rule_P = prop_5234 (* synonym *)

subsection ‹Proposition 5235›

proposition prop_5235:
  assumes "A  pwffs" and "B  pwffs"
  and "(x, α)  free_vars A"
  shows " xα⇙. (A 𝒬 B) 𝒬 (A 𝒬 xα⇙. B)"
proof -
  have "§1": " xα⇙. (To 𝒬 B) 𝒬 (To 𝒬 xα⇙. B)"
  proof (intro rule_P(2))
    show "is_tautologous (xα⇙. (To 𝒬 B) 𝒬 To 𝒬 xα⇙. B)"
    proof -
      let  = "{(𝔵, o)  xα⇙. (To 𝒬 B), (𝔶, o)  xα⇙. B}" and ?C = "𝔵o𝒬 (To 𝒬 (𝔶o))"
      have "is_tautology ?C"
        using 𝒱B_simps by simp
      moreover from assms(2) have "is_pwff_substitution "
        using pwffs_subset_of_wffso by fastforce
      moreover have "xα⇙. (To 𝒬 B) 𝒬 To 𝒬 xα⇙. B = S  ?C"
        by simp
      ultimately show ?thesis
        by blast
    qed
  qed simp
  have "§2": " xα⇙. B 𝒬 (Fo 𝒬 xα⇙. B)"
  proof (intro rule_P(2))
    show "is_tautologous (xα⇙. B 𝒬 (Fo 𝒬 xα⇙. B))"
    proof -
      let  = "{(𝔵, o)  xα⇙. B}" and ?C = "𝔵o𝒬 (Fo 𝒬 (𝔵o))"
      have "is_tautology (𝔵o𝒬 (Fo 𝒬 (𝔵o)))" (is is_tautology ?C)
        using 𝒱B_simps by simp
      moreover from assms(2) have "is_pwff_substitution "
        using pwffs_subset_of_wffso by auto
      moreover have "xα⇙. B 𝒬 (Fo 𝒬 xα⇙. B) = S  ?C"
        by simp
      ultimately show ?thesis
        by blast
    qed
  qed simp
  have "§3": " B 𝒬 (Fo 𝒬 B)"
  proof (intro rule_P(2))
    show "is_tautologous (B 𝒬 (Fo 𝒬 B))"
    proof -
      let  = "{(𝔵, o)  B}" and ?C = "𝔵o𝒬 (Fo 𝒬 (𝔵o))"
      have "is_tautology ?C"
        using 𝒱B_simps by simp
      moreover from assms(2) have "is_pwff_substitution "
        using pwffs_subset_of_wffso by auto
      moreover have "B 𝒬 (Fo 𝒬 B) = S  ?C"
        by simp
      ultimately show ?thesis
        by blast
    qed
  qed simp
  from "§2" and "§3"[unfolded equivalence_def] have "§4":
    " xα⇙. (Fo 𝒬 B) 𝒬 (Fo 𝒬 xα⇙. B)"
    by (rule rule_R[where p = "[«,»,»,«]"]) force+
  obtain p where "(p, o)  vars (xα⇙. (A 𝒬 B) 𝒬 (A 𝒬 xα⇙. B))"
    by (meson fresh_var_existence vars_form_finiteness)
  then have "(p, o)  (x, α)" and "(p, o)  vars A" and "(p, o)  vars B"
    by simp_all
  from (p, o)  vars B have sub: "S {(p, o)  C} B = B" for C
    using free_var_singleton_substitution_neutrality and free_vars_in_all_vars by blast
  have "§5": " xα⇙. (po𝒬 B) 𝒬 (po𝒬 xα⇙. B)" (is  ?C)
  proof -
    from sub and "§1" have " S {(p, o)  To} ?C"
      using (p, o)  (x, α) by auto
    moreover from sub and "§4" have " S {(p, o)  Fo} ?C"
      using (p, o)  (x, α) by auto
    moreover from assms(2) have "?C  wffs⇘o⇙"
      using pwffs_subset_of_wffso by auto
    ultimately show ?thesis
      by (rule Cases)
  qed
  then show ?thesis
  proof -
    let  = "{(p, o)  A}"
    from assms(1) have "is_substitution "
      using pwffs_subset_of_wffso by auto
    moreover have "
      v  fmdom' . var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v ?C"
    proof
      fix v
      assume "v  fmdom' "
      then have "v = (p, o)"
        by simp
      with assms(3) and (p, o)  vars B have "is_free_for ( $$! v) v ?C"
        using occurs_in_vars
        by (intro is_free_for_in_imp is_free_for_in_forall is_free_for_in_disj) auto
      moreover have "var_name v  free_var_names ({}::form set)"
        by simp
      ultimately show "var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v ?C"
        unfolding v = (p, o) by blast
    qed
    moreover have "  {$$}"
      by simp
    ultimately have " S  ?C"
      by (rule Sub[OF "§5"])
    moreover have "S  ?C = xα⇙. (A 𝒬 B) 𝒬 (A 𝒬 xα⇙. B)"
      using (p, o)  (x, α) and sub[of A] by simp fast
    ultimately show ?thesis
      by (simp only:)
  qed
qed

subsection ‹Proposition 5237 ($\supset \forall$ Rule)›

text ‹
  The proof in cite"andrews:2002" uses the pseudo-rule Q and the axiom 5 of ℱ›. Therefore, we
  prove such axiom, following the proof of Theorem 143 in cite"andrews:1965":
›

context begin

private lemma prop_5237_aux:
  assumes "A  wffs⇘o⇙" and "B  wffs⇘o⇙"
  and "(x, α)  free_vars A"
  shows " xα⇙. (A 𝒬 B) 𝒬 (A 𝒬 (xα⇙. B))"
proof -
  have "is_tautology (𝔵o𝒬 (To 𝒬 𝔵o))" (is is_tautology ?C1)
    using 𝒱B_simps by simp
  have "is_tautology (𝔵o𝒬 (𝔵o𝒬 (Fo 𝒬 𝔶o)))" (is is_tautology ?C2)
    using 𝒱B_simps by simp
  have "§1": " xα⇙. B 𝒬 (To 𝒬 xα⇙. B)"
  proof (intro rule_P(2))
    show "is_tautologous (xα⇙. B 𝒬 (To 𝒬 xα⇙. B))"
    proof -
      let  = "{(𝔵, o)  xα⇙. B}"
      from assms(2) have "is_pwff_substitution "
        using pwffs_subset_of_wffso by auto
      moreover have "xα⇙. B 𝒬 (To 𝒬 xα⇙. B) = S  ?C1"
        by simp
      ultimately show ?thesis
        using is_tautology ?C1 by blast
    qed
  qed simp
  have "§2": " B 𝒬 (To 𝒬 B)"
  proof (intro rule_P(2))
    show "is_tautologous (B 𝒬 To 𝒬 B)"
    proof -
      let  = "{(𝔵, o)  B}"
      from assms(2) have "is_pwff_substitution "
        using pwffs_subset_of_wffso by auto
      moreover have "B 𝒬 To 𝒬 B = S  ?C1"
        by simp
      ultimately show ?thesis
        using is_tautology ?C1 by blast
    qed
  qed simp
  have " To"
    by (fact true_is_derivable)
  then have "§3": " xα⇙. T⇘o⇙"
    using Gen by simp
  have "§4": " xα⇙. T⇘o⇙ 𝒬 (Fo 𝒬 xα⇙. B)"
  proof (intro rule_P(1)[where 𝒢 = "{xα⇙. T⇘o⇙}"])
    show "is_tautologous ([xα⇙. T⇘o⇙] 𝒬 (xα⇙. T⇘o⇙ 𝒬 (Fo 𝒬 xα⇙. B)))"
    proof -
      let  = "{(𝔵, o)  xα⇙. T⇘o⇙, (𝔶, o)  xα⇙. B}"
      from assms(2) have "is_pwff_substitution "
        using pwffs_subset_of_wffso by auto
      moreover have "[xα⇙. T⇘o⇙] 𝒬 (xα⇙. T⇘o⇙ 𝒬 (Fo 𝒬 xα⇙. B)) = S  ?C2"
        by simp
      ultimately show ?thesis
        using is_tautology ?C2 by blast
    qed
  qed (use "§3" in fastforce)+
  have "§5": " To 𝒬 (Fo 𝒬 B)"
  proof (intro rule_P(2))
    show "is_tautologous (To 𝒬 (Fo 𝒬 B))"
    proof -
      let  = "{(𝔵, o)  B}" and ?C = "To 𝒬 (Fo 𝒬 𝔵o)"
      have "is_tautology ?C"
        using 𝒱B_simps by simp
      moreover from assms(2) have "is_pwff_substitution "
        using pwffs_subset_of_wffso by auto
      moreover have "To 𝒬 (Fo 𝒬 B) = S  ?C"
        by simp
      ultimately show ?thesis
        by blast
    qed
  qed simp
  from "§4" and "§5" have "§6": " xα⇙. (Fo 𝒬 B) 𝒬 (Fo 𝒬 xα⇙. B)"
    unfolding equivalence_def by (rule rule_R[where p = "[«,»,»,«]"]) force+
  from "§1" and "§2" have "§7": " xα⇙. (To 𝒬 B) 𝒬 (To 𝒬 xα⇙. B)"
    unfolding equivalence_def by (rule rule_R[where p = "[«,»,»,«]"]) force+
  obtain p where "(p, o)  vars B" and "p  x"
    using fresh_var_existence and vars_form_finiteness by (metis finite_insert insert_iff)
  from (p, o)  vars B have sub: "S {(p, o)  C} B = B" for C
    using free_var_singleton_substitution_neutrality and free_vars_in_all_vars by blast
  have "§8": " xα⇙. (po𝒬 B) 𝒬 (po𝒬 xα⇙. B)" (is  ?C3)
  proof -
    from sub and "§7" have " S {(p, o)  To} ?C3"
      using p  x by auto
    moreover from sub and "§6" have " S {(p, o)  Fo} ?C3"
      using p  x by auto
    moreover from assms(2) have "?C3  wffs⇘o⇙"
      using pwffs_subset_of_wffso by auto
    ultimately show ?thesis
      by (rule Cases)
  qed
  then show ?thesis
  proof -
    let  = "{(p, o)  A}"
    from assms(1) have "is_substitution "
      using pwffs_subset_of_wffso by auto
    moreover have "
      v  fmdom' . var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v ?C3"
    proof
      fix v
      assume "v  fmdom' "
      then have "v = (p, o)"
        by simp
      with assms(3) and (p, o)  vars B have "is_free_for ( $$! v) v ?C3"
        using occurs_in_vars
        by (intro is_free_for_in_imp is_free_for_in_forall is_free_for_in_equivalence) auto
      moreover have "var_name v  free_var_names ({}::form set)"
        by simp
      ultimately show "var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v ?C3"
        unfolding v = (p, o) by blast
    qed
    moreover have "  {$$}"
      by simp
    ultimately have " S  ?C3"
      by (rule Sub[OF "§8"])
    moreover have "S  ?C3 = xα⇙. (A 𝒬 B) 𝒬 (A 𝒬 xα⇙. B)"
      using p  x and sub[of A] by simp
    ultimately show ?thesis
      by (simp only:)
  qed
qed

proposition prop_5237:
  assumes "is_hyps "
  and "  A 𝒬 B"
  and "(x, α)  free_vars ({A}  )"
  shows "  A 𝒬 (xα⇙. B)"
proof -
  have "  A 𝒬 B"
    by fact
  with assms(3) have "  xα⇙. (A 𝒬 B)"
    using Gen by simp
  moreover have "  xα⇙. (A 𝒬 B) 𝒬 (A 𝒬 (xα⇙. B))"
  proof -
    from assms(2) have "A  wffs⇘o⇙" and "B  wffs⇘o⇙"
      using hyp_derivable_form_is_wffso by (blast dest: wffs_from_imp_op)+
    with assms(1,3) show ?thesis
      using prop_5237_aux and derivability_implies_hyp_derivability by simp
  qed
  ultimately show ?thesis
    by (rule Equality_Rules(1))
qed

lemmas "⊃∀" = prop_5237 (* synonym *)

corollary generalized_prop_5237:
  assumes "is_hyps "
  and "  A 𝒬 B"
  and "v  S. v  free_vars ({A}  )"
  and "lset vs = S"
  shows "  A 𝒬 (𝒬 vs B)"
using assms proof (induction vs arbitrary: S)
  case Nil
  then show ?case
    by simp
next
  case (Cons v vs)
  obtain x and α where "v = (x, α)"
    by fastforce
  from Cons.prems(3) have *: "v'  S. v'  free_vars ({A}  )"
    by blast
  then show ?case
  proof (cases "v  lset vs")
    case True
    with Cons.prems(4) have "lset vs = S"
      by auto
    with assms(1,2) and * have "  A 𝒬 𝒬 vs B"
      by (fact Cons.IH)
    with True and lset vs = S and v = (x, α) and * have "  A 𝒬 (xα⇙. 𝒬 vs B)"
      using prop_5237[OF assms(1)] by simp
    with v = (x, α) show ?thesis
      by simp
  next
    case False
    with lset (v # vs) = S have "lset vs = S - {v}"
      by auto
    moreover from * have "v'  S - {v}. v'  free_vars ({A}  )"
      by blast
    ultimately have "  A 𝒬 𝒬 vs B"
      using assms(1,2) by (intro Cons.IH)
    moreover from Cons.prems(4) and v = (x, α) and * have "(x, α)  free_vars ({A}  )"
      by auto
    ultimately have "  A 𝒬 (xα⇙. 𝒬 vs B)"
      using assms(1) by (intro prop_5237)
    with v = (x, α) show ?thesis
      by simp
  qed
qed

end

subsection ‹Proposition 5238›

context begin

private lemma prop_5238_aux:
  assumes "A  wffs⇘α⇙" and "B  wffs⇘α⇙"
  shows " ((λxβ⇙. A) =⇘βα(λxβ⇙. B)) 𝒬 xβ⇙. (A =⇘αB)"
proof -
  have "§1": "
     (𝔣βα⇙ =⇘βα𝔤βα) 𝒬 𝔵β⇙. (𝔣βα· 𝔵β⇙ =⇘α𝔤βα· 𝔵β)" (is  _ 𝒬 𝔵β⇙. ?C1)
    by (fact axiom_is_derivable_from_no_hyps[OF axiom_3])
  then have "§2": "
     (𝔣βα⇙ =⇘βα𝔤βα) 𝒬 xβ⇙. (𝔣βα· xβ⇙ =⇘α𝔤βα· xβ)" (is  ?C2)
  proof (cases "x = 𝔵")
    case True
    with "§1" show ?thesis
      by (simp only:)
  next
    case False
    have "?C1  wffs⇘o⇙"
      by blast
    moreover from False have "(x, β)  free_vars ?C1"
      by simp
    moreover have "is_free_for (xβ) (𝔵, β) ?C1"
      by (intro is_free_for_in_equality is_free_for_to_app) simp_all
    ultimately have " λ𝔵β⇙. ?C1 =⇘βoλxβ⇙. (S {(𝔵, β)  xβ} ?C1)"
      by (rule "α")
    from "§1" and this show ?thesis
      by (rule rule_R[where p = "[»,»]"]) force+
  qed
  then have "§3": "
     ((λxβ⇙. A) =⇘βα(λxβ⇙. B)) 𝒬 xβ⇙. ((λxβ⇙. A) · xβ⇙ =⇘α(λxβ⇙. B) · xβ)"
  proof -
    let  = "{(𝔣, βα)  λxβ⇙. A, (𝔤, βα)  λxβ⇙. B}"
    have "λxβ⇙. A  wffs⇘βα⇙" and "λxβ⇙. B  wffs⇘βα⇙"
      by (blast intro: assms(1,2))+
    then have "is_substitution "
      by simp
    moreover have "
      v  fmdom' . var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v ?C2"
    proof
      fix v
      assume "v  fmdom' "
      then consider (a) "v = (𝔣, βα)" | (b) "v = (𝔤, βα)"
        by fastforce
      then show "var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v ?C2"
      proof cases
        case a
        have "(x, β)  free_vars (λxβ⇙. A)"
          by simp
        then have "is_free_for (λxβ⇙. A) (𝔣, βα) ?C2"
          unfolding equivalence_def
          by (intro is_free_for_in_equality is_free_for_in_forall is_free_for_to_app, simp_all)
        with a show ?thesis
          by force
      next
        case b
        have "(x, β)  free_vars (λxβ⇙. B)"
          by simp
        then have "is_free_for (λxβ⇙. B) (𝔤, βα) ?C2"
          unfolding equivalence_def
          by (intro is_free_for_in_equality is_free_for_in_forall is_free_for_to_app, simp_all)
        with b show ?thesis
          by force
      qed
    qed
    moreover have "  {$$}"
      by simp
    ultimately have " S  ?C2"
      by (rule Sub[OF "§2"])
    then show ?thesis
      by simp
  qed
  then have "§4": " ((λxβ⇙. A) =⇘βα(λxβ⇙. B)) 𝒬 xβ⇙. (A =⇘α(λxβ⇙. B) · xβ)"
  proof -
    have " (λxβ⇙. A) · xβ⇙ =⇘αA"
      using prop_5208[where vs = "[(x, β)]"] and assms(1) by simp
    from "§3" and this show ?thesis
      by (rule rule_R[where p = "[»,»,«,«,»]"]) force+
  qed
  then show ?thesis
  proof -
    have " (λxβ⇙. B) · xβ⇙ =⇘αB"
      using prop_5208[where vs = "[(x, β)]"] and assms(2) by simp
    from "§4" and this show ?thesis
      by (rule rule_R[where p = "[»,»,«,»]"]) force+
  qed
qed

proposition prop_5238:
  assumes "vs  []" and "A  wffs⇘α⇙" and "B  wffs⇘α⇙"
  shows " λ𝒬 vs A =⇘foldr (→) (map var_type vs) αλ𝒬 vs B 𝒬 𝒬 vs (A =⇘αB)"
using assms proof (induction vs arbitrary: A B α rule: rev_nonempty_induct)
  case (single v)
  obtain x and β where "v = (x, β)"
    by fastforce
  from single.prems have "
    λ𝒬 vs A =⇘foldr (→) (map var_type vs) αλ𝒬 vs B 𝒬 𝒬 vs (A =⇘αB)  wffs⇘o⇙"
    by blast
  with single.prems and v = (x, β) show ?case
    using prop_5238_aux by simp
next
  case (snoc v vs)
  obtain x and β where "v = (x, β)"
    by fastforce
  from snoc.prems have "λxβ⇙. A  wffs⇘βα⇙" and "λxβ⇙. B  wffs⇘βα⇙"
    by auto
  then have "
    
      λ𝒬 vs (λxβ⇙. A) =⇘foldr (→) (map var_type vs) (βα)λ𝒬 vs (λxβ⇙. B)
      𝒬
      𝒬 vs ((λxβ⇙. A) =⇘βα(λxβ⇙. B))"
    by (fact snoc.IH)
  moreover from snoc.prems have " λxβ⇙. A =⇘βαλxβ⇙. B 𝒬 xβ⇙. (A =⇘αB)"
    by (fact prop_5238_aux)
  ultimately have "
    
      λ𝒬 vs (λxβ⇙. A) =⇘foldr (→) (map var_type vs) (βα)λ𝒬 vs (λxβ⇙. B)
      𝒬
      𝒬 vs xβ⇙. (A =⇘αB)"
  unfolding equivalence_def proof (induction rule: rule_R[where p = "» # foldr (λ_. (@) [»,«]) vs []"])
    case occ_subform
    then show ?case
      using innermost_subform_in_generalized_forall[OF snoc.hyps] and is_subform_at.simps(3)
      by fastforce
  next
    case replacement
    then show ?case
      using innermost_replacement_in_generalized_forall[OF snoc.hyps]
      and is_replacement_at_implies_in_positions and replace_right_app by force
  qed
  with v = (x, β) show ?case
    by simp
qed

end

subsection ‹Proposition 5239›

lemma replacement_derivability:
  assumes "C  wffs⇘β⇙"
  and "A ≼⇘pC"
  and " A =⇘αB"
  and "Cp  B  D"
  shows " C =⇘βD"
using assms proof (induction arbitrary: D p)
  case (var_is_wff γ x)
  from var_is_wff.prems(1) have "p = []" and "A = xγ⇙"
    by (auto elim: is_subform_at.elims(2))
  with var_is_wff.prems(2) have "α = γ"
    using hyp_derivable_form_is_wffso and wff_has_unique_type and wffs_from_equality by blast
  moreover from p = [] and var_is_wff.prems(3) have "D = B"
    using is_replacement_at_minimal_change(1) and is_subform_at.simps(1) by iprover
  ultimately show ?case
    using A = xγ⇙› and var_is_wff.prems(2) by (simp only:)
next
  case (con_is_wff γ c)
  from con_is_wff.prems(1) have "p = []" and "A = c⦄⇘γ⇙"
    by (auto elim: is_subform_at.elims(2))
  with con_is_wff.prems(2) have "α = γ"
    using hyp_derivable_form_is_wffso and wff_has_unique_type
    by (meson wffs_from_equality wffs_of_type_intros(2))
  moreover from p = [] and con_is_wff.prems(3) have "D = B"
    using is_replacement_at_minimal_change(1) and is_subform_at.simps(1) by iprover
  ultimately show ?case
    using A = c⦄⇘γ⇙› and con_is_wff.prems(2) by (simp only:)
next
  case (app_is_wff γ δ C1 C2)
  from app_is_wff.prems(1) consider
    (a) "p = []"
  | (b) "p'. p = « # p'  A ≼⇘p'C1"
  | (c) "p'. p = » # p'  A ≼⇘p'C2"
    using subforms_from_app by blast
  then show ?case
  proof cases
    case a
    with app_is_wff.prems(1) have "A = C1 · C2"
      by simp
    moreover from a and app_is_wff.prems(3) have "D = B"
      using is_replacement_at_minimal_change(1) and at_top_is_self_subform by blast
    moreover from A = C1 · C2 and D = B and app_is_wff.hyps(1,2) and assms(3) have "α = δ"
      using hyp_derivable_form_is_wffso and wff_has_unique_type
      by (blast dest: wffs_from_equality)
    ultimately show ?thesis
      using assms(3) by (simp only:)
  next
    case b
    then obtain p' where "p = « # p'" and "A ≼⇘p'C1"
      by blast
    moreover obtain D1 where "D = D1 · C2" and "C1p'  B  D1"
      using app_is_wff.prems(3) and p = « # p' by (force dest: is_replacement_at.cases)
    ultimately have " C1 =⇘γδD1"
      using app_is_wff.IH(1) and assms(3) by blast
    moreover have " C2 =⇘γC2"
      by (fact prop_5200[OF app_is_wff.hyps(2)])
    ultimately have " C1 · C2 =⇘δD1 · C2"
      using Equality_Rules(4) by (simp only:)
    with D = D1 · C2 show ?thesis
      by (simp only:)
  next
    case c
    then obtain p' where "p = » # p'" and "A ≼⇘p'C2"
      by blast
    moreover obtain D2 where "D = C1 · D2" and "C2p'  B  D2"
      using app_is_wff.prems(3) and p = » # p' by (force dest: is_replacement_at.cases)
    ultimately have " C2 =⇘γD2"
      using app_is_wff.IH(2) and assms(3) by blast
    moreover have " C1 =⇘γδC1"
      by (fact prop_5200[OF app_is_wff.hyps(1)])
    ultimately have " C1 · C2 =⇘δC1 · D2"
      using Equality_Rules(4) by (simp only:)
    with D = C1 · D2 show ?thesis
      by (simp only:)
  qed
next
  case (abs_is_wff δ C' γ x)
  from abs_is_wff.prems(1) consider (a) "p = []" | (b) "p'. p = « # p'  A ≼⇘p'C'"
    using subforms_from_abs by blast
  then show ?case
  proof cases
    case a
    with abs_is_wff.prems(1) have "A = λxγ⇙. C'"
      by simp
    moreover from a and abs_is_wff.prems(3) have "D = B"
      using is_replacement_at_minimal_change(1) and at_top_is_self_subform by blast
    moreover from A = λxγ⇙. C' and D = B and abs_is_wff.hyps(1) and assms(3) have "α = γδ"
      using hyp_derivable_form_is_wffso and wff_has_unique_type
      by (blast dest: wffs_from_abs wffs_from_equality)
    ultimately show ?thesis
      using assms(3) by (simp only:)
  next
    case b
    then obtain p' where "p = « # p'" and "A ≼⇘p'C'"
      by blast
    moreover obtain D' where "D = λxγ⇙. D'" and "C'p'  B  D'"
      using abs_is_wff.prems(3) and p = « # p' by (force dest: is_replacement_at.cases)
    ultimately have " C' =⇘δD'"
      using abs_is_wff.IH and assms(3) by blast
    then have " λxγ⇙. C' =⇘γδλxγ⇙. D'"
    proof -
      from  C' =⇘δD' have " xγ⇙. (C' =⇘δD')"
        using Gen by simp
      moreover from  C' =⇘δD' and abs_is_wff.hyps have "D'  wffs⇘δ⇙"
        using hyp_derivable_form_is_wffso by (blast dest: wffs_from_equality)
      with abs_is_wff.hyps have " (λxγ⇙. C' =⇘γδλxγ⇙. D') 𝒬 xγ⇙. (C' =⇘δD')"
        using prop_5238[where vs = "[(x, γ)]"] by simp
      ultimately show ?thesis
        using Equality_Rules(1,2) unfolding equivalence_def by blast
    qed
    with D = λxγ⇙. D' show ?thesis
      by (simp only:)
  qed
qed

context
begin

private lemma prop_5239_aux_1:
  assumes "p  positions (·𝒬 (FVar v) (map FVar vs))"
  and "p  replicate (length vs) «"
  shows "
    (A B. A · B ≼⇘p(·𝒬 (FVar v) (map FVar vs)))
    
    (v  lset vs. occurs_at v p (·𝒬 (FVar v) (map FVar vs)))"
using assms proof (induction vs arbitrary: p rule: rev_induct)
  case Nil
  then show ?case
    using surj_pair[of v] by fastforce
next
  case (snoc v' vs)
  from snoc.prems(1) consider
    (a) "p = []"
  | (b) "p = [»]"
  | (c) "p'  positions (·𝒬 (FVar v) (map FVar vs)). p = « # p'"
    using surj_pair[of v'] by fastforce
  then show ?case
  proof cases
    case c
    then obtain p' where "p'  positions (·𝒬 (FVar v) (map FVar vs))" and "p = « # p'"
      by blast
    from p = « # p' and snoc.prems(2) have "p'  replicate (length vs) «"
      by force
    then have "
      (A B. A · B ≼⇘p'·𝒬 (FVar v) (map FVar vs))
      
      (v  lset vs. occurs_at v p' (·𝒬 (FVar v) (map FVar vs)))"
      using p'  positions (·𝒬 (FVar v) (map FVar vs)) and snoc.IH by simp
    with p = « # p' show ?thesis
      by auto
  qed simp_all
qed

private lemma prop_5239_aux_2:
  assumes "t  lset vs  vars C"
  and "Cp  (·𝒬 (FVar t) (map FVar vs))  G"
  and "Cp  (·𝒬 (λ𝒬 vs A) (map FVar vs))  G'"
  shows "S {t  λ𝒬 vs A} G = G'" (is S  G = G')
proof -
  have "S  (·𝒬 (FVar t) (map FVar vs)) = ·𝒬 (S  (FVar t)) (map (λv'. S  v') (map FVar vs))"
    using generalized_app_substitution by blast
  moreover have "S  (FVar t) = λ𝒬 vs A"
    using surj_pair[of t] by fastforce
  moreover from assms(1) have "map (λv'. S  v') (map FVar vs) = map FVar vs"
    by (induction vs) auto
  ultimately show ?thesis
  using assms proof (induction C arbitrary: G G' p)
    case (FVar v)
    from FVar.prems(5) have "p = []" and "G = ·𝒬 (FVar t) (map FVar vs)"
      by (blast dest: is_replacement_at.cases)+
    moreover from FVar.prems(6) and p = [] have "G' = ·𝒬 (λ𝒬 vs A) (map FVar vs)"
      by (blast dest: is_replacement_at.cases)
    ultimately show ?case
      using FVar.prems(1-3) by (simp only:)
  next
    case (FCon k)
    from FCon.prems(5) have "p = []" and "G = ·𝒬 (FVar t) (map FVar vs)"
      by (blast dest: is_replacement_at.cases)+
    moreover from FCon.prems(6) and p = [] have "G' = ·𝒬 (λ𝒬 vs A) (map FVar vs)"
      by (blast dest: is_replacement_at.cases)
    ultimately show ?case
      using FCon.prems(1-3) by (simp only:)
  next
    case (FApp C1 C2)
    from FApp.prems(4) have "t  lset vs  vars C1" and "t  lset vs  vars C2"
      by auto
    consider (a) "p = []" | (b) "p'. p = « # p'" | (c) "p'. p = » # p'"
      by (metis direction.exhaust list.exhaust)
    then show ?case
    proof cases
      case a
      with FApp.prems(5) have "G = ·𝒬 (FVar t) (map FVar vs)"
        by (blast dest: is_replacement_at.cases)
      moreover from FApp.prems(6) and p = [] have "G' = ·𝒬 (λ𝒬 vs A) (map FVar vs)"
        by (blast dest: is_replacement_at.cases)
      ultimately show ?thesis
        using FApp.prems(1-3) by (simp only:)
    next
      case b
      then obtain p' where "p = « # p'"
        by blast
      with FApp.prems(5) obtain G1 where "G = G1 · C2" and "C1p'  (·𝒬 (FVar t) (map FVar vs))  G1"
        by (blast elim: is_replacement_at.cases)
      moreover from p = « # p' and FApp.prems(6)
      obtain G'1 where "G' = G'1 · C2" and "C1p'  (·𝒬 (λ𝒬 vs A) (map FVar vs))  G'1"
        by (blast elim: is_replacement_at.cases)
      moreover from t  lset vs  vars C2 have "S {t  λ𝒬 vs A} C2 = C2"
        using surj_pair[of t] and free_var_singleton_substitution_neutrality
        by (simp add: vars_is_free_and_bound_vars)
      ultimately show ?thesis
        using FApp.IH(1)[OF FApp.prems(1-3) t  lset vs  vars C1] by simp
    next
      case c
      then obtain p' where "p = » # p'"
        by blast
      with FApp.prems(5) obtain G2 where "G = C1 · G2" and "C2p'  (·𝒬 (FVar t) (map FVar vs))  G2"
        by (blast elim: is_replacement_at.cases)
      moreover from p = » # p' and FApp.prems(6)
      obtain G'2 where "G' = C1 · G'2" and "C2p'  (·𝒬 (λ𝒬 vs A) (map FVar vs))  G'2"
        by (blast elim: is_replacement_at.cases)
      moreover from t  lset vs  vars C1 have "S {t  λ𝒬 vs A} C1 = C1"
        using surj_pair[of t] and free_var_singleton_substitution_neutrality
        by (simp add: vars_is_free_and_bound_vars)
      ultimately show ?thesis
        using FApp.IH(2)[OF FApp.prems(1-3) t  lset vs  vars C2] by simp
    qed
  next
    case (FAbs v C')
    from FAbs.prems(4) have "t  lset vs  vars C'" and "t  v"
      using vars_form.elims by blast+
    from FAbs.prems(5) consider (a) "p = []" | (b) "p'. p = « # p'"
      using is_replacement_at.simps by blast
    then show ?case
    proof cases
      case a
      with FAbs.prems(5) have "G = ·𝒬 (FVar t) (map FVar vs)"
        by (blast dest: is_replacement_at.cases)
      moreover from FAbs.prems(6) and p = [] have "G' = ·𝒬 (λ𝒬 vs A) (map FVar vs)"
        by (blast dest: is_replacement_at.cases)
      ultimately show ?thesis
        using FAbs.prems(1-3) by (simp only:)
    next
      case b
      then obtain p' where "p = « # p'"
        by blast
      then obtain G1 where "G = FAbs v G1" and "C'p'  (·𝒬 (FVar t) (map FVar vs))  G1"
        using FAbs.prems(5) by (blast elim: is_replacement_at.cases)
      moreover from p = « # p' and FAbs.prems(6)
      obtain G'1 where "G' = FAbs v G'1" and "C'p'  (·𝒬 (λ𝒬 vs A) (map FVar vs))  G'1"
        by (blast elim: is_replacement_at.cases)
      ultimately have "S {t  λ𝒬 vs A} G1 = G'1"
        using FAbs.IH[OF FAbs.prems(1-3) t  lset vs  vars C'] by simp
      with G = FAbs v G1 and G' = FAbs v G'1 and t  v show ?thesis
        using surj_pair[of v] by fastforce
    qed
  qed
qed

private lemma prop_5239_aux_3:
  assumes "t  lset vs  vars {A, C}"
  and "Cp  (·𝒬 (FVar t) (map FVar vs))  G"
  and "occurs_at t p' G"
  shows "p' = p @ replicate (length vs) «" (is p' = ?pt)
proof (cases "vs = []")
  case True
  then have "t  vars C"
    using assms(1) by auto
  moreover from True and assms(2) have "Cp  FVar t  G"
    by force
  ultimately show ?thesis
    using assms(3) and True and fresh_var_replacement_position_uniqueness by simp
next
  case False
  show ?thesis
  proof (rule ccontr)
    assume "p'  ?pt"
    have "¬ prefix ?pt p"
      by (simp add: False)
    from assms(3) have "p'  positions G"
      using is_subform_implies_in_positions by fastforce
    from assms(2) have "?pt  positions G"
      using is_replacement_at_minimal_change(1) and is_subform_at_transitivity
      and is_subform_implies_in_positions and leftmost_subform_in_generalized_app
      by (metis length_map)
    from assms(2) have "occurs_at t ?pt G"
      unfolding occurs_at_def using is_replacement_at_minimal_change(1) and is_subform_at_transitivity
      and leftmost_subform_in_generalized_app
      by (metis length_map)
    moreover from assms(2) and p'  positions G have *: "
      subform_at C p' = subform_at G p'" if "¬ prefix p' p" and "¬ prefix p p'"
      using  is_replacement_at_minimal_change(2) by (simp add: that(1,2))
    ultimately show False
    proof (cases "¬ prefix p' p  ¬ prefix p p'")
      case True
      with assms(3) and * have "occurs_at t p' C"
        using is_replacement_at_occurs[OF assms(2)] by blast
      then have "t  vars C"
        using is_subform_implies_in_positions and occurs_in_vars by fastforce
      with assms(1) show ?thesis
        by simp
    next
      case False
      then consider (a) "prefix p' p" | (b) "prefix p p'"
        by blast
      then show ?thesis
      proof cases
        case a
        with occurs_at t ?pt G and p'  ?pt and assms(3) show ?thesis
          unfolding occurs_at_def using loop_subform_impossibility
          by (metis prefix_order.dual_order.order_iff_strict prefix_prefix)
      next
        case b
        have "strict_prefix p' ?pt"
        proof (rule ccontr)
          assume "¬ strict_prefix p' ?pt"
          then consider
            (b1) "p' = ?pt"
          | (b2) "strict_prefix ?pt p'"
          | (b3) "¬ prefix p' ?pt" and "¬ prefix ?pt p'"
            by fastforce
          then show False
          proof cases
            case b1
            with p'  ?pt show ?thesis
              by contradiction
          next
            case b2
            with occurs_at t ?pt G and assms(3) show ?thesis
              using loop_subform_impossibility by blast
          next
            case b3
            from b obtain p'' where "p' = p @ p''" and "p''  positions (·𝒬 (FVar t) (map FVar vs))"
              using is_replacement_at_new_positions and p'  positions G and assms(2) by blast
            moreover have "p''  replicate (length vs) «"
              using p' = p @ p'' and p'  ?pt by blast
            ultimately consider
              (b3_1) "F1 F2. F1 · F2 ≼⇘p''(·𝒬 (FVar t) (map FVar vs))"
            | (b3_2) "v  lset vs. occurs_at v p'' (·𝒬 (FVar t) (map FVar vs))"
              using prop_5239_aux_1 and b3(1,2) and is_replacement_at_occurs
              and leftmost_subform_in_generalized_app_replacement
              by (metis (no_types, opaque_lifting) length_map prefix_append)
            then show ?thesis
            proof cases
              case b3_1
              with assms(2) and p' = p @ p'' have "F1 F2. F1 · F2 ≼⇘p'G"
                using is_replacement_at_minimal_change(1) and is_subform_at_transitivity by meson
              with occurs_at t p' G show ?thesis
                using is_subform_at_uniqueness by fastforce
            next
              case b3_2
              with assms(2) and p' = p @ p'' have "v  lset vs. occurs_at v p' G"
                unfolding occurs_at_def
                using is_replacement_at_minimal_change(1) and is_subform_at_transitivity by meson
              with assms(1,3) show ?thesis
                using is_subform_at_uniqueness by fastforce
            qed
          qed
        qed
        with occurs_at t ?pt G and assms(3) show ?thesis
          using loop_subform_impossibility by blast
      qed
    qed
  qed
qed

private lemma prop_5239_aux_4:
  assumes "t  lset vs  vars {A, C}"
  and "A ≼⇘pC"
  and "lset vs  capture_exposed_vars_at p C A"
  and "Cp  (·𝒬 (FVar t) (map FVar vs))  G"
  shows "is_free_for (λ𝒬 vs A) t G"
unfolding is_free_for_def proof (intro ballI impI)
  let ?pt = "p @ replicate (length vs) «"
  from assms(4) have "FVar t ≼⇘?ptG"
    using is_replacement_at_minimal_change(1) and is_subform_at_transitivity
    and leftmost_subform_in_generalized_app by (metis length_map)
  fix v' and p'
  assume "v'  free_vars (λ𝒬 vs A)" and "p'  positions G" and "is_free_at t p' G"
  have "v'  binders_at G ?pt"
  proof -
    have "free_vars (λ𝒬 vs A) = free_vars A - lset vs"
      by (fact free_vars_of_generalized_abs)
    also from assms(2,3) have "  free_vars A - (binders_at C p  free_vars A)"
      using capture_exposed_vars_at_alt_def and is_subform_implies_in_positions by fastforce
    also have " = free_vars A - (binders_at G p  free_vars A)"
      using assms(2,4) is_replacement_at_binders is_subform_implies_in_positions by blast
    finally have "free_vars (λ𝒬 vs A)  free_vars A - (binders_at G p  free_vars A)" .
    moreover have "binders_at (·𝒬 (FVar t) (map FVar vs)) (replicate (length vs) «) = {}"
      by (induction vs rule: rev_induct) simp_all
    with assms(4) have "binders_at G ?pt = binders_at G p"
      using binders_at_concat and is_replacement_at_minimal_change(1) by blast
    ultimately show ?thesis
      using v'  free_vars (λ𝒬 vs A) by blast
  qed
  moreover have "p' = ?pt"
    by
      (
        fact prop_5239_aux_3
          [OF assms(1,4) is_free_at t p' G[unfolded is_free_at_def, THEN conjunct1]]
      )
  ultimately show "¬ in_scope_of_abs v' p' G"
    using binders_at_alt_def[OF p'  positions G] and in_scope_of_abs_alt_def by auto
qed

proposition prop_5239:
  assumes "is_rule_R_app p D C (A =⇘αB)"
  and "lset vs =
    {(x, β) | x β p' E. strict_prefix p' p  λxβ⇙. E ≼⇘p'C  (x, β)  free_vars (A =⇘αB)}"
  shows " 𝒬 vs (A =⇘αB) 𝒬 (C 𝒬 D)"
proof -
  let  = "foldr (→) (map var_type vs) α"
  obtain t where "(t, )  lset vs  vars {A,B,C,D}"
    using fresh_var_existence and vars_form_set_finiteness
    by (metis List.finite_set finite.simps finite_UnI)
  from assms(1) have "A  wffs⇘α⇙" and "B  wffs⇘α⇙" and "A ≼⇘pC"
    using wffs_from_equality[OF equality_wff] by simp_all
  from assms(1) have "C  wffs⇘o⇙" and "D  wffs⇘o⇙"
    using replacement_preserves_typing by fastforce+
  have "·𝒬 t(map FVar vs)  wffs⇘α⇙"
    using generalized_app_wff[where As = "map FVar vs" and ts = "map var_type vs"]
    by (metis eq_snd_iff length_map nth_map wffs_of_type_intros(1))
  from assms(1) have "p  positions C"
    using is_subform_implies_in_positions by fastforce
  then obtain G where "Cp  (·𝒬 t(map FVar vs))  G"
    using is_replacement_at_existence by blast
  with  A ≼⇘pC and ·𝒬 t(map FVar vs)  wffs⇘α⇙› have "G  wffs⇘o⇙"
    using A  wffs⇘α⇙› and C  wffs⇘o⇙› and replacement_preserves_typing by blast
  let  = "{(𝔥, o)  λt⇙. G, (𝔵, )  λ𝒬 vs A, (𝔶, )  λ𝒬 vs B}"
    and ?A = "(𝔵⇙ =⇘𝔶) 𝒬 (𝔥o· 𝔵𝒬 𝔥o· 𝔶)"
  have " ?A"
    by (fact axiom_is_derivable_from_no_hyps[OF axiom_2])
  moreover have "λt⇙. G  wffs⇘o⇙" and "λ𝒬 vs A  wffs⇘⇙" and "λ𝒬 vs B  wffs⇘⇙"
    by (blast intro: G  wffs⇘o⇙› A  wffs⇘α⇙› B  wffs⇘α⇙›)+
  then have "is_substitution "
    by simp
  moreover have "
    v  fmdom' . var_name v  free_var_names ({}::form set)  is_free_for ( $$! v) v ?A"
    by
    (
      (
        code_simp, unfold atomize_conj[symmetric], simp,
        use is_free_for_in_equality is_free_for_in_equivalence is_free_for_in_imp is_free_for_in_var
        is_free_for_to_app in presburger
      )+,
      blast
    )
  moreover have "  {$$}"
    by simp
  ultimately have " S  ?A"
    by (rule Sub)
  moreover have "
    S  ?A = (λ𝒬 vs A =⇘λ𝒬 vs B) 𝒬 ((λt⇙. G) · (λ𝒬 vs A) 𝒬 (λt⇙. G) · (λ𝒬 vs B))"
    by simp
  ultimately have "§1": "
     (λ𝒬 vs A =⇘λ𝒬 vs B) 𝒬 ((λt⇙. G) · (λ𝒬 vs A) 𝒬 (λt⇙. G) · (λ𝒬 vs B))"
    by (simp only:)
  then have "§2": " (𝒬 vs (A =⇘αB)) 𝒬 ((λt⇙. G) · (λ𝒬 vs A) 𝒬 (λt⇙. G) · (λ𝒬 vs B))"
  proof (cases "vs = []")
    case True
    with "§1" show ?thesis
      by simp
  next
    case False
    from "§1" and prop_5238[OF False A  wffs⇘α⇙› B  wffs⇘α⇙›] show ?thesis
      unfolding equivalence_def by (rule rule_R[where p = "[«,»]"]) force+
  qed
  moreover have " (λt⇙. G) · (λ𝒬 vs A) =⇘oC" and " (λt⇙. G) · (λ𝒬 vs B) =⇘oD"
  proof -
    from assms(1) have "B ≼⇘pD"
      using is_replacement_at_minimal_change(1) by force
    from assms(1) have "Dp  (·𝒬 t(map FVar vs))  G"
      using Cp  (·𝒬 t(map FVar vs))  G and replacement_override
      by (meson is_rule_R_app_def)
    from B ≼⇘pD have "p  positions D"
      using is_subform_implies_in_positions by auto
    from assms(1) have "binders_at D p = binders_at C p"
      using is_replacement_at_binders by fastforce
    then have "binders_at D p  free_vars B = binders_at C p  free_vars B"
      by simp
    with assms(2)
      [
        folded capture_exposed_vars_at_def,
        unfolded capture_exposed_vars_at_alt_def[OF p  positions C]
      ] have "lset vs  capture_exposed_vars_at p D B"
      unfolding capture_exposed_vars_at_alt_def[OF p  positions D] by auto
    have "is_free_for (λ𝒬 vs A) (t, ) G" and "is_free_for (λ𝒬 vs B) (t, ) G"
    proof -
      have "(t, )  lset vs  vars {A, C}" and "(t, )  lset vs  vars {B, D}"
        using (t, )  lset vs  vars {A, B, C, D} by simp_all
      moreover from assms(2) have "
        lset vs  capture_exposed_vars_at p C A" and "lset vs  capture_exposed_vars_at p D B"
        by fastforce fact
      ultimately show "is_free_for (λ𝒬 vs A) (t, ) G" and "is_free_for (λ𝒬 vs B) (t, ) G"
        using prop_5239_aux_4 and B ≼⇘pD and A ≼⇘pC and Cp  (·𝒬 t(map FVar vs))  G
        and Dp  (·𝒬 t(map FVar vs))  G by meson+
    qed
    then have " (λt⇙. G) · (λ𝒬 vs A) =⇘oS {(t, )  λ𝒬 vs A} G"
      and " (λt⇙. G) · (λ𝒬 vs B) =⇘oS {(t, )  λ𝒬 vs B} G"
      using prop_5207[OF λ𝒬 vs A  wffs⇘⇙› G  wffs⇘o⇙›]
      and prop_5207[OF λ𝒬 vs B  wffs⇘⇙› G  wffs⇘o⇙›] by auto
    moreover obtain G'1 and G'2
      where "Cp  (·𝒬 (λ𝒬 vs A) (map FVar vs))  G'1"
      and "Dp  (·𝒬 (λ𝒬 vs B) (map FVar vs))  G'2"
      using is_replacement_at_existence[OF p  positions C]
      and is_replacement_at_existence[OF p  positions D] by metis
    then have "S {(t, )  λ𝒬 vs A} G = G'1" and "S {(t, )  λ𝒬 vs B} G = G'2"
    proof -
      have "(t, )  lset vs  vars C" and "(t, )  lset vs  vars D"
        using (t, )  lset vs  vars {A, B, C, D} by simp_all
      then show "S {(t, )  λ𝒬 vs A} G = G'1" and "S {(t, )  λ𝒬 vs B} G = G'2"
        using Cp  (·𝒬 t(map FVar vs))  G and Dp  (·𝒬 tmap FVar vs)  G
        and Cp  (·𝒬 (λ𝒬 vs A) (map FVar vs))  G'1
        and Dp  (·𝒬 (λ𝒬 vs B) (map FVar vs))  G'2 and prop_5239_aux_2 by blast+
    qed
    ultimately have " (λt⇙. G) · (λ𝒬 vs A) =⇘oG'1" and " (λt⇙. G) · (λ𝒬 vs B) =⇘oG'2"
      by (simp_all only:)
    moreover
    have " A =⇘α(·𝒬 (λ𝒬 vs A) (map FVar vs))" and " B =⇘α(·𝒬 (λ𝒬 vs B) (map FVar vs))"
    unfolding atomize_conj proof (cases "vs = []")
      assume "vs = []"
      show " A =⇘α·𝒬 (λ𝒬 vs A) (map FVar vs)   B =⇘α·𝒬 (λ𝒬 vs B) (map FVar vs)"
        unfolding vs = [] using prop_5200 and A  wffs⇘α⇙› and B  wffs⇘α⇙› by simp
    next
      assume "vs  []"
      show " A =⇘α·𝒬 (λ𝒬 vs A) (map FVar vs)   B =⇘α·𝒬 (λ𝒬 vs B) (map FVar vs)"
        using Equality_Rules(2)[OF prop_5208[OF vs  []]] and A  wffs⇘α⇙› and B  wffs⇘α⇙›
        by blast+
    qed
    with
      Cp  (·𝒬 (λ𝒬 vs A) (map FVar vs))  G'1
    and
      Dp  (·𝒬 (λ𝒬 vs B) (map FVar vs))  G'2
    have " G'1 =⇘oC" and " G'2 =⇘oD"
      using Equality_Rules(2)[OF replacement_derivability] and C  wffs⇘o⇙› and D  wffs⇘o⇙›
      and A ≼⇘pC and B ≼⇘pD by blast+
    ultimately show " (λt⇙. G) · (λ𝒬 vs A) =⇘oC" and " (λt⇙. G) · (λ𝒬 vs B) =⇘oD"
      using Equality_Rules(3) by blast+
  qed
  ultimately show ?thesis
  proof -
    from "§2" and  (λt⇙. G) · (λ𝒬 vs A) =⇘oC have "
       (𝒬 vs (A =⇘αB)) 𝒬 (C 𝒬 (λt⇙. G) · (λ𝒬 vs B))"
      by (rule rule_R[where p = "[»,«,»]"]) force+
    from this and  (λt⇙. G) · (λ𝒬 vs B) =⇘oD show ?thesis
      by (rule rule_R[where p = "[»,»]"]) force+
  qed
qed

end

subsection ‹Theorem 5240 (Deduction Theorem)›

lemma pseudo_rule_R_is_tautologous:
  assumes "C  wffs⇘o⇙" and "D  wffs⇘o⇙" and "E  wffs⇘o⇙" and "H  wffs⇘o⇙"
  shows "is_tautologous (((H 𝒬 C) 𝒬 ((H 𝒬 E) 𝒬 ((E 𝒬 (C 𝒬 D)) 𝒬 (H 𝒬 D)))))"
proof -
  let  = "{(𝔵, o)  C, (𝔶, o)  D, (𝔷, o)  E, (𝔥, o)  H}"
  have "
    is_tautology
      (((𝔥o𝒬 𝔵o) 𝒬 ((𝔥o𝒬 𝔷o) 𝒬 ((𝔷o𝒬 (𝔵o𝒬 𝔶o)) 𝒬 (𝔥o𝒬 𝔶o)))))"
    using 𝒱B_simps by simp
  moreover have "is_substitution "
    using assms by auto
  moreover have "(x, α)  fmdom' . α = o"
    by simp
  moreover have "
    ((H 𝒬 C) 𝒬 ((H 𝒬 E) 𝒬 ((E 𝒬 (C 𝒬 D)) 𝒬 (H 𝒬 D))))
    =
    S  (((𝔥o𝒬 𝔵o) 𝒬 ((𝔥o𝒬 𝔷o) 𝒬 ((𝔷o𝒬 (𝔵o𝒬 𝔶o)) 𝒬 (𝔥o𝒬 𝔶o)))))"
    by simp
  ultimately show ?thesis
    by blast
qed

syntax
  "_HypDer" :: "form  form set  form  bool" ("_,_  _" [50, 50, 50] 50)
translations
  ", H  P"  "  {H}  P"

theorem thm_5240:
  assumes "finite "
  and ", H  P"
  shows "  H 𝒬 P"
proof -
  from , H  P obtain 𝒮1 and 𝒮2 where *: "is_hyp_proof_of (  {H}) 𝒮1 𝒮2 P"
    using hyp_derivability_implies_hyp_proof_existence by blast
  have "  H 𝒬 (𝒮2 ! i')" if "i' <length 𝒮2" for i'
  using that proof (induction i' rule: less_induct)
    case (less i')
    let ?R = "𝒮2 ! i'"
    from less.prems(1) and * have "is_hyps "
      by fastforce
    from less.prems and * have "?R  wffs⇘o⇙"
      using elem_of_proof_is_wffo[simplified] by auto
    from less.prems and * have "is_hyp_proof_step (  {H}) 𝒮1 𝒮2 i'"
      by simp
    then consider
      (hyp) "?R    {H}"
    | (seq) "?R  lset 𝒮1"
    | (rule_R') "j k p. {j, k}  {0..<i'}  is_rule_R'_app (  {H}) p ?R (𝒮2 ! j) (𝒮2 ! k)"
      by force
    then show ?case
    proof cases
      case hyp
      then show ?thesis
      proof (cases "?R = H")
        case True
        with ?R  wffs⇘o⇙› have "is_tautologous (H 𝒬 ?R)"
          using implication_reflexivity_is_tautologous by (simp only:)
        with is_hyps  show ?thesis
          by (rule rule_P(2))
      next
        case False
        with hyp have "?R  "
          by blast
        with is_hyps  have "  ?R"
          by (intro dv_hyp)
        moreover from less.prems(1) and * have "is_tautologous (?R 𝒬 (H 𝒬 ?R))"
          using principle_of_simplification_is_tautologous[OF ?R  wffs⇘o⇙›] by force
        moreover from ?R  wffs⇘o⇙› have "is_hyps {?R}"
          by simp
        ultimately show ?thesis
          using rule_P(1)[where 𝒢 = "{?R}" and hs = "[?R]", OF is_hyps ] by simp
      qed
    next
      case seq
      then have "𝒮1  []"
        by force
      moreover from less.prems(1) and * have "is_proof 𝒮1"
        by fastforce
      moreover from seq obtain i'' where "i'' < length 𝒮1" and "?R = 𝒮1 ! i''"
        by (metis in_set_conv_nth)
      ultimately have "is_theorem ?R"
        using proof_form_is_theorem by fastforce
      with is_hyps  have "  ?R"
        by (intro dv_thm)
      moreover from ?R  wffs⇘o⇙› and less.prems(1) and * have "is_tautologous (?R 𝒬 (H 𝒬 ?R))"
        using principle_of_simplification_is_tautologous by force
      moreover from ?R  wffs⇘o⇙› have "is_hyps {?R}"
        by simp
      ultimately show ?thesis
        using rule_P(1)[where 𝒢 = "{?R}" and hs = "[?R]", OF is_hyps ] by simp
    next
      case rule_R'
      then obtain j and k and p
        where "{j, k}  {0..<i'}" and rule_R'_app: "is_rule_R'_app (  {H}) p ?R (𝒮2 ! j) (𝒮2 ! k)"
        by auto
      then obtain A and B and C and α where "C = 𝒮2 ! j" and "𝒮2 ! k = A =⇘αB"
        by fastforce
      with {j, k}  {0..<i'} have "  H 𝒬 C" and "  H 𝒬 (A =⇘αB)"
        using less.IH and less.prems(1) by (simp, force)
      define S where "S 
        {(x, β) | x β p' E. strict_prefix p' p  λxβ⇙. E ≼⇘p'C  (x, β)  free_vars (A =⇘αB)}"
      with C = 𝒮2 ! j and 𝒮2 ! k = A =⇘αB have "v  S. v  free_vars (  {H})"
        using rule_R'_app by fastforce
      moreover have "S  free_vars (A =⇘αB)"
        unfolding S_def by blast
      then have "finite S"
        by (fact rev_finite_subset[OF free_vars_form_finiteness])
      then obtain vs where "lset vs = S"
        using finite_list by blast
      ultimately have "  H 𝒬 𝒬 vs (A =⇘αB)"
        using generalized_prop_5237[OF is_hyps    H 𝒬 (A =⇘αB)] by simp
      moreover have rule_R_app: "is_rule_R_app p ?R (𝒮2 ! j) (𝒮2 ! k)"
        using rule_R'_app by fastforce
      with S_def and lset vs = S have " 𝒬 vs (A =⇘αB) 𝒬 (C 𝒬 ?R)"
        unfolding C = 𝒮2 ! j and 𝒮2 ! k = A =⇘αB using prop_5239 by (simp only:)
      with is_hyps  have "  𝒬 vs (A =⇘αB) 𝒬 (C 𝒬 ?R)"
        by (elim derivability_implies_hyp_derivability)
      ultimately show ?thesis
      proof -
        let ?A1 = "H 𝒬 C" and ?A2 = "H 𝒬 𝒬 vs (A =⇘αB)"
          and ?A3 = "𝒬 vs (A =⇘αB) 𝒬 (C 𝒬 ?R)"
        let ?hs = "[?A1, ?A2, ?A3]"
        let ?𝒢 = "lset ?hs"
        from   ?A1 have "H  wffs⇘o⇙"
          using hyp_derivable_form_is_wffso by (blast dest: wffs_from_imp_op(1))
        moreover from   ?A2 have "𝒬 vs (A =⇘αB)  wffs⇘o⇙"
          using hyp_derivable_form_is_wffso by (blast dest: wffs_from_imp_op(2))
        moreover from C = 𝒮2 ! j and rule_R_app have "C  wffs⇘o⇙"
          using replacement_preserves_typing by fastforce
        ultimately have *: "is_tautologous (?A1 𝒬 (?A2 𝒬 (?A3 𝒬 (H 𝒬 ?R))))"
          using ?R  wffs⇘o⇙› by (intro pseudo_rule_R_is_tautologous)
        moreover from   ?A1 and   ?A2 and   ?A3 have "is_hyps ?𝒢"
          using hyp_derivable_form_is_wffso by simp
        moreover from   ?A1 and   ?A2 and   ?A3 have "A  ?𝒢.   A"
          by force
        ultimately show ?thesis
          using rule_P(1)[where 𝒢 = ?𝒢 and hs = ?hs and B = "H 𝒬 ?R", OF is_hyps ] by simp
      qed
    qed
  qed
  moreover from is_hyp_proof_of (  {H}) 𝒮1 𝒮2 P have "𝒮2 ! (length 𝒮2 - 1) = P"
    using last_conv_nth by fastforce
  ultimately show ?thesis
    using is_hyp_proof_of (  {H}) 𝒮1 𝒮2 P by force
qed

lemmas Deduction_Theorem = thm_5240 (* synonym *)

text ‹
  We prove a generalization of the Deduction Theorem, namely that if ℋ ∪ {H1, … ,Hn} ⊢ P› then
  ℋ ⊢ H1𝒬 (⋯ ⊃𝒬 (Hn𝒬 P) ⋯)›:
›

corollary generalized_deduction_theorem:
  assumes "finite " and "finite ℋ'"
  and "  ℋ'  P"
  and "lset hs = ℋ'"
  shows "  hs 𝒬 P"
using assms proof (induction hs arbitrary: ℋ' P rule: rev_induct)
  case Nil
  then show ?case
    by simp
next
  case (snoc H hs)
  from lset (hs @ [H]) = ℋ' have "H  ℋ'"
    by fastforce
  from lset (hs @ [H]) = ℋ' obtain ℋ'' where "ℋ''  {H} = ℋ'" and "ℋ'' = lset hs"
    by simp
  from ℋ''  {H} = ℋ' and   ℋ'  P have "  ℋ''  {H}  P"
    by fastforce
  with finite  and finite ℋ' and ℋ'' = lset hs have "  ℋ''  H 𝒬 P"
    using Deduction_Theorem by simp
  with ℋ'' = lset hs and finite  have "  foldr (⊃𝒬) hs (H 𝒬 P)"
    using snoc.IH by fastforce
  moreover have "(hs @ [H]) 𝒬 P = hs 𝒬 (H 𝒬 P)"
    by simp
  ultimately show ?case
    by auto
qed

subsection ‹Proposition 5241›

proposition prop_5241:
  assumes "is_hyps 𝒢"
  and "  A" and "  𝒢"
  shows "𝒢  A"
proof (cases " = {}")
  case True
  show ?thesis
    by (fact derivability_implies_hyp_derivability[OF assms(2)[unfolded True] assms(1)])
next
  case False
  then obtain hs where "lset hs = " and "hs  []"
    using hyp_derivability_implies_hyp_proof_existence[OF assms(2)] unfolding is_hyp_proof_of_def
    by (metis empty_set finite_list)
  with assms(2) have " hs 𝒬 A"
    using generalized_deduction_theorem by force
  moreover from lset hs =  and assms(1,3) have "𝒢  H" if "H  lset hs" for H
    using that by (blast intro: dv_hyp)
  ultimately show ?thesis
    using assms(1) and generalized_modus_ponens and derivability_implies_hyp_derivability by meson
qed

subsection ‹Proposition 5242 (Rule of Existential Generalization)›

proposition prop_5242:
  assumes "A  wffs⇘α⇙" and "B  wffs⇘o⇙"
  and "  S {(x, α)  A} B"
  and "is_free_for A (x, α) B"
  shows "  xα⇙. B"
proof -
  from assms(3) have "is_hyps "
    by (blast dest: is_derivable_from_hyps.cases)
  then have "  xα⇙. 𝒬 B 𝒬 𝒬 S {(x, α)  A} B" (is   ?C 𝒬 𝒬 ?D)
    using prop_5226[OF assms(1) neg_wff[OF assms(2)] is_free_for_in_neg[OF assms(4)]]
    unfolding derived_substitution_simps(4) using derivability_implies_hyp_derivability by (simp only:)
  moreover have *: "is_tautologous ((?C 𝒬 𝒬 ?D) 𝒬 (?D 𝒬 𝒬 ?C))"
  proof -
    have "?C  wffs⇘o⇙" and "?D  wffs⇘o⇙"
      using assms(2) and hyp_derivable_form_is_wffso[OF assms(3)] by auto
    then show ?thesis
      by (fact pseudo_modus_tollens_is_tautologous)
  qed
  moreover from assms(3) and   ?C 𝒬 𝒬 ?D have "is_hyps {?C 𝒬 𝒬 ?D, ?D}"
    using hyp_derivable_form_is_wffso by force
  ultimately show ?thesis
    unfolding exists_def using assms(3)
    and rule_P(1)
      [
        where 𝒢 = "{?C 𝒬 𝒬 ?D, ?D}" and hs = "[?C 𝒬 𝒬 ?D, ?D]" and B = "𝒬 ?C",
        OF is_hyps 
      ]
    by simp
qed

lemmas "∃Gen" = prop_5242 (* synonym *)

subsection ‹Proposition 5243 (Comprehension Theorem)›

context
begin

private lemma prop_5243_aux:
  assumes "·𝒬 B (map FVar vs)  wffs⇘γ⇙"
  and "B  wffs⇘β⇙"
  and "k < length vs"
  shows "β  var_type (vs ! k)"
proof -
  from assms(1) obtain ts
    where "length ts = length (map FVar vs)"
    and *: "k < length (map FVar vs). (map FVar vs) ! k  wffs⇘ts ! k⇙"
    and "B  wffs⇘foldr (→) ts γ⇙"
    using wffs_from_generalized_app by force
  have "β = foldr (→) ts γ"
    by (fact wff_has_unique_type[OF assms(2) B  wffs⇘foldr (→) ts γ⇙›])
  have "ts = map var_type vs"
  proof -
    have "length ts = length (map var_type vs)"
      by (simp add: length ts = length (map FVar vs))
    moreover have "k < length ts. ts ! k = (map var_type vs) ! k"
    proof (intro allI impI)
      fix k
      assume "k < length ts"
      with * have "(map FVar vs) ! k  wffs⇘ts ! k⇙"
        by (simp add: length ts = length (map FVar vs))
      with k < length ts and length ts = length (map var_type vs)
      show "ts ! k = (map var_type vs) ! k"
        using surj_pair[of "vs ! k"] and wff_has_unique_type and wffs_of_type_intros(1) by force
    qed
    ultimately show ?thesis
      using list_eq_iff_nth_eq by blast
  qed
  with β = foldr (→) ts γ and assms(3) show ?thesis
    using fun_type_atoms_neq_fun_type by (metis length_map nth_map)
qed

proposition prop_5243:
  assumes "B  wffs⇘β⇙"
  and "γ = foldr (→) (map var_type vs) β"
  and "(u, γ)  free_vars B"
  shows " uγ⇙. 𝒬 vs ((·𝒬 uγ(map FVar vs)) =⇘βB)"
proof (cases "vs = []")
  case True
  with assms(2) have "γ = β"
    by simp
  from assms(1) have "uβ⇙ =⇘βB  wffs⇘o⇙"
    by blast
  moreover have " B =⇘βB"
    by (fact prop_5200[OF assms(1)])
  then have " S {(u, β)  B} (uβ⇙ =⇘βB)"
    using free_var_singleton_substitution_neutrality[OF assms(3)] unfolding γ = β by simp
  moreover from assms(3)[unfolded γ = β] have "is_free_for B (u, β) (uβ⇙ =⇘βB)"
    by (intro is_free_for_in_equality) (use is_free_at_in_free_vars in auto)
  ultimately have " uβ⇙. (uβ⇙ =⇘βB)"
    by (rule "∃Gen"[OF assms(1)])
  with γ = β and True show ?thesis
    by simp
next
  case False
  let  = "{(u, γ)  λ𝒬 vs B}"
  from assms(2) have *: "(u, γ)  v" if "v  lset vs" for v
    using that and fun_type_atoms_neq_fun_type by (metis in_set_conv_nth length_map nth_map snd_conv)
  from False and assms(1) have " ·𝒬 (λ𝒬 vs B) (map FVar vs) =⇘βB"
    by (fact prop_5208)
  then have " 𝒬 vs (·𝒬 (λ𝒬 vs B) (map FVar vs) =⇘βB)"
    using generalized_Gen by simp
  moreover
  have "S  (𝒬 vs ((·𝒬 uγ(map FVar vs)) =⇘βB)) = 𝒬 vs (·𝒬 (λ𝒬 vs B) (map FVar vs) =⇘βB)"
  proof -
    from * have **: "map (λA. S {(u, γ)  B} A) (map FVar vs) = map FVar vs" for B
      by (induction vs) fastforce+
    from * have "
      S  (𝒬 vs ((·𝒬 uγ(map FVar vs)) =⇘βB)) = 𝒬 vs (S  ((·𝒬 uγ(map FVar vs)) =⇘βB))"
      using generalized_forall_substitution by force
    also have " = 𝒬 vs ((S  (·𝒬 uγ(map FVar vs))) =⇘βS {(u, γ)  λ𝒬 vs B} B)"
      by simp
    also from assms(3) have " = 𝒬 vs ((S  (·𝒬 uγ(map FVar vs))) =⇘βB)"
      using free_var_singleton_substitution_neutrality by simp
    also have " = 𝒬 vs (·𝒬 S  (uγ) (map (λA. S  A) (map FVar vs)) =⇘βB)"
      using generalized_app_substitution by simp
    also have " = 𝒬 vs (·𝒬 (λ𝒬 vs B) (map (λA. S  A) (map FVar vs)) =⇘βB)"
      by simp
    also from ** have " = 𝒬 vs (·𝒬 (λ𝒬 vs B) (map FVar vs) =⇘βB)"
      by presburger
    finally show ?thesis .
  qed
  ultimately have " S  (𝒬 vs (·𝒬 uγ(map FVar vs) =⇘βB))"
    by simp
  moreover from assms(3) have "is_free_for (λ𝒬 vs B) (u, γ) (𝒬 vs (·𝒬 uγ(map FVar vs) =⇘βB))"
    by
      (intro is_free_for_in_generalized_forall is_free_for_in_equality is_free_for_in_generalized_app)
      (use free_vars_of_generalized_abs is_free_at_in_free_vars in fastforce+)
  moreover have "λ𝒬 vs B  wffs⇘γ⇙" and "𝒬 vs (·𝒬 uγ(map FVar vs) =⇘βB)  wffs⇘o⇙"
  proof -
    have "FVar (vs ! k)  wffs⇘var_type (vs ! k)⇙" if "k < length vs" for k
      using that and surj_pair[of "vs ! k"] by fastforce
    with assms(2) have "·𝒬 uγ(map FVar vs)  wffs⇘β⇙"
      using generalized_app_wff[where ts = "map var_type vs"] by force
    with assms(1) show "𝒬 vs (·𝒬 uγ(map FVar vs) =⇘βB)  wffs⇘o⇙"
      by (auto simp only:)
  qed (use assms(1,2) in blast)
  ultimately show ?thesis
    using "∃Gen" by (simp only:)
qed

end

subsection ‹Proposition 5244 (Existential Rule)›

text ‹
  The proof in cite"andrews:2002" uses the pseudo-rule Q and 2123 of ℱ›. Therefore, we instead
  base our proof on the proof of Theorem 170 in cite"andrews:1965":
›

lemma prop_5244_aux:
  assumes "A  wffs⇘o⇙" and "B  wffs⇘o⇙"
  and "(x, α)  free_vars A"
  shows " xα⇙. (B 𝒬 A) 𝒬 (xα⇙. B 𝒬 A)"
proof -
  have "B 𝒬 A  wffs⇘o⇙"
    using assms by blast
  moreover have "is_free_for (xα) (x, α) (B 𝒬 A)"
    by simp
  ultimately have " xα⇙. (B 𝒬 A) 𝒬 (B 𝒬 A)"
    using prop_5226[where A = "xα⇙" and B = "B 𝒬 A", OF wffs_of_type_intros(1)]
    and identity_singleton_substitution_neutrality by metis
  moreover have "is_hyps {xα⇙. (B 𝒬 A)}"
    using B 𝒬 A  wffs⇘o⇙› by blast
  ultimately have "§1": "{xα⇙. (B 𝒬 A)}  xα⇙. (B 𝒬 A) 𝒬 (B 𝒬 A)"
    by (fact derivability_implies_hyp_derivability)
  have "§2": "{xα⇙. (B 𝒬 A)}  xα⇙. (B 𝒬 A)"
    using B 𝒬 A  wffs⇘o⇙› by (blast intro: dv_hyp)
  have "§3": "{xα⇙. (B 𝒬 A)}  𝒬 A 𝒬 𝒬 B"
  proof (intro rule_P(1)
    [where= "{xα⇙. (B 𝒬 A)}" and 𝒢 = "{xα⇙. (B 𝒬 A) 𝒬 (B 𝒬 A), xα⇙. (B 𝒬 A)}"])
    have "is_tautologous ([C 𝒬 (B 𝒬 A), C] 𝒬 (𝒬 A 𝒬 𝒬 B))" if "C  wffs⇘o⇙" for C
    proof -
      let  = "{(𝔵, o)  A, (𝔶, o)  B, (𝔷, o)  C}"
      have "is_tautology ((𝔷o𝒬 (𝔶o𝒬 𝔵o)) 𝒬 (𝔷o𝒬 (𝒬 𝔵o𝒬 𝒬 𝔶o)))"
        (is "is_tautology ?A")
        using 𝒱B_simps by (auto simp add: inj_eq)
      moreover have "is_pwff_substitution "
        using assms(1,2) and that by auto
      moreover have "[C 𝒬 (B 𝒬 A), C] 𝒬 (𝒬 A 𝒬 𝒬 B) = S  ?A"
        by simp
      ultimately show ?thesis
        by blast
    qed
    then show "is_tautologous ([xα⇙. (B 𝒬 A) 𝒬 (B 𝒬 A), xα⇙. (B 𝒬 A)] 𝒬 (𝒬 A 𝒬 𝒬 B))"
      using B 𝒬 A  wffs⇘o⇙› and forall_wff by simp
  qed (use "§1" "§2" is_hyps {xα⇙. (B 𝒬 A)} hyp_derivable_form_is_wffso[OF "§1"] in force)+
  have "§4": "{xα⇙. (B 𝒬 A)}  𝒬 A 𝒬 xα⇙. 𝒬 B"
    using prop_5237[OF is_hyps {xα⇙. (B 𝒬 A)} "§3"] and assms(3) by auto
  have "§5": "{xα⇙. (B 𝒬 A)}  xα⇙. B 𝒬 A"
  unfolding exists_def
  proof (intro rule_P(1)[where= "{xα⇙. (B 𝒬 A)}" and 𝒢 = "{𝒬 A 𝒬 xα⇙. 𝒬 B}"])
    have "is_tautologous ([𝒬 A 𝒬 C] 𝒬 (𝒬 C 𝒬 A))" if "C  wffs⇘o⇙" for C
    proof -
      let  = "{(𝔵, o)  A, (𝔶, o)  C}"
      have "is_tautology ((𝒬 𝔵o𝒬 𝔶o) 𝒬 (𝒬 𝔶o𝒬 𝔵o))" (is "is_tautology ?A")
        using 𝒱B_simps by (auto simp add: inj_eq)
      moreover have "is_pwff_substitution "
        using assms(1) and that by auto
      moreover have "[𝒬 A 𝒬 C] 𝒬 (𝒬 C 𝒬 A) = S  ?A"
        by simp
      ultimately show ?thesis
        by blast
    qed
    then show "is_tautologous ([𝒬 A 𝒬 xα⇙. 𝒬 B] 𝒬 (𝒬 xα⇙. 𝒬 B 𝒬 A))"
      using forall_wff[OF neg_wff[OF assms(2)]] by (simp only:)
  qed (use "§4" is_hyps {xα⇙. (B 𝒬 A)} hyp_derivable_form_is_wffso[OF "§4"] in force)+
  then show ?thesis
    using Deduction_Theorem by simp
qed

proposition prop_5244:
  assumes ", B  A"
  and "(x, α)  free_vars (  {A})"
  shows ", xα⇙. B  A"
proof -
  from assms(1) have "is_hyps "
    using hyp_derivability_implies_hyp_proof_existence by force
  then have "  B 𝒬 A"
    using assms(1) and Deduction_Theorem by simp
  then have "  xα⇙. (B 𝒬 A)"
    using Gen and assms(2) by simp
  moreover have "A  wffs⇘o⇙" and "B  wffs⇘o⇙"
    by
    (
      fact hyp_derivable_form_is_wffso[OF assms(1)],
      fact hyp_derivable_form_is_wffso[OF   B 𝒬 A, THEN wffs_from_imp_op(1)]
    )
  with assms(2) and is_hyps  have "  xα⇙. (B 𝒬 A) 𝒬 (xα⇙. B 𝒬 A)"
    using prop_5244_aux[THEN derivability_implies_hyp_derivability] by simp
  ultimately have "  xα⇙. B 𝒬 A"
    by (rule MP)
  then have ", xα⇙. B  xα⇙. B 𝒬 A"
    using prop_5241 and exists_wff[OF B  wffs⇘o⇙›] and is_hyps 
    by (meson Un_subset_iff empty_subsetI finite.simps finite_Un inf_sup_ord(3) insert_subsetI)
  moreover from is_hyps  and B  wffs⇘o⇙› have "is_hyps (  {xα⇙. B})"
    by auto
  then have ", xα⇙. B  xα⇙. B"
    using dv_hyp by simp
  ultimately show ?thesis
    using MP by blast
qed

lemmas "∃_Rule" = prop_5244 (* synonym *)

subsection ‹Proposition 5245 (Rule C)›

lemma prop_5245_aux:
  assumes "x  y"
  and "(y, α)  free_vars (xα⇙. B)"
  and "is_free_for (yα) (x, α) B"
  shows "is_free_for (xα) (y, α) S {(x, α)  yα} B"
using assms(2,3) proof (induction B)
  case (FVar v)
  then show ?case
    using surj_pair[of v] by fastforce
next
  case (FCon k)
  then show ?case
    using surj_pair[of k] by fastforce
next
  case (FApp B1 B2)
  from FApp.prems(1) have "(y, α)  free_vars (xα⇙. B1)" and "(y, α)  free_vars (xα⇙. B2)"
    by force+
  moreover from FApp.prems(2) have "is_free_for (yα) (x, α) B1" and "is_free_for (yα) (x, α) B2"
    using is_free_for_from_app by iprover+
  ultimately have "is_free_for (xα) (y, α) S {(x, α)  yα} B1"
    and "is_free_for (xα) (y, α) S {(x, α)  yα} B2"
    using FApp.IH by simp_all
  then have "is_free_for (xα) (y, α) ((S {(x, α)  yα} B1) · (S {(x, α)  yα} B2))"
    by (intro is_free_for_to_app)
  then show ?case
    unfolding singleton_substitution_simps(3) .
next
  case (FAbs v B')
  obtain z and β where "v = (z, β)"
    by fastforce
  then show ?case
  proof (cases "v = (x, α)")
    case True
    with FAbs.prems(1) have "(y, α)  free_vars (xα⇙. B')"
      by simp
    moreover from assms(1) have "(y, α)  (x, α)"
      by blast
    ultimately have "(y, α)  free_vars B'"
      using FAbs.prems(1) by simp
    with (y, α)  (x, α) have "(y, α)  free_vars (λxα⇙. B')"
      by simp
    then have "is_free_for (xα) (y, α) (λxα⇙. B')"
      unfolding is_free_for_def using is_free_at_in_free_vars by blast
    then have "is_free_for (xα) (y, α) S {(x, α)  yα} (λxα⇙. B')"
      using singleton_substitution_simps(4) by presburger
    then show ?thesis
      unfolding True .
  next
    case False
    from assms(1) have "(y, α)  (x, α)"
      by blast
    with FAbs.prems(1) have *: "(y, α)  free_vars (xα⇙. (λzβ⇙. B'))"
      using v = (z, β) by fastforce
    then show ?thesis
    proof (cases "(y, α)  v")
      case True
      from True[unfolded v = (z, β)] and * have "(y, α)  free_vars (xα⇙. B')"
        by simp
      moreover from False[unfolded v = (z, β)] have "is_free_for (yα) (x, α) B'"
        using is_free_for_from_abs[OF FAbs.prems(2)[unfolded v = (z, β)]] by blast
      ultimately have "is_free_for (xα) (y, α) (S {(x, α)  yα} B')"
        by (fact FAbs.IH)
      then have "is_free_for (xα) (y, α) (λzβ⇙. (S {(x, α)  yα} B'))"
        using False[unfolded v = (z, β)] by (intro is_free_for_to_abs, fastforce+)
      then show ?thesis
        unfolding singleton_substitution_simps(4) and v = (z, β) using (z, β)  (x, α) by auto
    next
      case False
      then have "v = (y, α)"
        by simp
      have "is_free_for (xα) (y, α) (λyα⇙. S {(x, α)  yα} B')"
      proof-
        have "(y, α)  free_vars (λyα⇙. S {(x, α)  yα} B')"
          by simp
        then show ?thesis
          using is_free_at_in_free_vars by blast
      qed
      withv = (y, α) and (y, α)  (x, α) show ?thesis
       using singleton_substitution_simps(4) by presburger
    qed
  qed
qed

proposition prop_5245:
  assumes "  xα⇙. B"
  and ", S {(x, α)  yα} B  A"
  and "is_free_for (yα) (x, α) B"
  and "(y, α)  free_vars (  {xα⇙. B, A})"
  shows "  A"
proof -
  from assms(1) have "is_hyps "
    by (blast elim: is_derivable_from_hyps.cases)
  from assms(2,4) have ", yα⇙. S {(x, α)  yα} B  A"
    using "∃_Rule" by simp
  then have *: "  (yα⇙. S {(x, α)  yα} B) 𝒬 A" (is _  ?F)
    using Deduction_Theorem and is_hyps  by blast
  then have "  xα⇙. B 𝒬 A"
  proof (cases "x = y")
    case True
    with * show ?thesis
      using identity_singleton_substitution_neutrality by force
  next
    case False
    from assms(4) have "(y, α)  free_vars (xα⇙. B)"
      using free_vars_in_all_vars by auto
    have "𝒬 S {(x, α)  yα} B  wffs⇘o⇙"
      by
        (
          fact hyp_derivable_form_is_wffso
          [OF *, THEN wffs_from_imp_op(1), THEN wffs_from_exists, THEN neg_wff]
        )
    moreover from False have "(x, α)  free_vars (𝒬 S {(x, α)  yα} B)"
      using free_var_in_renaming_substitution by simp
    moreover have "is_free_for (xα) (y, α) (𝒬 S {(x, α)  yα} B)"
      by (intro is_free_for_in_neg prop_5245_aux[OF False (y, α)  free_vars (xα⇙. B) assms(3)])
    moreover from assms(3,4) have "S {(y, α)  xα} S {(x, α)  yα} B = B"
      using identity_singleton_substitution_neutrality and renaming_substitution_composability
      by force
    ultimately have " (λyα⇙. 𝒬 S {(x, α)  yα} B) =⇘αo(λxα⇙. 𝒬 B)"
      using "α"[where A = "𝒬 S {(x, α)  yα} B"] by (metis derived_substitution_simps(4))
    then show ?thesis
      by (rule rule_RR[OF disjI1, where p = "[«,»,»,»]" and C = "?F"]) (use * in force)+
  qed
  with assms(1) show ?thesis
    by (rule MP)
qed

lemmas Rule_C = prop_5245 (* synonym *)

end