Theory AOT_misc

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 "≡⇩d⇩fI"] "&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 ‹❙𝒜Numbers(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 ❙𝒜[λ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) ≡⇩d⇩f 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⇩1 where ‹∃w w⇩1 ≠ w›
    using "two-worlds-exist:4" "PossibleWorld.∃E"[rotated] by fast
  then AOT_obtain w⇩2 where distinct_worlds: ‹w⇩1 ≠ w⇩2›
    using "PossibleWorld.∃E"[rotated] by blast
  AOT_obtain x where x_prop:
    ‹A!x & ∀F (x[F] ≡ w⇩1 ⊨ 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⇩2 ⊨ 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 ≠⇩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⇩1 ⊨ p & ¬w⇩2 ⊨ p)›
    proof(rule "raa-cor:1")
      AOT_assume 0: ‹¬∃p (w⇩1 ⊨ p & ¬w⇩2 ⊨ p)›
      AOT_have 1: ‹w⇩1 ⊨ p → w⇩2 ⊨ p› for p
      proof(safe intro!: GEN "→I")
        AOT_assume ‹w⇩1 ⊨ p›
        AOT_thus ‹w⇩2 ⊨ p›
          using 0 "con-dis-i-e:1" "∃I"(2) "raa-cor:4" by fast
      qed
      moreover AOT_have ‹w⇩2 ⊨ p → w⇩1 ⊨ p› for p
      proof(safe intro!: GEN "→I")
        AOT_assume ‹w⇩2 ⊨ p›
        AOT_hence ‹¬w⇩2 ⊨ ¬p›
          using "coherent:2" "intro-elim:3:a" by blast
        AOT_hence ‹¬w⇩1 ⊨ ¬p›
          using 1["∀I" p, THEN "∀E"(1), OF "log-prop-prop:2"]
          by (metis "modus-tollens:1")
        AOT_thus ‹w⇩1 ⊨ p›
          using "coherent:1" "intro-elim:3:b" "reductio-aa:1" by blast
      qed
      ultimately AOT_have ‹w⇩1 ⊨ p ≡ w⇩2 ⊨ p› for p
        by (metis "intro-elim:2")
      AOT_hence ‹w⇩1 = w⇩2›
        using "sit-identity"[unconstrain s, THEN "→E",
            OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)],
            unconstrain s', THEN "→E",
            OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)],
            THEN "≡E"(2)] GEN by fast
      AOT_thus ‹w⇩1 = w⇩2 & ¬w⇩1 = w⇩2›
        using  "=-infix" "≡⇩d⇩fE" "con-dis-i-e:1" distinct_worlds by blast
    qed
    then AOT_obtain p where 0: ‹w⇩1 ⊨ p & ¬w⇩2 ⊨ 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⇩2 ⊨ [λ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⇩2 ⊨ ∃u [λy p]u›
        proof (rule "raa-cor:2")
          AOT_assume ‹w⇩2 ⊨ ∃u [λy p]u›
          AOT_hence ‹∃x w⇩2 ⊨ (O!x & [λy p]x)›
            by (metis "conj-dist-w:6" "intro-elim:3:a")
          then AOT_obtain x where ‹w⇩2 ⊨ (O!x & [λy p]x)›
            using "∃E"[rotated] by blast
          AOT_hence ‹w⇩2 ⊨ [λ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⇩2 ⊨ p›
            using world_prop_beta[THEN "PossibleWorld.∀E", THEN "≡E"(1)] by blast
          AOT_thus ‹w⇩2 ⊨ p & ¬w⇩2 ⊨ p›
            using 0[THEN "&E"(2)] "&I" by blast
        qed
        AOT_thus ‹w⇩2 ⊨ ¬∃u [λy p]u›
          by (safe intro!: "coherent:1"[unvarify p, OF "log-prop-prop:2",
                                        THEN "≡E"(2)])
      next
        AOT_show ‹w⇩2 ⊨ ¬∃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⇩1 ⊨ [λ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⇩1 ⊨ ¬[λ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⇩1 ⊨ ¬([λ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⇩1 ⊨ 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⇩1 ⊨ [λy p]u›
          by (safe intro!: world_prop_beta[THEN "PossibleWorld.∀E", THEN "≡E"(2)]
                           0[THEN "&E"(1)])
        ultimately AOT_have ‹w⇩1 ⊨ (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⇩1 ⊨ (O!x & [λy p]x)›
          by (rule "∃I")
        AOT_thus ‹w⇩1 ⊨ ∃u [λy p]u›
          by (metis "conj-dist-w:6" "intro-elim:3:b")
      next
        AOT_show ‹w⇩1 ⊨ ¬∃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 =⇩ℛ y ≡ (InDomainOf(x,ℛ) & InDomainOf(y,ℛ) & 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]) ≡⇩d⇩f A!x & G↓ & ∀F(x[F] ≡ ∀z([F]z ≡ [G]z))›

AOT_define OrdinaryExtensionOf :: ‹τ ⇒ Π ⇒ φ› (‹OrdinaryExtensionOf'(_,_')›)
   ‹OrdinaryExtensionOf(x,[G]) ≡⇩d⇩f 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 "≡⇩d⇩fE", 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] ≡⇩d⇩f F↓ & G↓ & □∀x ([G]x → [F]x)›

AOT_define concept :: ‹Π› (‹C!›)
  concepts: ‹C! =⇩d⇩f 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 ≡⇩d⇩f ∀F(c[F] → d[F])›


AOT_define conceptOf :: ‹τ ⇒ τ ⇒ φ› (‹ConceptOf'(_,_')›)
  "concept-of-G": ‹ConceptOf(c,G) ≡⇩d⇩f 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 "≡⇩d⇩fE"] "&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 "≡⇩d⇩fE"] "&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 "≡⇩d⇩fE"] "&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 "≡⇩d⇩fI"] "&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 "≡⇩d⇩fI"] "&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 =⇩d⇩f ❙ι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 ‹❙𝒜(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 ‹❙𝒜C!❙c⇩G›
    by (metis "Act-Basic:2" "con-dis-i-e:2:a" "intro-elim:3:a")
  AOT_hence ‹❙𝒜A!❙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 "≡⇩d⇩fI"] RN GEN "≡I" "→I" "&I" "cqt:2"
               dest: "&E";
        auto dest: "∀E"(2) "≡E"(1,2) dest!: "&E"(2) "concept-of-G"[THEN "≡⇩d⇩fE"])
  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 ‹❙𝒜∀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 ‹❙𝒜(❙c⇩G[F] ≡ [G] ⇒ [F])›
    using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] "∀E"(2)
    by blast
  AOT_hence 0: ‹❙𝒜❙c⇩G[F] ≡ ❙𝒜[G] ⇒ [F]›
    using "Act-Basic:5"[THEN "≡E"(1)] by blast
  {
    AOT_assume ‹❙c⇩G[F]›
    AOT_hence ‹❙𝒜❙c⇩G[F]›
      by(safe intro!: "en-eq:10[1]"[unvarify x⇩1, THEN "≡E"(2)]
                      "concept-G[den]")
    AOT_hence ‹❙𝒜[G] ⇒ [F]›
      using 0[THEN "≡E"(1)] by blast
    AOT_hence ‹❙𝒜(F↓ & G↓ & □∀x([G]x → [F]x))›
      by (AOT_subst_def (reverse) "F-imp-G")
    AOT_hence ‹❙𝒜□∀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 "≡⇩d⇩fE"] "&E"(2))
    AOT_hence ‹❙𝒜□∀x([G]x → [F]x)›
      using "qml-act:2"[axiom_inst, THEN "≡E"(1)] by simp
    AOT_hence ‹❙𝒜(F↓ & G↓ & □∀x([G]x → [F]x))›
      by (auto intro!: "Act-Basic:2"[THEN "≡E"(2)] "&I" "cqt:2"
               intro: "RA[2]")
    AOT_hence ‹❙𝒜([G] ⇒ [F])›
      by (AOT_subst_def "F-imp-G")
    AOT_hence ‹❙𝒜❙c⇩G[F]›
      using 0[THEN "≡E"(2)] by blast
    AOT_thus ‹❙c⇩G[F]›
      by(safe intro!: "en-eq:10[1]"[unvarify x⇩1, 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 "≡⇩d⇩fE"[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 "≡⇩d⇩fE"] "&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 "≡⇩d⇩fE"] "&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 "≡⇩d⇩fE"], 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 "≡⇩d⇩fI"] "&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 "≡⇩d⇩fI"]
                          "≡I" "→I" "&I" "cqt:2" Ordinary.GEN
                  dest!: eqE[THEN "≡⇩d⇩fE"] "&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) ≡⇩d⇩f 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 "≡⇩d⇩fI"] "&I" "df-1-1:1"[THEN "≡⇩d⇩fI"]
                    GEN "→I" "df-rigid-rel:1"[THEN "≡⇩d⇩fI"] "=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⇩1...∀x⇩n □([(=⇩E)]x⇩1...x⇩n → □[(=⇩E)]x⇩1...x⇩n)›
    by (rule tuple_forall[THEN "≡⇩d⇩fI"])
  AOT_thus ‹□∀x⇩1...∀x⇩n ([(=⇩E)]x⇩1...x⇩n → □[(=⇩E)]x⇩1...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 "≡⇩d⇩fE" "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 "≡⇩d⇩fI" "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 "≡⇩d⇩fI"] "&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