Quelle  AOT_misc.thy

theory AOT_misc
  imports AOT_NaturalNumbers
begin

section‹Miscellaneous Theorems›

AOT_theorem PossiblyNumbersEmptyPropertyImpliesZero:
  ‹♢Numbers(x,[λz O!z & z ≠_E z]) → x = 0›
proof(rule "→I")
  AOT_have ‹Rigid([λz O!z & z ≠_E z])›
  proof (safe intro!: "df-rigid-rel:1"[THEN "≡_dfI"] "&I" "cqt:2";
         rule RN; safe intro!: GEN "→I")
    AOT_modally_strict {
      fix x
      AOT_assume ‹[λz O!z & z ≠_E z]x›
      AOT_hence ‹O!x & x ≠_E x› by (rule "β→C")
      moreover AOT_have ‹x =_E x› using calculation[THEN "&E"(1)] 
        by (metis "ord=Eequiv:1" "vdash-properties:10")
      ultimately AOT_have ‹x =_E x & ¬x =_E x›
        by (metis "con-dis-i-e:1" "con-dis-i-e:2:b" "intro-elim:3:a" "thm-neg=E")
      AOT_thus ‹◻[λz O!z & z ≠_E z]x› using "raa-cor:1" by blast
    }
  qed
  AOT_hence ‹◻∀x (Numbers(x,[λz O!z & z ≠_E z]) → ◻Numbers(x,[λz O!z & z ≠_E z]))›
    by (safe intro!: "num-cont:2"[unvarify G, THEN "→E"] "cqt:2")
  AOT_hence ‹∀x ◻(Numbers(x,[λz O!z & z ≠_E z]) → ◻Numbers(x,[λz O!z & z ≠_E z]))›
    using "BFs:2"[THEN "→E"] by blast
  AOT_hence ‹◻(Numbers(x,[λz O!z & z ≠_E z]) → ◻Numbers(x,[λz O!z & z ≠_E z]))›
    using "∀E"(2) by auto
  moreover AOT_assume ‹♢Numbers(x,[λz O!z & z ≠_E z])›
  ultimately AOT_have ‹\ANumbers(x,[λz O!z & z ≠_E z])›
    using "sc-eq-box-box:1"[THEN "≡E"(1), THEN "→E", THEN "nec-imp-act"[THEN "→E"]]
    by blast
  AOT_hence ‹Numbers(x,[λz \A[λz O!z & z ≠_E z]z])›
    by (safe intro!: "eq-num:1"[unvarify G, THEN "≡E"(1)] "cqt:2")
  AOT_hence ‹x = #[λz O!z & z ≠_E z]›
    by (safe intro!: "eq-num:2"[unvarify G, THEN "≡E"(1)] "cqt:2")
  AOT_thus ‹x = 0›
    using "cqt:2"(1) "rule-id-df:2:b[zero]" "rule=E" "zero:1" by blast
qed

AOT_define Numbers' :: ‹τ ==> τ ==> φ› (‹Numbers'''(_,_')›)
  ‹Numbers'(x, G) ≡_df A!x & G↓ & ∀F (x[F] ≡ F ≈_E G)›
AOT_theorem Numbers'equiv: ‹Numbers'(x,G) ≡ A!x & ∀F (x[F] ≡ F ≈_E G)›
  by (AOT_subst_def Numbers')
     (auto intro!: "≡I" "→I" "&I" "cqt:2" dest: "&E")

AOT_theorem Numbers'DistinctZeroes:
  ‹∃x∃y (♢Numbers'(x,[λz O!z & z ≠_E z]) & ♢Numbers'(y,[λz O!z & z ≠_E z]) & x ≠ y)›
proof -
  AOT_obtain w₁ where ‹∃w w₁ ≠ w›
    using "two-worlds-exist:4" "PossibleWorld.∃E"[rotated] by fast
  then AOT_obtain w₂ where distinct_worlds: ‹w₁ ≠ w₂›
    using "PossibleWorld.∃E"[rotated] by blast
  AOT_obtain x where x_prop:
    ‹A!x & ∀F (x[F] ≡ w₁ ⊨ F ≈_E [λz O!z & z ≠_E z])›
    using "A-objects"[axiom_inst] "∃E"[rotated] by fast
  moreover AOT_obtain y where y_prop:
    ‹A!y & ∀F (y[F] ≡ w₂ ⊨ F ≈_E [λz O!z & z ≠_E z])›
    using "A-objects"[axiom_inst] "∃E"[rotated] by fast
  moreover {
    fix x w
    AOT_assume x_prop: ‹A!x & ∀F (x[F] ≡ w ⊨ F ≈_E [λz O!z & z pan style='font-size: 18px;'>≠_E z])›
    AOT_have ‹∀F w ⊨ (x[F] ≡ F ≈_E [λz O!z & z ≠_E z])›
    proof(safe intro!: GEN "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
                              OF "log-prop-prop:2",THEN "≡E"(2)] "≡I" "→I")
      fix F
      AOT_assume ‹w ⊨ x[F]›
      AOT_hence ‹♢x[F]›
        using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(2),
                       OF "PossibleWorld.∃I"] by blast
      AOT_hence ‹x[F]›
        by (metis "en-eq:3[1]" "intro-elim:3:a")
      AOT_thus ‹w ⊨ (F ≈_E [λz O!z & z ≠_E z])›
        using x_prop[THEN "&E"(2), THEN "∀E"(2), THEN "≡E"(1)] by blast
    next
      fix F
      AOT_assume ‹w ⊨ (F ≈_E [λz O!z & z ≠_E z])›
      AOT_hence ‹x[F]›
        using x_prop[THEN "&E"(2), THEN "∀E"(2), THEN "≡E"(2)] by blast
      AOT_hence ‹◻x[F]›
        using "pre-en-eq:1[1]"[THEN "→E"] by blast
      AOT_thus ‹w ⊨ x[F]›
        using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)]
              "PossibleWorld.∀E" by fast
    qed
    AOT_hence ‹w ⊨ ∀F (x[F] ≡ F ≈_E [λz O!z & z ≠_E z])›
      using "conj-dist-w:5"[THEN "≡E"(2)] by fast
    moreover {
      AOT_have ‹◻[λz O!z & z ≠_E z]↓›
        by (safe intro!: RN "cqt:2")
      AOT_hence ‹w ⊨ [λz O!z & z ≠_E z]↓›
        using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1),
                       THEN "PossibleWorld.∀E"] by blast
    }
    moreover {
      AOT_have ‹◻A!x›
        using x_prop[THEN "&E"(1)] by (metis "oa-facts:2" "→E")
      AOT_hence ‹w ⊨ A!x›
        using "fund:2"[unvarify p, OF "log-prop-prop:2",
                       THEN "≡E"(1), THEN "PossibleWorld.∀E"] by blast
    }
    ultimately AOT_have ‹w ⊨ (A!x & [λz O!z & z ≠_E z]↓ &
 ∀F (x[F] ≡ F ≈_E [λz O!z & z ≠_E z]))›
      using "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
              OF "log-prop-prop:2", THEN "≡E"(2), OF "&I"] by auto
    AOT_hence ‹∃w w ⊨ (A!x & [λz O!z & z ≠_E z]↓ &
 ∀F (x[F] ≡ F ≈_E [λz O!z & z ≠_E z]))›
      using "PossibleWorld.∃I" by auto
    AOT_hence ‹♢(A!x & [λz O!z & z ≠_E z]↓ & ∀F (x[F] ≡ F ≈_E [λz O!z & z ≠_E z]))›
      using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(2)] by blast
    AOT_hence ‹♢Numbers'(x,[λz O!z & z ≠_E z])›
      by (AOT_subst_def Numbers')
  }
  ultimately AOT_have ‹♢Numbers'(x,[λz O!z & z ≠_E z])›
                  and ‹♢Numbers'(y,[λz O!z & z ≠_E z])›
    by auto
  moreover AOT_have ‹x ≠ y›
  proof (rule "ab-obey:2"[THEN "→E"])
    AOT_have ‹◻¬∃u [λz O!z & z ≠_E z]u›
    proof (safe intro!: RN "raa-cor:2")
      AOT_modally_strict {
        AOT_assume ‹∃u [λz O!z & z ≠_E z]u›
        then AOT_obtain u where ‹[λz O!z & z ≠_E z]u›
          using "Ordinary.∃E"[rotated] by blast
        AOT_hence ‹O!u & u ≠_E u›
          by (rule "β→C")
        AOT_hence ‹¬(u =_E u)›
          by (metis "con-dis-taut:2" "intro-elim:3:d" "modus-tollens:1"
                    "raa-cor:3" "thm-neg=E")
        AOT_hence ‹u =_E u & ¬u =_E u›
          by (metis "modus-tollens:1" "ord=Eequiv:1" "raa-cor:3" Ordinary.ψ)
        AOT_thus ‹p & ¬p› for p
          by (metis "raa-cor:1")
      }
    qed
    AOT_hence nec_not_ex: ‹∀w w ⊨ ¬∃u [λz O!z & z ≠_E z]u›
      using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
    AOT_have ‹◻([λy p]x ≡ p)› for x p
      by (safe intro!: RN "beta-C-meta"[THEN "→E"] "cqt:2")
    AOT_hence ‹∀w w ⊨ ([λy p]x ≡ p)› for x p
      using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
    AOT_hence world_prop_beta: ‹∀w (w ⊨ [λy p]x ≡ w ⊨ p)› for x p
      using "conj-dist-w:4"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)]
            "PossibleWorld.∀E" "PossibleWorld.∀I" by meson

    AOT_have ‹∃p (w₁ ⊨ p & ¬w₂ ⊨ p)›
    proof(rule "raa-cor:1")
      AOT_assume 0: ‹¬∃p (w₁ ⊨ p & ¬w₂ ⊨ p)›
      AOT_have 1: ‹w₁ ⊨ p → w₂ ⊨ p› for p
      proof(safe intro!: GEN "→I")
        AOT_assume ‹w₁ ⊨ p›
        AOT_thus ‹w₂ ⊨ p›
          using 0 "con-dis-i-e:1" "∃I"(2) "raa-cor:4" by fast
      qed
      moreover AOT_have ‹w₂ ⊨ p → w₁ ⊨ p› for p
      proof(safe intro!: GEN "→I")
        AOT_assume ‹w₂ ⊨ p›
        AOT_hence ‹¬w₂ ⊨ ¬p›
          using "coherent:2" "intro-elim:3:a" by blast
        AOT_hence ‹¬w₁ ⊨ ¬p›
          using 1["∀I" p, THEN "∀E"(1), OF "log-prop-prop:2"]
          by (metis "modus-tollens:1")
        AOT_thus ‹w₁ ⊨ p›
          using "coherent:1" "intro-elim:3:b" "reductio-aa:1" by blast
      qed
      ultimately AOT_have ‹w₁ ⊨ p ≡ w₂ ⊨ p› for p
        by (metis "intro-elim:2")
      AOT_hence ‹w₁ = w₂›
        using "sit-identity"[unconstrain s, THEN "→E",
            OF PossibleWorld.ψ[THEN "world:1"[THEN "≡_dfE"], THEN "&E"(1)],
            unconstrain s', THEN "→E",
            OF PossibleWorld.ψ[THEN "world:1"[THEN "≡_dfE"], THEN "&E"(1)],
            THEN "≡E"(2)] GEN by fast
      AOT_thus ‹w₁ = w₂ & ¬w₁ = w₂›
        using  "=-infix" "≡_dfE" "con-dis-i-e:1" distinct_worlds by blast
    qed
    then AOT_obtain p where 0: ‹w₁ ⊨ p & ¬w₂ ⊨ p›
      using "∃E"[rotated] by blast
    AOT_have ‹y[λy p]›
    proof (safe intro!: y_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(2)] "cqt:2")
      AOT_show ‹w₂ ⊨ [λy p] ≈_E [λz O!z & z ≠_E z]›
      proof (safe intro!:  "cqt:2" "empty-approx:1"[unvarify F H, THEN RN,
                  THEN "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)],
                  THEN "PossibleWorld.∀E",
                  THEN "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2",
                                       OF "log-prop-prop:2", THEN "≡E"(1)],
                                       THEN "→E"]
                  "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
                                  OF "log-prop-prop:2", THEN "≡E"(2)] "&I")
        AOT_have ‹¬w₂ ⊨ ∃u [λy p]u›
        proof (rule "raa-cor:2")
          AOT_assume ‹w₂ ⊨ ∃u [λy p]u›
          AOT_hence ‹∃x w₂ ⊨ (O!x & [λy p]x)›
            by (metis "conj-dist-w:6" "intro-elim:3:a")
          then AOT_obtain x where ‹w₂ ⊨ (O!x & [λy p]x)›
            using "∃E"[rotated] by blast
          AOT_hence ‹w₂ ⊨ [λy p]x›
            using "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
                    OF "log-prop-prop:2", THEN "≡E"(1), THEN "&E"(2)] by blast
          AOT_hence ‹w₂ ⊨ p›
            using world_prop_beta[THEN "PossibleWorld.∀E", THEN "≡E"(1)] by blast
          AOT_thus ‹w₂ ⊨ p & ¬w₂ ⊨ p›
            using 0[THEN "&E"(2)] "&I" by blast
        qed
        AOT_thus ‹w₂ ⊨ ¬∃u [λy p]u›
          by (safe intro!: "coherent:1"[unvarify p, OF "log-prop-prop:2",
                                        THEN "≡E"(2)])
      next
        AOT_show ‹w₂ ⊨ ¬∃v [λz O!z & z ≠_E z]v›
          using nec_not_ex[THEN "PossibleWorld.∀E"] by blast
      qed
    qed
    moreover AOT_have ‹¬x[λy p]›
    proof(rule "raa-cor:2")
      AOT_assume ‹x[λy p]›
      AOT_hence "w₁ ⊨ [λy p] ≈_E [λz O!z & z ≠_E z]"
        using x_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(1)]
              "prop-prop2:2" by blast
      AOT_hence "¬w₁ ⊨ ¬[λy p] ≈_E [λz O!z & z ≠_E z]"
        using "coherent:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
      moreover AOT_have "w₁ ⊨ ¬([λy p] ≈_E [λz O!z & z ≠_E z])"
      proof (safe intro!: "cqt:2" "empty-approx:2"[unvarify F H, THEN RN,
                    THEN "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)],
                    THEN "PossibleWorld.∀E",
                    THEN "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2",
                        OF "log-prop-prop:2", THEN "≡E"(1)], THEN "→E"]
                    "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
                                    OF "log-prop-prop:2", THEN "≡E"(2)] "&I")
        fix u
        AOT_have ‹w₁ ⊨ O!u›
          using Ordinary.ψ[THEN RN,
                  THEN "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)],
                  THEN "PossibleWorld.∀E"] by simp
        moreover AOT_have ‹w₁ ⊨ [λy p]u›
          by (safe intro!: world_prop_beta[THEN "PossibleWorld.∀E", THEN "≡E"(2)]
                           0[THEN "&E"(1)])
        ultimately AOT_have ‹w₁ ⊨ (O!u & [λy p]u)›
          using "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
                                OF "log-prop-prop:2", THEN "≡E"(2),
                                OF "&I"] by blast
        AOT_hence ‹∃x w₁ ⊨ (O!x & [λy p]x)›
          by (rule "∃I")
        AOT_thus ‹w₁ ⊨ ∃u [λy p]u›
          by (metis "conj-dist-w:6" "intro-elim:3:b")
      next
        AOT_show ‹w₁ ⊨ ¬∃v [λz O!z & z ≠_E z]v›
          using "PossibleWorld.∀E" nec_not_ex by fastforce
      qed
      ultimately AOT_show ‹p & ¬p› for p
        using "raa-cor:3" by blast
    qed
    ultimately AOT_have ‹y[λy p] & ¬x[λy p]›
      using "&I" by blast
    AOT_hence ‹∃F (y[F] & ¬x[F])›
      by (metis "existential:1" "prop-prop2:2")
    AOT_thus ‹∃F (x[F] & ¬y[F]) ∨ ∃F (y[F] & ¬x[F])›
      by (rule "∨I")
  qed
  ultimately AOT_have ‹♢Numbers'(x,[λz O!z & z ≠_E z]) &
 ♢Numbers'(y,[λz O!z & z ≠_E z]) & x ≠ y›
    using "&I" by blast
  AOT_thus ‹∃x∃y (♢Numbers'(x,[λz O!z & z ≠_E z]) &
 ♢Numbers'(y,[λz O!z & z ≠_E z]) & x ≠ y)›
    using "∃I"(2)[where β=x] "∃I"(2)[where β=y] by auto
qed

AOT_theorem restricted_identity:
  ‹x =_\R y ≡ (InDomainOf(x,R) & InDomainOf(y,R) & x = y)›
  by (auto intro!: "≡I" "→I" "&I"
             dest: "id-R-thm:2"[THEN "→E"] "&E"
                   "id-R-thm:3"[THEN "→E"]
                   "id-R-thm:4"[THEN "→E", OF "∨I"(1), THEN "≡E"(2)])

AOT_theorem induction': ‹∀F ([F]0 & ∀n([F]n → [F]n') → ∀n [F]n)›
proof(rule GEN; rule "→I")
  fix F n
  AOT_assume A: ‹[F]0 & ∀n([F]n → [F]n')›
  AOT_have ‹∀n∀m([ℙ]nm → ([F]n → [F]m))›
  proof(safe intro!: "Number.GEN" "→I")
    fix n m
    AOT_assume ‹[ℙ]nm›
    moreover AOT_have ‹[ℙ]n n'›
      using "suc-thm".
    ultimately AOT_have m_eq_suc_n: ‹m = n'›
      using "pred-func:1"[unvarify z, OF "def-suc[den2]", THEN "→E", OF "&I"]
      by blast
    AOT_assume ‹[F]n›
    AOT_hence ‹[F]n'›
      using A[THEN "&E"(2), THEN "Number.∀E", THEN "→E"] by blast
    AOT_thus ‹[F]m›
      using m_eq_suc_n[symmetric] "rule=E" by fast
  qed
  AOT_thus ‹∀n[F]n›
    using induction[THEN "∀E"(2), THEN "→E", OF "&I", OF A[THEN "&E"(1)]]
    by simp
qed

AOT_define ExtensionOf :: ‹τ ==> Π ==> φ› (‹ExtensionOf'(_,_')›)
  "exten-property:1": ‹ExtensionOf(x,[G]) ≡_df A!x & G↓ & an style='font-size: 18px;'>∀F(x[F] ≡ ∀z([F]z ≡ [G]z))›

AOT_define OrdinaryExtensionOf :: ‹τ ==> Π ==> φ› (‹OrdinaryExtensionOf'(_,_')›)
   ‹OrdinaryExtensionOf(x,[G]) ≡_df A!x & G↓ & ∀F(x[F] ≡ ∀z(O!z → ([F]z ≡ [G]z)))›

AOT_theorem BeingOrdinaryExtensionOfDenotes:
  ‹[λx OrdinaryExtensionOf(x,[G])]↓›
proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
  AOT_show ‹[λx A!x & G↓ & [λx ∀F(x[F] ≡ ∀z(O!z → ([F]z ≡ [G]z)))]x]↓›
    by "cqt:2"
next
  AOT_show ‹◻∀x (A!x & G↓ & [λx ∀F (x[F] ≡ ∀z (O!z → ([F]z ≡ [G]z)))]x ≡
 OrdinaryExtensionOf(x,[G]))›
  proof(safe intro!: RN GEN)
    AOT_modally_strict {
      fix x
      AOT_modally_strict {
        AOT_have ‹[λx ∀F (x[F] ≡ ∀z (O!z → ([F]z ≡ [G]z)))]↓›
        proof (safe intro!: "Comprehension_3"[THEN "→E"] RN GEN
                            "→I" "≡I" Ordinary.GEN)
          AOT_modally_strict {
            fix F H u
            AOT_assume ‹◻H ≡_E F›
            AOT_hence ‹∀u([H]u ≡ [F]u)›
              using eqE[THEN "≡_dfE", THEN "&E"(2)] "qml:2"[axiom_inst, THEN "→E"]
              by blast
            AOT_hence 0: ‹[H]u ≡ [F]u› using "Ordinary.∀E" by fast
            {
              AOT_assume ‹∀u([F]u ≡ [G]u)›
              AOT_hence 1: ‹[F]u ≡ [G]u› using "Ordinary.∀E" by fast
              AOT_show ‹[G]u› if ‹[H]u› using 0 1 "≡E"(1) that by blast
              AOT_show ‹[H]u› if ‹[G]u› using 0 1 "≡E"(2) that by blast
            }
            {
              AOT_assume ‹∀u([H]u ≡ [G]u)›
              AOT_hence 1: ‹[H]u ≡ [G]u› using "Ordinary.∀E" by fast
              AOT_show ‹[G]u› if ‹[F]u› using 0 1 "≡E"(1,2) that by blast 
              AOT_show ‹[F]u› if ‹[G]u› using 0 1 "≡E"(1,2) that by blast 
            }
          }
        qed
      }
      AOT_thus ‹(A!x & G↓ & [λx ∀F (x[F] ≡ ∀z (O!z → ([F]z ≡ [G]z)))]x) ≡
 OrdinaryExtensionOf(x,[G])›
        apply (AOT_subst_def OrdinaryExtensionOf)
        apply (AOT_subst ‹[λx ∀F (x[F] ≡ ∀z (O!z → ([F]z ≡ [G]z)))]x›
                         ‹∀F (x[F] ≡ ∀z (O!z → ([F]z ≡ [G]z)))›)
        by (auto intro!: "beta-C-meta"[THEN "→E"] simp: "oth-class-taut:3:a")
    }
  qed
qed

text‹Fragments of PLM's theory of Concepts.›

AOT_define FimpG :: ‹Π ==> Π ==> φ› (infixl ‹==>› 50)
  "F-imp-G": ‹[G] ==> [F] ≡_df F↓ & G↓ & ◻∀x ([G]x → [F]x)›

AOT_define concept :: ‹Π› (‹C!›)
  concepts: ‹C! =_df A!›

AOT_register_rigid_restricted_type
  Concept: ‹C!κ›
proof
  AOT_modally_strict {
    AOT_have ‹∃x A!x›
      using "o-objects-exist:2" "qml:2"[axiom_inst] "→E" by blast
    AOT_thus ‹∃x C!x›
      using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"] "rule=E" id_sym
      by fast
  }
next
  AOT_modally_strict {
    AOT_show ‹C!κ → κ↓› for κ
      using "cqt:5:a"[axiom_inst, THEN "→E", THEN "&E"(2)] "→I"
      by blast
  }
next
  AOT_modally_strict {
    AOT_have ‹∀x(A!x → ◻A!x)›
      by (simp add: "oa-facts:2" GEN)
    AOT_thus ‹∀x(C!x → ◻C!x)›
      using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"] "rule=E" id_sym
      by fast
  }
qed

AOT_register_variable_names
  Concept: c d e

AOT_theorem "concept-comp:1": ‹∃x(C!x & ∀F(x[F] ≡ φ{F}))›
    using concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2", symmetric]
          "A-objects"[axiom_inst]
          "rule=E" by fast

AOT_theorem "concept-comp:2": ‹∃!x(C!x & ∀F(x[F] ≡ φ{F}))›
    using concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2", symmetric]
          "A-objects!"
          "rule=E" by fast

AOT_theorem "concept-comp:3": ‹\ιx(C!x & ∀F(x[F] ≡ φ{F}))↓›
  using "concept-comp:2" "A-Exists:2"[THEN "≡E"(2)] "RA[2]" by blast

AOT_theorem "concept-comp:4":
  ‹\ιx(C!x & ∀F(x[F] ≡ φ{F})) = \ιx(A!x & ∀F(x[F] ≡ φ{F}))›
    using "=I"(1)[OF "concept-comp:3"]
          "rule=E"[rotated]
          concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2"]
          by fast

AOT_define conceptInclusion :: ‹τ ==> τ ==> φ› (infixl ‹⪯› 100)
  "con:1": ‹c ⪯ d ≡_df ∀F(c[F] → d[F])›


AOT_define conceptOf :: ‹τ ==> τ ==> φ› (‹ConceptOf'(_,_')›)
  "concept-of-G": ‹ConceptOf(c,G) ≡_df G↓ & ∀F (c[F] ≡ [G] ==> [F])›

AOT_theorem ConceptOfOrdinaryProperty: ‹([H] ==> O!) → [λx ConceptOf(x,H)]↓›
proof(rule "→I")
  AOT_assume ‹[H] ==> O!›
  AOT_hence ‹◻∀x([H]x → O!x)›
    using "F-imp-G"[THEN "≡_dfE"] "&E" by blast
  AOT_hence ‹◻◻∀x([H]x → O!x)›
    using "S5Basic:6"[THEN "≡E"(1)] by blast
  moreover AOT_have ‹◻◻∀x([H]x → O!x) →
 ◻∀F∀G(◻(G ≡_E F) → ([H] ==> [F] ≡ [H] ==> [G]))›
  proof(rule RM; safe intro!: "→I" GEN "≡I")
    AOT_modally_strict {
      fix F G
      AOT_assume 0: ‹◻∀x([H]x → O!x)›
      AOT_assume ‹◻G ≡_E F›
      AOT_hence 1: ‹◻∀u([G]u ≡ [F]u)›
        by (AOT_subst_thm eqE[THEN "≡Df", THEN "≡S"(1), OF "&I",
              OF "cqt:2[const_var]"[axiom_inst],
              OF "cqt:2[const_var]"[axiom_inst], symmetric])
      {
        AOT_assume ‹[H] ==> [F]›
        AOT_hence ‹◻∀x([H]x → [F]x)›
          using "F-imp-G"[THEN "≡_dfE"] "&E" by blast
        moreover AOT_modally_strict {
          AOT_assume ‹∀x([H]x → O!x)›
          moreover AOT_assume ‹∀u([G]u ≡ [F]u)›
          moreover AOT_assume ‹∀x([H]x → [F]x)›
          ultimately AOT_have ‹[H]x → [G]x› for x
            by (auto intro!: "→I" dest!: "∀E"(2) dest: "→E" "≡E")
          AOT_hence ‹∀x([H]x → [G]x)›
            by (rule GEN)
        }
        ultimately AOT_have ‹◻∀x([H]x → [G]x)›
          using "RN[prem]"[where
              Γ="{«∀x([H]x → O!x)¬, «∀u([G]u ≡ [F]u)¬, «∀x([H]x → [F]x)¬}"]
          using 0 1 by fast
        AOT_thus ‹[H] ==> [G]›
          by (AOT_subst_def "F-imp-G")
             (safe intro!: "cqt:2" "&I")
      }
      {
        AOT_assume ‹[H] ==> [G]›
        AOT_hence ‹◻∀x([H]x → [G]x)›
          using "F-imp-G"[THEN "≡_dfE"] "&E" by blast
        moreover AOT_modally_strict {
          AOT_assume ‹∀x([H]x → O!x)›
          moreover AOT_assume ‹∀u([G]u ≡ [F]u)›
          moreover AOT_assume ‹∀x([H]x → [G]x)›
          ultimately AOT_have ‹[H]x → [F]x› for x
            by (auto intro!: "→I" dest!: "∀E"(2) dest: "→E" "≡E")
          AOT_hence ‹∀x([H]x → [F]x)›
            by (rule GEN)
        }
        ultimately AOT_have ‹◻∀x([H]x → [F]x)›
          using "RN[prem]"[where
              Γ="{«∀x([H]x → O!x)¬, «∀u([G]u ≡ [F]u)¬, «∀x([H]x → [G]x)¬}"]
          using 0 1 by fast
        AOT_thus ‹[H] ==> [F]›
          by (AOT_subst_def "F-imp-G")
             (safe intro!: "cqt:2" "&I")
      }
    }
  qed
  ultimately AOT_have ‹◻∀F∀G(◻(G ≡_E F) → ([H] ==> [F] ≡ [H] ==> [G]))›
    using "→E" by blast
  AOT_hence 0: ‹[λx ∀F(x[F] ≡ ([H] ==> [F]))]↓›
    using Comprehension_3[THEN "→E"] by blast
  AOT_show ‹[λx ConceptOf(x,H)]↓›
  proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show ‹[λx C!x & [λx ∀F(x[F] ≡ ([H] ==> [F]))]x]↓› by "cqt:2"
  next
    AOT_show ‹◻∀x (C!x & [λx ∀F (x[F] ≡ [H] ==> [F])]x ≡ ConceptOf(x,H))›
    proof (rule "RN[prem]"[where Γ=‹{«[λx ∀F(x[F] ≡ ([H] ==> [F]))]↓¬}›, simplified])
      AOT_modally_strict {
        AOT_assume 0: ‹[λx ∀F (x[F] ≡ [H] ==> [F])]↓›
        AOT_show ‹∀x (C!x & [λx ∀F (x[F] ≡ [H] ==> [F])]x ≡ ConceptOf(x,H))›
        proof(safe intro!: GEN "≡I" "→I" "&I")
          fix x
          AOT_assume ‹C!x & [λx ∀F (x[F] ≡ [H] ==> [F])]x›
          AOT_thus ‹ConceptOf(x,H)›
            by (AOT_subst_def "concept-of-G")
               (auto intro!: "&I" "cqt:2" dest: "&E" "β→C")
        next
          fix x
          AOT_assume ‹ConceptOf(x,H)›
          AOT_hence ‹C!x & (H↓ & ∀F(x[F] ≡ [H] ==> [F]))›
            by (AOT_subst_def (reverse) "concept-of-G")
          AOT_thus ‹C!x› and ‹[λx ∀F(x[F] ≡ [H] ==> [F])]x›
            by (auto intro!: "β←C" 0 "cqt:2" dest: "&E")
        qed
      }
    next
      AOT_show ‹◻[λx ∀F(x[F] ≡ ([H] ==> [F]))]↓›
        using "exist-nec"[THEN "→E"] 0 by blast
    qed
  qed
qed

AOT_theorem "con-exists:1": ‹∃c ConceptOf(c,G)›
proof -
  AOT_obtain c where ‹∀F (c[F] ≡ [G] ==> [F])›
    using "concept-comp:1" "Concept.∃E"[rotated] by meson
  AOT_hence ‹ConceptOf(c,G)›
    by (auto intro!: "concept-of-G"[THEN "≡_dfI"] "&I" "cqt:2" Concept.ψ)
  thus ?thesis by (rule "Concept.∃I")
qed

AOT_theorem "con-exists:2": ‹∃!c ConceptOf(c,G)›
proof -
  AOT_have ‹∃!c ∀F (c[F] ≡ [G] ==> [F])›
    using "concept-comp:2" by simp
  moreover {
    AOT_modally_strict {
      fix x
      AOT_assume ‹∀F (x[F] ≡ [G] ==> [F])›
      moreover AOT_have ‹[G] ==> [G]›
        by (safe intro!: "F-imp-G"[THEN "≡_dfI"] "&I" "cqt:2" RN GEN "→I")
      ultimately AOT_have ‹x[G]›
        using "∀E"(2) "≡E" by blast
      AOT_hence ‹A!x›
        using "encoders-are-abstract"[THEN "→E", OF "∃I"(2)] by simp
      AOT_hence ‹C!x›
        using concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2", symmetric]
              "rule=E"[rotated]
        by fast
    }
  }
  ultimately show ?thesis
    by (AOT_subst ‹ConceptOf(c,G)› ‹∀F (c[F] ≡ [G] ==> [F])› for: c;
           AOT_subst_def "concept-of-G")
       (auto intro!: "≡I" "→I" "&I" "cqt:2" Concept.ψ dest: "&E")
qed

AOT_theorem "con-exists:3": ‹\ιc ConceptOf(c,G)↓›
  by (safe intro!: "A-Exists:2"[THEN "≡E"(2)] "con-exists:2"[THEN "RA[2]"])


AOT_define theConceptOfG :: ‹τ ==> κ_s› (‹c_{_}›)
  "concept-G": ‹c_G =_df \ιc ConceptOf(c, G)›

AOT_theorem "concept-G[den]": ‹c_G↓›
  by (auto intro!: "rule-id-df:1"[OF "concept-G"]
                   "t=t-proper:1"[THEN "→E"]
                   "con-exists:3")


AOT_theorem "concept-G[concept]": ‹C!c_G›
proof -
  AOT_have ‹\A(C!c_G & ConceptOf(c_G, G))›
    by (auto intro!: "actual-desc:2"[unvarify x, THEN "→E"]
                     "rule-id-df:1"[OF "concept-G"]
                     "concept-G[den]"
                     "con-exists:3")
  AOT_hence ‹\AC!c_G›
    by (metis "Act-Basic:2" "con-dis-i-e:2:a" "intro-elim:3:a")
  AOT_hence ‹\AA!c_G›
    using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"]
          "rule=E" by fast
  AOT_hence ‹A!c_G›
    using "oa-facts:8"[unvarify x, THEN "≡E"(2)] "concept-G[den]" by blast
  thus ?thesis
    using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2", symmetric]
          "rule=E" by fast
qed

AOT_theorem "conG-strict": ‹c_G = \ιc ∀F(c[F] ≡ [G] ==> [F])›
proof (rule "id-eq:3"[unvarify α β γ, THEN "→E"])
  AOT_have ‹◻∀x (C!x & ConceptOf(x,G) ≡ C!x & ∀F (x[F] ≡ [G] ==> [F]))›
    by (auto intro!: "concept-of-G"[THEN "≡_dfI"] RN GEN "≡I" "→I" "&I" "cqt:2"
               dest: "&E";
        auto dest: "∀E"(2) "≡E"(1,2) dest!: "&E"(2) "concept-of-G"[THEN "≡_dfE"])
  AOT_thus ‹c_G = \ιc ConceptOf(c, G) & \ιc ConceptOf(c, G) = \ιc ∀F(c[F] ≡ [G] ==> [F])›
    by (auto intro!: "&I" "rule-id-df:1"[OF "concept-G"] "con-exists:3"
                      "equiv-desc-eq:3"[THEN "→E"])
qed(auto simp: "concept-G[den]" "con-exists:3" "concept-comp:3")


AOT_theorem "conG-lemma:1": ‹∀F(c_G[F] ≡ [G] ==> [F])›
proof(safe intro!: GEN "≡I" "→I")
  fix F
  AOT_have ‹\A∀F(c_G[F] ≡ [G] ==> [F])›
    using "actual-desc:4"[THEN "→E", OF "concept-comp:3",
                          THEN "Act-Basic:2"[THEN "≡E"(1)],
                          THEN "&E"(2)]
          "conG-strict"[symmetric] "rule=E" by fast
  AOT_hence ‹\A(c_G[F] ≡ [G] ==> [F])›
    using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] "∀E"(2)
    by blast
  AOT_hence 0: ‹\Ac_G[F] ≡ \A[G] ==> [F]›
    using "Act-Basic:5"[THEN "≡E"(1)] by blast
  {
    AOT_assume ‹c_G[F]›
    AOT_hence ‹\Ac_G[F]›
      by(safe intro!: "en-eq:10[1]"[unvarify x₁, THEN "≡E"(2)]
                      "concept-G[den]")
    AOT_hence ‹\A[G] ==> [F]›
      using 0[THEN "≡E"(1)] by blast
    AOT_hence ‹\A(F↓ & G↓ & ◻∀x([G]x → [F]x))›
      by (AOT_subst_def (reverse) "F-imp-G")
    AOT_hence ‹\A◻∀x([G]x → [F]x)›
      using "Act-Basic:2"[THEN "≡E"(1)] "&E" by blast
    AOT_hence ‹◻∀x([G]x → [F]x)›
      using "qml-act:2"[axiom_inst, THEN "≡E"(2)] by simp
    AOT_thus ‹[G] ==> [F]›
      by (AOT_subst_def "F-imp-G"; auto intro!: "&I" "cqt:2")
  }
  {
    AOT_assume ‹[G] ==> [F]›
    AOT_hence ‹◻∀x([G]x → [F]x)›
      by (safe dest!: "F-imp-G"[THEN "≡_dfE"] "&E"(2))
    AOT_hence ‹\A◻∀x([G]x → [F]x)›
      using "qml-act:2"[axiom_inst, THEN "≡E"(1)] by simp
    AOT_hence ‹\A(F↓ & G↓ & ◻∀x([G]x → [F]x))›
      by (auto intro!: "Act-Basic:2"[THEN "≡E"(2)] "&I" "cqt:2"
               intro: "RA[2]")
    AOT_hence ‹\A([G] ==> [F])›
      by (AOT_subst_def "F-imp-G")
    AOT_hence ‹\Ac_G[F]›
      using 0[THEN "≡E"(2)] by blast
    AOT_thus ‹c_G[F]›
      by(safe intro!: "en-eq:10[1]"[unvarify x₁, THEN "≡E"(1)]
                      "concept-G[den]")
  }
qed

AOT_theorem conH_enc_ord:
  ‹([H] ==> O!) → ◻∀F ∀G (◻G ≡_E F → (c_H[F] ≡ c_H[G]))›
proof(rule "→I")
  AOT_assume 0: ‹[H] ==> O!›
  AOT_have 0: ‹◻([H] ==> O!)›
    apply (AOT_subst_def "F-imp-G")
    using 0[THEN "≡_dfE"[OF "F-imp-G"]]
    by (auto intro!: "KBasic:3"[THEN "≡E"(2)] "&I" "exist-nec"[THEN "→E"]
               dest: "&E" 4[THEN "→E"])
  moreover AOT_have ‹◻([H] ==> O!) → ◻∀F ∀G (◻G ≡_E F → (c_H[F] ≡ c_H[G]))›
  proof(rule RM; safe intro!: "→I" GEN)
    AOT_modally_strict {
      fix F G
      AOT_assume ‹[H] ==> O!›
      AOT_hence 0: ‹◻∀x ([H]x → O!x)›
        by (safe dest!: "F-imp-G"[THEN "≡_dfE"] "&E"(2))
      AOT_assume 1: ‹◻G ≡_E F›
      AOT_assume ‹c_H[F]›
      AOT_hence ‹[H] ==> [F]›
        using "conG-lemma:1"[THEN "∀E"(2), THEN "≡E"(1)] by simp
      AOT_hence 2: ‹◻∀x ([H]x → [F]x)›
        by (safe dest!: "F-imp-G"[THEN "≡_dfE"] "&E"(2))
      AOT_modally_strict {
        AOT_assume 0: ‹∀x ([H]x → O!x)›
        AOT_assume 1: ‹∀x ([H]x → [F]x)›
        AOT_assume 2: ‹G ≡_E F›
        AOT_have ‹∀x ([H]x → [G]x)›
        proof(safe intro!: GEN "→I")
          fix x
          AOT_assume ‹[H]x›
          AOT_hence ‹O!x› and ‹[F]x›
            using 0 1 "∀E"(2) "→E" by blast+
          AOT_thus ‹[G]x›
            using 2[THEN eqE[THEN "≡_dfE"], THEN "&E"(2)]
                  "∀E"(2) "→E" "≡E"(2) calculation by blast
        qed
      }
      AOT_hence ‹◻∀x ([H]x → [G]x)›
        using "RN[prem]"[where Γ=‹{«∀x ([H]x → O!x)¬,
 «∀x ([H]x → [F]x)¬,
 «G ≡_E F¬}›, simplified] 0 1 2 by fast
      AOT_hence ‹[H] ==> [G]›
        by (safe intro!: "F-imp-G"[THEN "≡_dfI"] "&I" "cqt:2")
      AOT_hence ‹c_H[G]›
        using "conG-lemma:1"[THEN "∀E"(2), THEN "≡E"(2)] by simp
    } note 0 = this
    AOT_modally_strict {
      fix F G
      AOT_assume ‹[H] ==> O!›
      moreover AOT_assume ‹◻G ≡_E F›
      moreover AOT_have ‹◻F ≡_E G›
        by (AOT_subst ‹F ≡_E G› ‹G ≡_E F›)
            (auto intro!: calculation(2)
                          eqE[THEN "≡_dfI"]
                          "≡I" "→I" "&I" "cqt:2" Ordinary.GEN
                  dest!: eqE[THEN "≡_dfE"] "&E"(2)
                  dest: "≡E"(1,2) "Ordinary.∀E")
      ultimately AOT_show ‹(c_H[F] ≡ c_H[G])›
        using 0 "≡I" "→I" by auto
    }
  qed
  ultimately AOT_show ‹◻∀F ∀G (◻G ≡_E F → (c_H[F] ≡ c_H[G]))›
    using "→E" by blast
qed

AOT_theorem concept_inclusion_denotes_1:
  ‹([H] ==> O!) → [λx c_H ⪯ x]↓›
proof(rule "→I")
  AOT_assume 0: ‹[H] ==> O!›
  AOT_show ‹[λx c_H ⪯ x]↓›
  proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show ‹[λx C!x & ∀F(c_H[F] → x[F])]↓›
      by (safe intro!: conjunction_denotes[THEN "→E", OF "&I"]
                       Comprehension_2'[THEN "→E"]
                       conH_enc_ord[THEN "→E", OF 0]) "cqt:2"
  next
    AOT_show ‹◻∀x (C!x & ∀F (c_H[F] → x[F]) ≡ c_H ⪯ x)›
      by (safe intro!: RN GEN; AOT_subst_def "con:1")
         (auto intro!: "≡I" "→I" "&I" "concept-G[concept]" dest: "&E")
  qed
qed

AOT_theorem concept_inclusion_denotes_2:
  ‹([H] ==> O!) → [λx x ⪯ c_H]↓›
proof(rule "→I")
  AOT_assume 0: ‹[H] ==> O!›
  AOT_show ‹[λx x ⪯ c_H]↓›
  proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show ‹[λx C!x & ∀F(x[F] → c_H[F])]↓›
      by (safe intro!: conjunction_denotes[THEN "→E", OF "&I"]
                       Comprehension_1'[THEN "→E"]
                       conH_enc_ord[THEN "→E", OF 0]) "cqt:2"
  next
    AOT_show ‹◻∀x (C!x & ∀F (x[F] → c_H[F]) ≡ x ⪯ c_H)›
      by (safe intro!: RN GEN; AOT_subst_def "con:1")
         (auto intro!: "≡I" "→I" "&I" "concept-G[concept]" dest: "&E")
  qed
qed

AOT_define ThickForm :: ‹τ ==> τ ==> φ› (‹FormOf'(_,_')›)
  "tform-of": ‹FormOf(x,G) ≡_df A!x & G↓ & ∀F(x[F] ≡ [G] ==> [F])›

AOT_theorem FormOfOrdinaryProperty: ‹([H] ==> O!) → [λx FormOf(x,H)]↓›
proof(rule "→I")
  AOT_assume 0: ‹[H] ==> [O!]›
  AOT_show ‹[λx FormOf(x,H)]↓›
  proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show ‹[λx ConceptOf(x,H)]↓›
      using 0 ConceptOfOrdinaryProperty[THEN "→E"] by blast
    AOT_show ‹◻∀x (ConceptOf(x,H) ≡ FormOf(x,H))›
    proof(safe intro!: RN GEN)
      AOT_modally_strict {
        fix x
        AOT_modally_strict {
          AOT_have ‹A!x ≡ A!x›
            by (simp add: "oth-class-taut:3:a")
          AOT_hence ‹C!x ≡ A!x›
            using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"]
                  "rule=E" id_sym by fast
        }
        AOT_thus ‹ConceptOf(x,H) ≡ FormOf(x,H)›
          by (AOT_subst_def "tform-of";
              AOT_subst_def "concept-of-G";
              AOT_subst ‹C!x› ‹A!x›)
             (auto intro!: "≡I" "→I" "&I" dest: "&E")
      }
    qed
  qed
qed

AOT_theorem equal_E_rigid_one_to_one: ‹Rigid_1-1((=_E))›
proof (safe intro!: "df-1-1:2"[THEN "≡_dfI"] "&I" "df-1-1:1"[THEN "≡_dfI"]
                    GEN "→I" "df-rigid-rel:1"[THEN "≡_dfI"] "=E[denotes]")
  fix x y z
  AOT_assume ‹x =_E z & y =_E z›
  AOT_thus ‹x = y›
    by (metis "rule=E" "&E"(1) "Conjunction Simplification"(2)
              "=E-simple:2" id_sym "→E")
next
  AOT_have ‹∀x∀y ◻(x =_E y → ◻x =_E y)›
  proof(rule GEN; rule GEN)
    AOT_show ‹◻(x =_E y → ◻x =_E y)› for x y
      by (meson RN "deduction-theorem" "id-nec3:1" "≡E"(1))
  qed
  AOT_hence ‹∀x₁...∀x_n ◻([(=_E)]x₁...x_n → ◻[(=_E)]x₁...x_n)›
    by (rule tuple_forall[THEN "≡_dfI"])
  AOT_thus ‹◻∀x₁...∀x_n ([(=_E)]x₁...x_n → ◻[(=_E)]x₁...x_n)›
    using BF[THEN "→E"] by fast
qed

AOT_theorem equal_E_domain: ‹InDomainOf(x,(=_E)) ≡ O!x›
proof(safe intro!: "≡I" "→I")
  AOT_assume ‹InDomainOf(x,(=_E))›
  AOT_hence ‹∃y x =_E y›
    by (metis "≡_dfE" "df-1-1:5")
  then AOT_obtain y where ‹x =_E y›
    using "∃E"[rotated] by blast
  AOT_thus ‹O!x›
    using "=E-simple:1"[THEN "≡E"(1)] "&E" by blast
next
  AOT_assume ‹O!x›
  AOT_hence ‹x =_E x›   
    by (metis "ord=Eequiv:1"[THEN "→E"])
  AOT_hence ‹∃y x =_E y›
    using "∃I"(2) by fast
  AOT_thus ‹InDomainOf(x,(=_E))›
    by (metis "≡_dfI" "df-1-1:5")
qed

AOT_theorem shared_urelement_projection_identity:
  assumes ‹∀y [λx (y[λz [R]zx])]↓›
  shows ‹∀F([F]a ≡ [F]b) → [λz [R]za] = [λz [R]zb]›
proof(rule "→I")
  AOT_assume 0: ‹∀F([F]a ≡ [F]b)›
  {
    fix z
    AOT_have ‹[λx (z[λz [R]zx])]↓›
      using assms[THEN "∀E"(2)].
    AOT_hence 1: ‹∀x ∀y (∀F ([F]x ≡ [F]y) → ◻(z[λz [R]zx] ≡ z[λz [R]zy]))›
      using "kirchner-thm-cor:1"[THEN "→E"]
      by blast
    AOT_have ‹◻(z[λz [R]za] ≡ z[λz [R]zb])›
      using 1[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", OF 0] by blast
  }
  AOT_hence ‹∀z ◻(z[λz [R]za] ≡ z[λz [R]zb])›
    by (rule GEN)
  AOT_hence ‹◻∀z(z[λz [R]za] ≡ z[λz [R]zb])›
    by (rule BF[THEN "→E"])
  AOT_thus ‹[λz [R]za] = [λz [R]zb]›
    by (AOT_subst_def "identity:2")
       (auto intro!: "&I" "cqt:2")
qed

AOT_theorem shared_urelement_exemplification_identity:
  assumes ‹∀y [λx (y[λz [G]x])]↓›
  shows ‹∀F([F]a ≡ [F]b) → ([G]a) = ([G]b)›
proof(rule "→I")
  AOT_assume 0: ‹∀F([F]a ≡ [F]b)›
  {
    fix z
    AOT_have ‹[λx (z[λz [G]x])]↓›
      using assms[THEN "∀E"(2)].
    AOT_hence 1: ‹∀x ∀y (∀F ([F]x ≡ [F]y) → ◻(z[λz [G]x] ≡ z[λz [G]y]))›
      using "kirchner-thm-cor:1"[THEN "→E"]
      by blast
    AOT_have ‹◻(z[λz [G]a] ≡ z[λz [G]b])›
      using 1[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", OF 0] by blast
  }
  AOT_hence ‹∀z ◻(z[λz [G]a] ≡ z[λz [G]b])›
    by (rule GEN)
  AOT_hence ‹◻∀z(z[λz [G]a] ≡ z[λz [G]b])›
    by (rule BF[THEN "→E"])
  AOT_hence ‹[λz [G]a] = [λz [G]b]›
    by (AOT_subst_def "identity:2")
       (auto intro!: "&I" "cqt:2")
  AOT_thus ‹([G]a) = ([G]b)›
    by (safe intro!: "identity:4"[THEN "≡_dfI"] "&I" "log-prop-prop:2")
qed

text‹The assumptions of the theorems above are derivable, if the additional
 introduction rules for the upcoming extension of @{thm "cqt:2[lambda]"}
 are explicitly allowed (while they are currently not part of the
 abstraction layer).›
notepad
begin
  AOT_modally_strict {
    AOT_have ‹∀R∀y [λx (y[λz [R]zx])]↓›
      by (safe intro!: GEN "cqt:2" AOT_instance_of_cqt_2_intro_next)
    AOT_have ‹∀G∀y [λx (y[λz [G]x])]↓›
      by (safe intro!: GEN "cqt:2" AOT_instance_of_cqt_2_intro_next)
  }
end

end