Theory Cantor

theory Cantor
  imports Consistency
begin


section ‹Example: Cantor's theorem›

text ‹The surjective and the injective Cantor theorem, at every type ‹σ›: there is no
  surjection from ‹σ› onto ‹σ ❙⇒ 𝗈›, and no injection from ‹σ ❙⇒ 𝗈› into ‹σ›.  Both are
  derived @{emph ‹inside the calculus›}: genuine ‹NK›-derivations via the diagonal
  predicate (for the injective version via the description operator ‹NK(ι)›, following
  Andrews 1972).  The Cantor sentences are stated as in the @{emph ‹Stanford
  Encyclopedia of Philosophy›} entry on Church's type theory (Benzm\"uller and
  Andrews 2024), generalised from ‹ι› to every type ‹σ›.›

subsection ‹The defined existential quantifier, and the Cantor sentences›

text ‹The Cantor sentences are stated literally, as in the cited encyclopedia entry: 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⇘σ ❙⇒ 𝗈⇙))"
  unfolding surj_norm
  by (intro wff_Not wff_Forall)
     (auto del: wff_Not wff_PEq wff_Forall
           intro!: wff_Not wff_Forall wff_PEq wff_Eq wff_App wff_Fre)

lemma wff_inj:
  "wff⇘𝗈⇙(❙∃ℐ⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙. ❙Πℱ⇘σ ❙⇒ 𝗈⇙. ❙Πℋ⇘σ ❙⇒ 𝗈⇙.
      (((ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℱ⇧f⇘σ ❙⇒ 𝗈⇙) ❙=⇘σ⇙ (ℐ⇧f⇘(σ ❙⇒ 𝗈) ❙⇒ σ⇙ ❙⋅ ℋ⇧f⇘σ ❙⇒ 𝗈⇙))
       ❙⊃ (ℱ⇧f⇘σ ❙⇒ 𝗈⇙ ❙=⇘σ ❙⇒ 𝗈⇙ ℋ⇧f⇘σ ❙⇒ 𝗈⇙)))"
  unfolding inj_norm
  by (intro wff_Not wff_Forall)
     (auto del: wff_Not wff_Forall wff_ImpB wff_PEq
           intro!: wff_Not wff_Forall wff_ImpB wff_PEq wff_Eq wff_App wff_Fre)

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)"
    (is "⊢ ❙¬ ?S")
proof -
  ― ‹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 fp1: "freep {?S, ?Sg}" and 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)›, tertium non datur›
    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} ⊢ ❙⊥"  ― ‹‹NK(∃E)›, 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} ⊢ ❙⊥"  ― ‹‹NK(∃E)›, 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)"
  (is "⊢ ❙¬ ?S")
proof -
  ― ‹The same narrative 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 ‹NK(ι)› describes it to ‹?G› itself (step (4)) --- description inverts
    ‹i›; steps (5)-(6) derive the diagonal contradiction ‹?ψ ❙≐ ❙¬ ?ψ›;
    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 ‹NK(⊃E)››
    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)›, tertium non datur›
    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} ⊢ ❙⊥"  ― ‹‹NK(∃E)›, 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