Theory Cantor

theory Cantor
  imports Calculus
begin


section ‹Example: Cantor's theorem›

text ‹Cantor's theorem is derived inside ‹NK› itself, in both forms and at every type
  ‹σ›: there is no surjection from ‹σ› onto ‹σ ❙⇒ 𝗈›, and no injection from ‹σ ❙⇒ 𝗈› into
  ‹σ›.  Both derivations go through the diagonal predicate; the injective one forms it
  with the description operator, by the rule ‹NK(ι)›, following Andrews \<^cite>‹Andrews72›.
  The Cantor sentences are stated as in the Stanford Encyclopedia entry on Church's type
  theory \<^cite>‹SEPChurchTT›, generalised from ‹ι› to every type ‹σ›.›

subsection ‹The Cantor sentences›

text ‹The Cantor sentences: no surjection
  ‹𝒢 : σ ❙⇒ σ ❙⇒ 𝗈› onto ‹σ ❙⇒ 𝗈›, and no injection ‹ℐ : (σ ❙⇒ 𝗈) ❙⇒ σ›.  The
  following lemmas record their locally-nameless normal forms (by computation) and
  the closedness facts used by the derivations.  The right-hand sides deliberately
  show the machine-level de Bruijn normal form (indices ‹Bnd 0›, ‹Bnd (Suc 0)›
  and so on); the named-binder left-hand sides are the human-facing statements.›

lemma surj_norm:
  "(❙∃𝒢⇘σ ❙⇒ σ ❙⇒ 𝗈⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙∃𝒳⇘σ⇙. ((𝒢⇧f⇘σ ❙⇒ σ ❙⇒ 𝗈⇙ ❙⋅ 𝒳⇧f⇘σ⇙) ❙=⇘σ ❙⇒ 𝗈⇙ ℱ⇧f⇘σ ❙⇒ 𝗈⇙))
   = ❙∃⇘σ ❙⇒ σ ❙⇒ 𝗈⇙ (❙Π⇘σ ❙⇒ 𝗈⇙ (❙∃⇘σ⇙
      ((Bnd (Suc (Suc 0)) ❙⋅ Bnd 0) ❙=⇘σ ❙⇒ 𝗈⇙ Bnd (Suc 0))))"
  by (simp add: ExN_def AllN_def 𝒢_def ℱ_def 𝒳_def)

lemma inj_norm:
  "(❙∃ℐ⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙Πℋ⇘σ ❙⇒ 𝗈⇙.
      (((ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℱ⇧f⇘σ ❙⇒ 𝗈⇙) ❙=⇘σ⇙ (ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℋ⇧f⇘σ ❙⇒ 𝗈⇙))
       ❙⊃ (ℱ⇧f⇘σ ❙⇒ 𝗈⇙ ❙=⇘σ ❙⇒ 𝗈⇙ ℋ⇧f⇘σ ❙⇒ 𝗈⇙)))
   = ❙∃⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ (❙Π⇘σ ❙⇒ 𝗈⇙ (❙Π⇘σ ❙⇒ 𝗈⇙
      (((Bnd (Suc (Suc 0)) ❙⋅ Bnd (Suc 0)) ❙=⇘σ⇙ (Bnd (Suc (Suc 0)) ❙⋅ Bnd
          0))
       ❙⊃ (Bnd (Suc 0) ❙=⇘σ ❙⇒ 𝗈⇙ Bnd 0))))"
  by (simp add: ExN_def AllN_def ℐ_def ℱ_def ℋ_def)

lemma wff_surj:
  "wff⇘𝗈⇙(❙∃𝒢⇘σ ❙⇒ σ ❙⇒ 𝗈⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙∃𝒳⇘σ⇙.
      ((𝒢⇧f⇘σ ❙⇒ σ ❙⇒ 𝗈⇙ ❙⋅ 𝒳⇧f⇘σ⇙) ❙=⇘σ ❙⇒ 𝗈⇙ ℱ⇧f⇘σ ❙⇒ 𝗈⇙))"
  by wffs

lemma wff_inj:
  "wff⇘𝗈⇙(❙∃ℐ⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙Πℋ⇘σ ❙⇒ 𝗈⇙.
      (((ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℱ⇧f⇘σ ❙⇒ 𝗈⇙) ❙=⇘σ⇙ (ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℋ⇧f⇘σ ❙⇒ 𝗈⇙))
       ❙⊃ (ℱ⇧f⇘σ ❙⇒ 𝗈⇙ ❙=⇘σ ❙⇒ 𝗈⇙ ℋ⇧f⇘σ ❙⇒ 𝗈⇙)))"
  by wffs

lemma fvs_surj [simp]:
  "fvs (❙¬ (❙∃𝒢⇘σ ❙⇒ σ ❙⇒ 𝗈⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙∃𝒳⇘σ⇙.
      ((𝒢⇧f⇘σ ❙⇒ σ ❙⇒ 𝗈⇙ ❙⋅ 𝒳⇧f⇘σ⇙) ❙=⇘σ ❙⇒ 𝗈⇙ ℱ⇧f⇘σ ❙⇒ 𝗈⇙))) = {}"
  by (simp add: surj_norm)

lemma fvs_inj [simp]:
  "fvs (❙¬ (❙∃ℐ⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙Πℋ⇘σ ❙⇒ 𝗈⇙.
      (((ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℱ⇧f⇘σ ❙⇒ 𝗈⇙) ❙=⇘σ⇙ (ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℋ⇧f⇘σ ❙⇒ 𝗈⇙))
       ❙⊃ (ℱ⇧f⇘σ ❙⇒ 𝗈⇙ ❙=⇘σ ❙⇒ 𝗈⇙ ℋ⇧f⇘σ ❙⇒ 𝗈⇙)))) = {}"
  by (simp add: inj_norm)

lemma pars_surj [simp]:
  "pars (❙∃𝒢⇘σ ❙⇒ σ ❙⇒ 𝗈⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙∃𝒳⇘σ⇙.
      ((𝒢⇧f⇘σ ❙⇒ σ ❙⇒ 𝗈⇙ ❙⋅ 𝒳⇧f⇘σ⇙) ❙=⇘σ ❙⇒ 𝗈⇙ ℱ⇧f⇘σ ❙⇒ 𝗈⇙)) = {}"
  by (simp add: surj_norm Forall_def)

lemma pars_inj [simp]:
  "pars (❙∃ℐ⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙Πℋ⇘σ ❙⇒ 𝗈⇙.
      (((ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℱ⇧f⇘σ ❙⇒ 𝗈⇙) ❙=⇘σ⇙ (ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℋ⇧f⇘σ ❙⇒ 𝗈⇙))
       ❙⊃ (ℱ⇧f⇘σ ❙⇒ 𝗈⇙ ❙=⇘σ ❙⇒ 𝗈⇙ ℋ⇧f⇘σ ❙⇒ 𝗈⇙))) = {}"
  by (simp add: inj_norm)

text ‹Typing of the terms occurring in the derivations, once and for all.›

lemma wff_surj_body:
  "wff⇘(σ ❙⇒ σ ❙⇒ 𝗈) ❙⇒ 𝗈⇙(❙Λ⇘σ ❙⇒ σ ❙⇒ 𝗈⇙ (❙Π⇘σ ❙⇒ 𝗈⇙ (❙∃⇘σ⇙
     ((Bnd (Suc (Suc 0)) ❙⋅ Bnd 0) ❙=⇘σ ❙⇒ 𝗈⇙ Bnd (Suc 0)))))"
  by (rule wff_AbsI)
     (auto del: wff_Not wff_Forall wff_PEq
           intro!: wff_Not wff_Forall wff_PEq wff_Eq wff_App wff_Fre)

lemma wff_inst_body:
  "wff⇘(σ ❙⇒ 𝗈) ❙⇒ 𝗈⇙(❙Λ⇘σ ❙⇒ 𝗈⇙ (❙∃⇘σ⇙
     ((Par g (σ ❙⇒ σ ❙⇒ 𝗈) ❙⋅ Bnd 0) ❙=⇘σ ❙⇒ 𝗈⇙ Bnd (Suc 0))))"
  by (rule wff_AbsI)
     (auto del: wff_Not wff_Forall wff_PEq
           intro!: wff_Not wff_Forall wff_PEq wff_Eq wff_App wff_Par wff_Fre)

lemma wff_diag:
  "wff⇘σ ❙⇒ 𝗈⇙(❙Λ⇘σ⇙ (❙¬ ((Par g (σ ❙⇒ σ ❙⇒ 𝗈) ❙⋅ Bnd 0) ❙⋅ Bnd 0)))"
  by (rule wff_AbsI) (auto del: wff_Not intro!: wff_Not wff_App wff_Par wff_Fre)

lemma wff_wit_body:
  assumes "wff⇘σ ❙⇒ 𝗈⇙(D)" and "lc D"
  shows "wff⇘σ ❙⇒ 𝗈⇙(❙Λ⇘σ⇙ ((Par g (σ ❙⇒ σ ❙⇒ 𝗈) ❙⋅ Bnd 0) ❙=⇘σ ❙⇒ 𝗈⇙ D))"
  using assms
  by (intro wff_AbsI) (auto del: wff_PEq intro!: wff_PEq wff_Eq wff_App wff_Par wff_Fre)

subsection ‹The surjective Cantor theorem in ‹NK››

theorem nk_surjective_cantor: fixes σ :: ty shows
  "⊢ (❙¬ (❙∃𝒢⇘σ ❙⇒ σ ❙⇒ 𝗈⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙∃𝒳⇘σ⇙.
     ((𝒢⇧f⇘σ ❙⇒ σ ❙⇒ 𝗈⇙ ❙⋅ 𝒳⇧f⇘σ⇙) ❙=⇘σ ❙⇒ 𝗈⇙ ℱ⇧f⇘σ ❙⇒ 𝗈⇙)) :: 'p::infinite tm)"
proof -
  ― ‹abbreviate the Cantor sentence under the negation›
  let ?S = "❙∃𝒢⇘σ ❙⇒ σ ❙⇒ 𝗈⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙∃𝒳⇘σ⇙.
     ((𝒢⇧f⇘σ ❙⇒ σ ❙⇒ 𝗈⇙ ❙⋅ 𝒳⇧f⇘σ⇙) ❙=⇘σ ❙⇒ 𝗈⇙ ℱ⇧f⇘σ ❙⇒ 𝗈⇙) :: 'p tm"
  ― ‹two distinct parameters: the assumed surjection ‹g›, the inner witness ‹a››
  obtain g a :: 'p where ag: "a ≠ g"
    by (metis (full_types) ex_new_if_finite finite.emptyI
        finite.insertI infinite_UNIV insert_iff)
  let ?gP = "g⇧p⇘σ ❙⇒ σ ❙⇒ 𝗈⇙ :: 'p tm" and ?aP = "a⇧p⇘σ⇙ :: 'p tm"
  ― ‹the diagonal ‹?F = ❙Λ𝒳. ❙¬ (g ❙⋅ 𝒳 ❙⋅ 𝒳)›; the two ‹❙∃›-assumptions;
    the diagonal instance ‹?φ = g ❙⋅ a ❙⋅ a››
  let ?F = "❙Λ⇘σ⇙ (❙¬ ((?gP ❙⋅ Bnd 0) ❙⋅ Bnd 0))"
  let ?Sg = "❙Π⇘σ ❙⇒ 𝗈⇙ (❙∃⇘σ⇙ ((?gP ❙⋅ Bnd 0) ❙=⇘σ ❙⇒ 𝗈⇙ Bnd (Suc 0)))"
  let ?E = "(?gP ❙⋅ ?aP) ❙=⇘σ ❙⇒ 𝗈⇙ ?F"
  let ?φ = "(?gP ❙⋅ ?aP) ❙⋅ ?aP"
  ― ‹bookkeeping, once and for all: typing and parameter-freshness›
  have wF: "wff⇘σ ❙⇒ 𝗈⇙(?F)" by (rule wff_diag)
  have lcF: "lc ?F" by (rule wff_lc[OF wF])
  have fp2: "freep {?S, ?Sg, ?E}"
    by (intro freep_finite) simp
  ― ‹the derivation, innermost context first›
  have 1: "{?S, ?Sg, ?E} ⊢ ?E"  ― ‹‹NK(Hyp)››
    by (auto intro: bprov.Hyp)
  have 2: "{?S, ?Sg, ?E} ⊢ ?φ ❙≐⇘𝗈⇙ (?F ❙⋅ ?aP)"
    ― ‹apply both sides of (1) to ‹a› --- ‹NK(=⇩l)›, Leibniz ‹NK(ΠE)››
    by (rule peq_app[OF 1 fp2]) (auto intro!: wff_App wff_Par wF)
  have 3: "?F ❙⋅ ?aP ≈⇘𝗈⇙ ❙¬ ?φ"  ― ‹‹β›-reduce the diagonal›
    using beq.beta[OF wF wff_Par] by simp
  have 4: "{?S, ?Sg, ?E} ⊢ ?φ ❙≐⇘𝗈⇙ (❙¬ ?φ)"  ― ‹‹NK(β)› on (2) by (3)›
    by (rule leib_reduce_right[OF 2 3]) (auto intro!: wff_App wff_Par)
  have 5: "{?S, ?Sg, ?E} ⊢ ❙⊥"
    ― ‹‹?φ ❙≐ ❙¬ ?φ› is contradictory --- ‹NK(ΠE)›, ‹NK(¬E)›, excluded middle›
    by (rule leib_neg_contra[OF 4 fp2]) (auto intro!: wff_App wff_Par)
  have 6: "{?S, ?Sg} ⊢ ?Sg"  ― ‹‹NK(Hyp)››
    by (auto intro: bprov.Hyp)
  have 7: "{?S, ?Sg} ⊢ ❙∃⇘σ⇙ ((?gP ❙⋅ Bnd 0) ❙=⇘σ ❙⇒ 𝗈⇙ ?F)"
    ― ‹‹NK(ΠE)›: instantiate the surjectivity of ‹g› at the diagonal ‹?F››
    using PiE_open[OF 6 wff_inst_body wF]
    by (simp add: opn_lc[OF lcF])
  have 8: "{?S, ?Sg} ⊢ ❙⊥"  ― ‹derived rule ‹ExE›, discharging the witness ‹a››
    by (rule ExE[where w = a, OF 7 _
          wff_wit_body[OF wF lcF] wff_FalseB])
      (use 5 ag in ‹auto simp: opn_lc[OF lcF] insert_commute
        intro!: freep_finite›)
  have 9: "{?S} ⊢ ❙∃⇘σ ❙⇒ σ ❙⇒ 𝗈⇙ (❙Π⇘σ ❙⇒ 𝗈⇙ (❙∃⇘σ⇙
      ((Bnd (Suc (Suc 0)) ❙⋅ Bnd 0) ❙=⇘σ ❙⇒ 𝗈⇙ Bnd (Suc 0))))"
    ― ‹‹NK(Hyp)›, in locally-nameless normal form›
    by (subst surj_norm[symmetric]) (auto intro: bprov.Hyp)
  have 10: "{?S} ⊢ ❙⊥"  ― ‹derived rule ‹ExE›, discharging the witness ‹g››
    by (rule ExE[where w = g, OF 9 _ wff_surj_body wff_FalseB])
      (use 8 in ‹auto simp: insert_commute intro!: freep_finite›)
  show ?thesis  ― ‹‹NK(¬I)› discharges the assumed surjection›
    by (rule bprov.NegI[OF _ wff_surj]) (use 10 in simp)
qed

subsection ‹The injective Cantor theorem in ‹NK››

text ‹Typing of the description-based diagonal predicate.›

lemma wff_desc_diag: 
  "wff⇘σ ❙⇒ 𝗈⇙(❙Λ⇘σ⇙ (❙¬ (((Iota (σ ❙⇒ 𝗈)) ❙⋅ (❙Λ⇘σ ❙⇒ 𝗈⇙ (((Par i ((σ ❙⇒ 𝗈) ❙⇒ σ)) ❙⋅
      Bnd 0) ❙≐⇘σ⇙ Bnd (Suc 0)))) ❙⋅ Bnd 0)))"
proof (rule wff_AbsI)
  fix x
  have inner: "wff⇘(σ ❙⇒ 𝗈) ❙⇒ 𝗈⇙(❙Λ⇘σ ❙⇒ 𝗈⇙ (((Par i ((σ ❙⇒ 𝗈) ❙⇒ σ)) ❙⋅ Bnd 0)
      ❙≐⇘σ⇙ x⇧f⇘σ⇙))"
    by (rule wff_AbsI)
       (auto del: wff_PEq wff_LeibE wff_Leib
             intro!: wff_LeibE wff_Leib wff_PEq wff_Eq wff_App wff_Par wff_Fre)
  show "wff⇘𝗈⇙((❙¬ (((Iota (σ ❙⇒ 𝗈)) ❙⋅
     (❙Λ⇘σ ❙⇒ 𝗈⇙ (((Par i ((σ ❙⇒ 𝗈) ❙⇒ σ)) ❙⋅ Bnd 0) ❙≐⇘σ⇙ Bnd (Suc 0)))) ❙⋅ Bnd
         0))❙⟨x⇧f⇘σ⇙❙⟩)"
    using inner by (auto del: wff_Not intro!: wff_Not wff_App wff_Iota wff_Fre)
qed


theorem nk_injective_cantor: fixes σ :: ty shows 
  "⊢ (❙¬ (❙∃ℐ⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙Πℋ⇘σ ❙⇒ 𝗈⇙.
     (((ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℱ⇧f⇘σ ❙⇒ 𝗈⇙) ❙=⇘σ⇙ (ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℋ⇧f⇘σ ❙⇒ 𝗈⇙))
      ❙⊃ (ℱ⇧f⇘σ ❙⇒ 𝗈⇙ ❙=⇘σ ❙⇒ 𝗈⇙ ℋ⇧f⇘σ ❙⇒ 𝗈⇙))) :: 'p::infinite tm)"
proof -
  ― ‹abbreviate the Cantor sentence under the negation›
  let ?S = "❙∃ℐ⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙Πℋ⇘σ ❙⇒ 𝗈⇙.
     (((ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℱ⇧f⇘σ ❙⇒ 𝗈⇙) ❙=⇘σ⇙ (ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℋ⇧f⇘σ ❙⇒ 𝗈⇙))
      ❙⊃ (ℱ⇧f⇘σ ❙⇒ 𝗈⇙ ❙=⇘σ ❙⇒ 𝗈⇙ ℋ⇧f⇘σ ❙⇒ 𝗈⇙)) :: 'p tm"
  ― ‹The same structure as for the surjective theorem, with the diagonal
    formed through the description operator: steps (1)-(2) instantiate the
    assumed injectivity; step (3) shows that, by injectivity, the singleton
    predicate ‹❙ΛH. i ❙⋅ H ❙≐ a› of the image point ‹a = i ❙⋅ ?G› is the
    Leibniz singleton of the diagonal ‹?G = ❙Λx. ❙¬ (❙ι(❙ΛH. i ❙⋅ H ❙≐ x) ❙⋅ x)›,
    so that by ‹NK(ι)› its description is ‹?G› itself (step (4)): description
    recovers ‹?G› from its image under ‹i›; step (5) ‹β›-reduces the diagonal at
    ‹a›, step (6) derives the contradiction ‹?ψ ❙≐ ❙¬ ?ψ› and closes the context;
    steps (7)-(8) and ‹NK(¬I)› discharge the assumption.›
  obtain i h :: 'p where hi: "h ≠ i"
    by (metis (full_types) ex_new_if_finite finite.emptyI
        finite.insertI infinite_UNIV insert_iff)
  let ?τ = "(σ ❙⇒ 𝗈) ❙⇒ σ"
  let ?iP = "i⇧p⇘?τ⇙ :: 'p tm" and ?hP = "h⇧p⇘σ ❙⇒ 𝗈⇙ :: 'p tm"
  let ?G = "❙Λ⇘σ⇙ (❙¬ (((Iota (σ ❙⇒ 𝗈)) ❙⋅ (❙Λ⇘σ ❙⇒ 𝗈⇙ ((?iP ❙⋅ Bnd 0) ❙≐⇘σ⇙ Bnd (Suc 0)))) ❙⋅ Bnd 0))"
  let ?a = "?iP ❙⋅ ?G"
  let ?PX = "❙Λ⇘σ ❙⇒ 𝗈⇙ ((?iP ❙⋅ Bnd 0) ❙≐⇘σ⇙ ?a)"
  let ?LG = "(Leib (σ ❙⇒ 𝗈)) ❙⋅ ?G"
  let ?ψ = "((Iota (σ ❙⇒ 𝗈)) ❙⋅ ?PX) ❙⋅ ?a"
  let ?IBb = "❙Π⇘σ ❙⇒ 𝗈⇙ (❙Π⇘σ ❙⇒ 𝗈⇙
    (((Bnd (Suc (Suc 0)) ❙⋅ Bnd (Suc 0)) ❙=⇘σ⇙ (Bnd (Suc (Suc 0)) ❙⋅ Bnd
        0))
     ❙⊃ (Bnd (Suc 0) ❙=⇘σ ❙⇒ 𝗈⇙ Bnd 0)))"
  let ?IB = "❙Π⇘σ ❙⇒ 𝗈⇙ (❙Π⇘σ ❙⇒ 𝗈⇙
    (((?iP ❙⋅ Bnd (Suc 0)) ❙=⇘σ⇙ (?iP ❙⋅ Bnd 0))
     ❙⊃ (Bnd (Suc 0) ❙=⇘σ ❙⇒ 𝗈⇙ Bnd 0)))"
  let ?Γ = "{?S, ?IB}"
  have wG: "wff⇘σ ❙⇒ 𝗈⇙(?G)"
    using wff_desc_diag[where σ = σ and i = i] by simp
  ― ‹bookkeeping, once and for all: typing, local closure, freshness›
  have lcG: "lc ?G" by (rule wff_lc[OF wG])
  have wa: "wff⇘σ⇙(?a)" by (auto intro!: wff_App wff_Par wG)
  have lca: "lc ?a" by (rule wff_lc[OF wa])
  have wPX: "wff⇘(σ ❙⇒ 𝗈) ❙⇒ 𝗈⇙(?PX)"
    by (rule wff_AbsI)
       (auto del: wff_LeibE simp: opn_lc[OF lca]
             intro!: wff_LeibE wff_App wff_Par wff_Fre wa wG)
  have wLG: "wff⇘(σ ❙⇒ 𝗈) ❙⇒ 𝗈⇙(?LG)"
    by (auto del: wff_Leib intro!: wff_App wff_Leib wG)
  have wIo: "wff⇘σ ❙⇒ 𝗈⇙((Iota (σ ❙⇒ 𝗈)) ❙⋅ ?PX)"
    by (auto intro!: wff_App wff_Iota wPX)
  have wψ: "wff⇘𝗈⇙(?ψ)" by (rule wff_App[OF wIo wa])
  have wIBb: "wff⇘((σ ❙⇒ 𝗈) ❙⇒ σ) ❙⇒ 𝗈⇙(❙Λ⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ?IBb :: 'p tm)"
    by (rule wff_AbsI)
       (auto del: wff_Forall wff_ImpB wff_LeibE wff_Leib wff_PEq
             intro!: wff_Forall wff_ImpB wff_LeibE wff_Leib wff_PEq wff_Eq wff_App wff_Fre)
  have fpΓ: "freep ?Γ" by (intro freep_finite) simp
  ― ‹the derivation›
  have 1: "?Γ ⊢ ?IB"  ― ‹‹NK(Hyp)››
    by (auto intro: bprov.Hyp)
  have 2: "?Γ ⊢ ((?iP ❙⋅ F) ❙=⇘σ⇙ (?iP ❙⋅ H)) ❙⊃ (F ❙=⇘σ ❙⇒ 𝗈⇙ H)"
    if wF: "wff⇘σ ❙⇒ 𝗈⇙(F)" and wH: "wff⇘σ ❙⇒ 𝗈⇙(H)"
      and lcF: "lc F" and lcH: "lc H" for F H
    ― ‹instantiate (1) at closed ‹F›, ‹H›: twice ‹NK(ΠE)›, each followed by ‹NK(β)››
  proof -
    let ?B1 = "❙Π⇘σ ❙⇒ 𝗈⇙ (((?iP ❙⋅ Bnd (Suc 0)) ❙=⇘σ⇙ (?iP ❙⋅ Bnd 0))
        ❙⊃ (Bnd (Suc 0) ❙=⇘σ ❙⇒ 𝗈⇙ Bnd 0))"
    have wB1: "wff⇘(σ ❙⇒ 𝗈) ❙⇒ 𝗈⇙(❙Λ⇘σ ❙⇒ 𝗈⇙ ?B1)"
      by (rule wff_AbsI)
         (auto del: wff_ImpB intro!: wff_ImpB wff_Eq wff_App wff_Par wff_Fre)
    have bq1: "(❙Λ⇘σ ❙⇒ 𝗈⇙ ?B1) ❙⋅ F ≈⇘𝗈⇙
          ❙Π⇘σ ❙⇒ 𝗈⇙ (((?iP ❙⋅ F) ❙=⇘σ⇙ (?iP ❙⋅ Bnd 0)) ❙⊃ (F ❙=⇘σ ❙⇒ 𝗈⇙ Bnd 0))"
      using beq.beta[OF wB1 wF] by (simp add: opn_lc[OF lcF])
    have wB2: "wff⇘(σ ❙⇒ 𝗈) ❙⇒ 𝗈⇙(❙Λ⇘σ ❙⇒ 𝗈⇙
        (((?iP ❙⋅ F) ❙=⇘σ⇙ (?iP ❙⋅ Bnd 0)) ❙⊃ (F ❙=⇘σ ❙⇒ 𝗈⇙ Bnd 0)))"
      by (rule wff_AbsI)
         (auto simp: opn_lc[OF lcF] del: wff_ImpB
               intro!: wff_ImpB wff_Eq wff_App wff_Par wff_Fre wF)
    have bq2: "(❙Λ⇘σ ❙⇒ 𝗈⇙
        (((?iP ❙⋅ F) ❙=⇘σ⇙ (?iP ❙⋅ Bnd 0)) ❙⊃ (F ❙=⇘σ ❙⇒ 𝗈⇙ Bnd 0))) ❙⋅ H ≈⇘𝗈⇙
        ((?iP ❙⋅ F) ❙=⇘σ⇙ (?iP ❙⋅ H)) ❙⊃ (F ❙=⇘σ ❙⇒ 𝗈⇙ H)"
      using beq.beta[OF wB2 wH] by (simp add: opn_lc[OF lcF]
          opn_lc[OF lcH])
    show ?thesis by (rule bprov.Beta[OF bq2 PiE_Forall[OF
        bprov.Beta[OF bq1 PiE_Forall[OF 1 wF]] wH]])
  qed
  have 3: "?Γ ⊢ ?PX ❙≐⇘(σ ❙⇒ 𝗈) ❙⇒ 𝗈⇙ ?LG"
    ― ‹by injectivity, the singleton predicate of ‹?a› is the Leibniz
      singleton of ‹?G›: pointwise by ‹NK(b)›, closed by ‹NK(ΠI)›
      and ‹NK(f)››
  proof -
    let ?body = "(?PX ❙⋅ Bnd 0) ❙≐⇘𝗈⇙ (?LG ❙⋅ Bnd 0)"
    have wbody: "wff⇘(σ ❙⇒ 𝗈) ❙⇒ 𝗈⇙(❙Λ⇘σ ❙⇒ 𝗈⇙ ?body)"
      by (rule wff_AbsI) (auto simp: opn_lc[OF wff_lc[OF wPX]]
          opn_lc[OF wff_lc[OF wLG]]
          intro!: wff_Eq wff_App wff_Fre
              wPX wLG wG)
    have A_beta: "?PX ❙⋅ ?hP ≈⇘𝗈⇙ ((?iP ❙⋅ ?hP) ❙≐⇘σ⇙ ?a)"  ― ‹‹NK(β)››
      using beq.beta[OF wPX wff_Par] by (simp add: opn_lc[OF lca])
    have wA: "wff⇘𝗈⇙(?PX ❙⋅ ?hP)" by (auto intro!: wff_App wPX wff_Par)
    have wB: "wff⇘𝗈⇙(?LG ❙⋅ ?hP)"
      by (auto intro!: wff_App wLG wff_Par wG)
    have wih: "wff⇘σ⇙(?iP ❙⋅ ?hP)" by (auto intro!: wff_App wff_Par)
    have dir1: "?Γ ∪ {?PX ❙⋅ ?hP} ⊢ ?LG ❙⋅ ?hP"
      ― ‹if ‹h› is in the singleton then ‹i ❙⋅ h ❙= i ❙⋅ ?G›, so ‹h ❙= ?G›
        by the injectivity instance (2) and ‹bprov_ImpE››
    proof -
      let ?Δ = "?Γ ∪ {?PX ❙⋅ ?hP}"
      have fpΔ: "freep ?Δ" by (intro freep_finite) simp
      have d1: "?Δ ⊢ ?PX ❙⋅ ?hP" by (auto intro: bprov.Hyp)
      have imp: "?Δ ⊢ ((?iP ❙⋅ ?hP) ❙=⇘σ⇙ ?a) ❙⊃ (?hP ❙=⇘σ ❙⇒ 𝗈⇙ ?G)"
        by (rule bprov_weaken[OF 2[OF wff_Par wG wff_lc[OF wff_Par]
            lcG] _ fpΔ]) auto
      have "?Δ ⊢ ?hP ❙=⇘σ ❙⇒ 𝗈⇙ ?G"
        by (rule bprov_ImpE[OF imp leib_to_peq[OF bprov.Beta[OF
            A_beta d1] fpΔ wih wa] fpΔ])
           (auto intro!: wih wa wff_Par wG)
      hence "?Δ ⊢ ?hP ❙≐⇘σ ❙⇒ 𝗈⇙ ?G" by (rule bprov.EqL)
      hence "?Δ ⊢ ?G ❙≐⇘σ ❙⇒ 𝗈⇙ ?hP"
        by (rule leib_sym[OF _ fpΔ wff_Par wG])
      thus ?thesis by simp
    qed
    have dir2: "?Γ ∪ {?LG ❙⋅ ?hP} ⊢ ?PX ❙⋅ ?hP"
      ― ‹conversely, Leibniz-equals of ‹?G› lie in the singleton --- by
        congruence and ‹NK(β)››
    proof -
      let ?Δ = "?Γ ∪ {?LG ❙⋅ ?hP}"
      have fpΔ: "freep ?Δ" by (intro freep_finite) simp
      have d1: "?Δ ⊢ ?G ❙≐⇘σ ❙⇒ 𝗈⇙ ?hP" by (auto intro: bprov.Hyp)
      show ?thesis by (rule bprov.Beta[OF beq.sym[OF A_beta]
          leib_cong2[OF leib_sym[OF d1 fpΔ wG wff_Par] fpΔ wff_Par
              wG wff_Par]])
    qed
    have bqh: "(❙Λ⇘σ ❙⇒ 𝗈⇙ ?body) ❙⋅ ?hP ≈⇘𝗈⇙ (?PX ❙⋅ ?hP) ❙≐⇘𝗈⇙ (?LG ❙⋅ ?hP)"
      using beq.beta[OF wbody wff_Par]
      by (simp add: opn_lc[OF wff_lc[OF wPX]] opn_lc[OF wff_lc[OF
          wLG]])
    have allh: "?Γ ⊢ ❙Π⇘σ ❙⇒ 𝗈⇙ ?body"
      ― ‹‹NK(b)›, then ‹NK(ΠI)› at the fresh ‹h››
      by (rule PiI_Forall[OF bprov.Beta[OF beq.sym[OF bqh]
          bprov.BoolE[OF dir1 dir2 wA wB]] wbody])
        (use hi in ‹auto simp: Leib_def›)
    show ?thesis  ― ‹‹NK(f)›: functional extensionality›
      by (rule bprov.FuncE[OF allh wPX wLG])
  qed
  have 4: "?Γ ⊢ ((Iota (σ ❙⇒ 𝗈)) ❙⋅ ?PX) ❙≐⇘σ ❙⇒ 𝗈⇙ ?G"
    ― ‹‹NK(ι)›: description maps the Leibniz singleton --- and by (3)
      the singleton predicate of ‹?a› --- to ‹?G› itself›
    by (rule leib_trans[OF leib_cong2[OF 3 fpΓ wPX wLG wff_Iota]
          bprov.Desc[OF wG] fpΓ])
      (auto intro!: wff_App wff_Iota wPX wLG wG)
  have 5: "?G ❙⋅ ?a ≈⇘𝗈⇙ ❙¬ ?ψ"  ― ‹‹β›-reduce the diagonal at ‹?a››
    using beq.beta[OF wG wa] by (simp add: opn_lc[OF lca])
  have 6: "?Γ ⊢ ❙⊥"
    ― ‹apply (4) at ‹?a›, ‹β›-reduce by (5): ‹?ψ ❙≐ ❙¬ ?ψ›, contradictory
      --- ‹NK(ΠE)›, ‹NK(¬E)›, excluded middle›
    by (rule leib_neg_contra[OF bprov.Beta[OF beq.appR[OF 5
          wff_App[OF wff_Leib wψ]]
          leib_cong1[OF 4 fpΓ wIo wG wa]] fpΓ wψ])
  have 7: "{?S} ⊢ ❙∃⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ?IBb"
    ― ‹‹NK(Hyp)›, in locally-nameless normal form›
    by (subst inj_norm[symmetric]) (auto intro: bprov.Hyp)
  have 8: "{?S} ⊢ ❙⊥"  ― ‹derived rule ‹ExE›, discharging the witness ‹i››
  proof (rule ExE[where w = i, OF 7 _ wIBb wff_FalseB], goal_cases)
    case 1 show ?case using 6 by (simp add: insert_commute)
    next case 2 show ?case
      by (simp add: Leib_def ImpB_def Forall_def)
    next case 3 show ?case by (simp add: FalseB_def Forall_def)
    next case 4 show ?case by auto
    next case 5 show ?case by (intro freep_finite) simp
  qed
  show ?thesis  ― ‹‹NK(¬I)› discharges the assumed injection›
    by (rule bprov.NegI[OF _ wff_inj]) (use 8 in simp)
qed

end