Theory AOT_NaturalNumbers

(*<*)
theory AOT_NaturalNumbers
  imports AOT_PossibleWorlds AOT_ExtendedRelationComprehension
  abbrevs one-to-one = ‹⇩1⇩-⇩1›
      and onto = ‹⇩o⇩n⇩t⇩o›
begin
(*>*)

section‹Natural Numbers›
 
AOT_define CorrelatesOneToOne :: ‹τ ⇒ τ ⇒ τ ⇒ φ› (‹_ |: _ ⇩1⇩-⇩1⟷ _›)
  "1-1-cor": ‹R |: F ⇩1⇩-⇩1⟷ G ≡⇩d⇩f R↓ & F↓ & G↓ &
                                   ∀x ([F]x → ∃!y([G]y & [R]xy)) &
                                   ∀y ([G]y → ∃!x([F]x & [R]xy))›

AOT_define MapsTo :: ‹τ ⇒ τ ⇒ τ ⇒ φ› (‹_ |: _ ⟶ _›)
  "fFG:1": ‹R |: F ⟶ G ≡⇩d⇩f R↓ & F↓ & G↓ & ∀x ([F]x → ∃!y([G]y & [R]xy))›

AOT_define MapsToOneToOne :: ‹τ ⇒ τ ⇒ τ ⇒ φ› (‹_ |: _ ⇩1⇩-⇩1⟶ _›)
  "fFG:2": ‹R |: F ⇩1⇩-⇩1⟶ G ≡⇩d⇩f
      R |: F ⟶ G & ∀x∀y∀z (([F]x & [F]y & [G]z) → ([R]xz & [R]yz → x = y))›

AOT_define MapsOnto :: ‹τ ⇒ τ ⇒ τ ⇒ φ› (‹_ |: _ ⟶⇩o⇩n⇩t⇩o _›)
  "fFG:3": ‹R |: F ⟶⇩o⇩n⇩t⇩o G ≡⇩d⇩f R |: F ⟶ G & ∀y ([G]y → ∃x([F]x & [R]xy))›

AOT_define MapsOneToOneOnto :: ‹τ ⇒ τ ⇒ τ ⇒ φ› (‹_ |: _ ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩o _›)
  "fFG:4": ‹R |: F ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩o G ≡⇩d⇩f R |: F ⇩1⇩-⇩1⟶ G & R |: F ⟶⇩o⇩n⇩t⇩o G›

AOT_theorem "eq-1-1": ‹R |: F ⇩1⇩-⇩1⟷ G ≡ R |: F ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩o G›
proof(rule "≡I"; rule "→I")
  AOT_assume ‹R |: F ⇩1⇩-⇩1⟷ G›
  AOT_hence A: ‹∀x ([F]x → ∃!y([G]y & [R]xy))›
        and B: ‹∀y ([G]y → ∃!x([F]x & [R]xy))›
    using "≡⇩d⇩fE"[OF "1-1-cor"] "&E" by blast+
  AOT_have C: ‹R |: F ⟶ G›
  proof (rule "≡⇩d⇩fI"[OF "fFG:1"]; rule "&I")
    AOT_show ‹R↓ & F↓ & G↓›
      using "cqt:2[const_var]"[axiom_inst] "&I" by metis
  next
    AOT_show ‹∀x ([F]x → ∃!y([G]y & [R]xy))› by (rule A)
  qed
  AOT_show ‹R |: F ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩o G›
  proof (rule "≡⇩d⇩fI"[OF "fFG:4"]; rule "&I")
    AOT_show ‹R |: F ⇩1⇩-⇩1⟶ G›
    proof (rule "≡⇩d⇩fI"[OF "fFG:2"]; rule "&I")
      AOT_show ‹R |: F ⟶ G› using C.
    next
      AOT_show ‹∀x∀y∀z ([F]x & [F]y & [G]z → ([R]xz & [R]yz → x = y))›
      proof(rule GEN; rule GEN; rule GEN; rule "→I"; rule "→I")
        fix x y z
        AOT_assume 1: ‹[F]x & [F]y & [G]z›
        moreover AOT_assume 2: ‹[R]xz & [R]yz›
        ultimately AOT_have 3: ‹∃!x ([F]x & [R]xz)›
          using B "&E" "∀E" "→E" by fast
        AOT_show ‹x = y›
          by (rule "uni-most"[THEN "→E", OF 3, THEN "∀E"(2)[where β=x],
                              THEN "∀E"(2)[where β=y], THEN "→E"])
             (metis "&I" "&E" 1 2)
      qed
    qed
  next
    AOT_show ‹R |: F ⟶⇩o⇩n⇩t⇩o G›
    proof (rule "≡⇩d⇩fI"[OF "fFG:3"]; rule "&I")
      AOT_show ‹R |: F ⟶ G› using C.
    next
      AOT_show ‹∀y ([G]y → ∃x ([F]x & [R]xy))›
      proof(rule GEN; rule "→I")
        fix y
        AOT_assume ‹[G]y›
        AOT_hence ‹∃!x ([F]x & [R]xy)›
          using B[THEN "∀E"(2), THEN "→E"] by blast
        AOT_hence ‹∃x ([F]x & [R]xy & ∀β (([F]β & [R]βy) → β = x))›
          using "uniqueness:1"[THEN "≡⇩d⇩fE"] by blast
        then AOT_obtain x where ‹[F]x & [R]xy›
          using "∃E"[rotated] "&E" by blast
        AOT_thus ‹∃x ([F]x & [R]xy)› by (rule "∃I")
      qed
    qed
  qed
next
  AOT_assume ‹R |: F ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩o G›
  AOT_hence ‹R |: F ⇩1⇩-⇩1⟶ G› and ‹R |: F ⟶⇩o⇩n⇩t⇩o G›
    using "≡⇩d⇩fE"[OF "fFG:4"] "&E" by blast+
  AOT_hence C: ‹R |: F ⟶ G›
    and D: ‹∀x∀y∀z ([F]x & [F]y & [G]z → ([R]xz & [R]yz → x = y))›
    and E: ‹∀y ([G]y → ∃x ([F]x & [R]xy))›
    using "≡⇩d⇩fE"[OF "fFG:2"] "≡⇩d⇩fE"[OF "fFG:3"] "&E" by blast+
  AOT_show ‹R |: F ⇩1⇩-⇩1⟷ G›
  proof(rule "1-1-cor"[THEN "≡⇩d⇩fI"]; safe intro!: "&I" "cqt:2[const_var]"[axiom_inst])
    AOT_show ‹∀x ([F]x → ∃!y ([G]y & [R]xy))›
      using "≡⇩d⇩fE"[OF "fFG:1", OF C] "&E" by blast
  next
    AOT_show ‹∀y ([G]y → ∃!x ([F]x & [R]xy))›
    proof (rule "GEN"; rule "→I")
      fix y
      AOT_assume 0: ‹[G]y›
      AOT_hence ‹∃x ([F]x & [R]xy)›
        using E "∀E" "→E" by fast
      then AOT_obtain a where a_prop: ‹[F]a & [R]ay›
        using "∃E"[rotated] by blast
      moreover AOT_have ‹∀z ([F]z & [R]zy → z = a)›
      proof (rule GEN; rule "→I")
        fix z
        AOT_assume ‹[F]z & [R]zy›
        AOT_thus ‹z = a›
          using D[THEN "∀E"(2)[where β=z], THEN "∀E"(2)[where β=a],
                  THEN "∀E"(2)[where β=y], THEN "→E", THEN "→E"]
                a_prop 0 "&E" "&I" by metis
      qed
      ultimately AOT_have ‹∃x ([F]x & [R]xy & ∀z ([F]z & [R]zy → z = x))›
        using "&I" "∃I"(2) by fast
      AOT_thus ‹∃!x ([F]x & [R]xy)›
        using "uniqueness:1"[THEN "≡⇩d⇩fI"] by fast
    qed
  qed
qed

text‹We have already introduced the restricted type of Ordinary objects in the
     Extended Relation Comprehension theory. However, make sure all variable names
     are defined as expected (avoiding conflicts with situations
     of possible world theory).›
AOT_register_variable_names
  Ordinary: u v r t s

AOT_theorem "equi:1": ‹∃!u φ{u} ≡ ∃u (φ{u} & ∀v (φ{v} → v =⇩E u))›
proof(rule "≡I"; rule "→I")
  AOT_assume ‹∃!u φ{u}›
  AOT_hence ‹∃!x (O!x & φ{x})›.
  AOT_hence ‹∃x (O!x & φ{x} & ∀β (O!β & φ{β} → β = x))›
    using "uniqueness:1"[THEN "≡⇩d⇩fE"] by blast
  then AOT_obtain x where x_prop: ‹O!x & φ{x} & ∀β (O!β & φ{β} → β = x)›
    using "∃E"[rotated] by blast
  {
    fix β
    AOT_assume beta_ord: ‹O!β›
    moreover AOT_assume ‹φ{β}›
    ultimately AOT_have ‹β = x›
      using x_prop[THEN "&E"(2), THEN "∀E"(2)[where β=β]] "&I" "→E" by blast
    AOT_hence ‹β =⇩E x›
      using "ord-=E=:1"[THEN "→E", OF "∨I"(1)[OF beta_ord],
                        THEN "qml:2"[axiom_inst, THEN "→E"],
                        THEN "≡E"(1)]
      by blast
  }
  AOT_hence ‹(O!β → (φ{β} → β =⇩E x))› for β
    using "→I" by blast
  AOT_hence ‹∀β(O!β → (φ{β} → β =⇩E x))›
    by (rule GEN)
  AOT_hence ‹O!x & φ{x} & ∀y (O!y → (φ{y} → y =⇩E x))›
    using x_prop[THEN "&E"(1)] "&I" by blast
  AOT_hence ‹O!x & (φ{x} & ∀y (O!y → (φ{y} → y =⇩E x)))›
    using "&E" "&I" by meson
  AOT_thus ‹∃u (φ{u} & ∀v (φ{v} → v =⇩E u))›
    using "∃I" by fast
next
  AOT_assume ‹∃u (φ{u} & ∀v (φ{v} → v =⇩E u))›
  AOT_hence ‹∃x (O!x & (φ{x} & ∀y (O!y → (φ{y} → y =⇩E x))))›
    by blast
  then AOT_obtain x where x_prop: ‹O!x & (φ{x} & ∀y (O!y → (φ{y} → y =⇩E x)))›
    using "∃E"[rotated] by blast
  AOT_have ‹∀y ([O!]y & φ{y} → y = x)›
  proof(rule GEN; rule "→I")
    fix y
    AOT_assume ‹O!y & φ{y}›
    AOT_hence ‹y =⇩E x›
      using x_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=y]]
            "→E" "&E" by blast
    AOT_thus ‹y = x›
      using "ord-=E=:1"[THEN "→E", OF "∨I"(2)[OF x_prop[THEN "&E"(1)]],
                        THEN "qml:2"[axiom_inst, THEN "→E"], THEN "≡E"(2)] by blast
  qed
  AOT_hence ‹[O!]x & φ{x} & ∀y ([O!]y & φ{y} → y = x)›
    using x_prop "&E" "&I" by meson
  AOT_hence ‹∃x ([O!]x & φ{x} & ∀y ([O!]y & φ{y} → y = x))›
    by (rule "∃I")
  AOT_hence ‹∃!x (O!x & φ{x})›
    by (rule "uniqueness:1"[THEN "≡⇩d⇩fI"])
  AOT_thus ‹∃!u φ{u}›.
qed

AOT_define CorrelatesEOneToOne :: ‹τ ⇒ τ ⇒ τ ⇒ φ› (‹_ |: _ ⇩1⇩-⇩1⟷⇩E _›)
  "equi:2": ‹R |: F ⇩1⇩-⇩1⟷⇩E G ≡⇩d⇩f R↓ & F↓ & G↓ &
                               ∀u ([F]u → ∃!v([G]v & [R]uv)) &
                               ∀v ([G]v → ∃!u([F]u & [R]uv))›

AOT_define EquinumerousE :: ‹τ ⇒ τ ⇒ φ› (infixl "≈⇩E" 50)
  "equi:3": ‹F ≈⇩E G ≡⇩d⇩f ∃R (R |: F ⇩1⇩-⇩1⟷⇩E G)›

text‹Note: not explicitly in PLM.›
AOT_theorem eq_den_1: ‹Π↓› if ‹Π ≈⇩E Π'›
proof -
  AOT_have ‹∃R (R |: Π ⇩1⇩-⇩1⟷⇩E Π')›
    using "equi:3"[THEN "≡⇩d⇩fE"] that by blast
  then AOT_obtain R where ‹R |: Π ⇩1⇩-⇩1⟷⇩E Π'›
    using "∃E"[rotated] by blast
  AOT_thus ‹Π↓›
    using "equi:2"[THEN "≡⇩d⇩fE"] "&E" by blast
qed

text‹Note: not explicitly in PLM.›
AOT_theorem eq_den_2: ‹Π'↓› if ‹Π ≈⇩E Π'›
proof -
  AOT_have ‹∃R (R |: Π ⇩1⇩-⇩1⟷⇩E Π')›
    using "equi:3"[THEN "≡⇩d⇩fE"] that by blast
  then AOT_obtain R where ‹R |: Π ⇩1⇩-⇩1⟷⇩E Π'›
    using "∃E"[rotated] by blast
  AOT_thus ‹Π'↓›
    using "equi:2"[THEN "≡⇩d⇩fE"] "&E" by blast+
qed

AOT_theorem "eq-part:1": ‹F ≈⇩E F›
proof (safe intro!: "&I" GEN "→I" "cqt:2[const_var]"[axiom_inst]
                    "≡⇩d⇩fI"[OF "equi:3"] "≡⇩d⇩fI"[OF "equi:2"] "∃I"(1))
  fix x
  AOT_assume 1: ‹O!x›
  AOT_assume 2: ‹[F]x›
  AOT_show ‹∃!v ([F]v & x =⇩E v)›
  proof(rule "equi:1"[THEN "≡E"(2)];
        rule "∃I"(2)[where β=x];
        safe dest!: "&E"(2)
             intro!:  "&I" "→I" 1 2 Ordinary.GEN "ord=Eequiv:1"[THEN "→E", OF 1])
    AOT_show ‹v =⇩E x› if ‹x =⇩E v› for v
      by (metis that "ord=Eequiv:2"[THEN "→E"])
  qed
next
  fix y
  AOT_assume 1: ‹O!y›
  AOT_assume 2: ‹[F]y›
  AOT_show ‹∃!u ([F]u & u =⇩E y)›
    by(safe dest!: "&E"(2)
            intro!: "equi:1"[THEN "≡E"(2)] "∃I"(2)[where β=y]
                    "&I" "→I" 1 2 GEN "ord=Eequiv:1"[THEN "→E", OF 1])
qed(auto simp: "=E[denotes]")


AOT_theorem "eq-part:2": ‹F ≈⇩E G → G ≈⇩E F›
proof (rule "→I")
  AOT_assume ‹F ≈⇩E G›
  AOT_hence ‹∃R R |: F ⇩1⇩-⇩1⟷⇩E G›
    using "equi:3"[THEN "≡⇩d⇩fE"] by blast
  then AOT_obtain R where ‹R |: F ⇩1⇩-⇩1⟷⇩E G›
    using "∃E"[rotated] by blast
  AOT_hence 0: ‹R↓ & F↓ & G↓ & ∀u ([F]u → ∃!v([G]v & [R]uv)) &
                            ∀v ([G]v → ∃!u([F]u & [R]uv))›
    using "equi:2"[THEN "≡⇩d⇩fE"] by blast

  AOT_have ‹[λxy [R]yx]↓ & G↓ & F↓ & ∀u ([G]u → ∃!v([F]v & [λxy [R]yx]uv)) &
                            ∀v ([F]v → ∃!u([G]u & [λxy [R]yx]uv))›
  proof (AOT_subst ‹[λxy [R]yx]yx› ‹[R]xy› for: x y;
        (safe intro!: "&I" "cqt:2[const_var]"[axiom_inst] 0[THEN "&E"(2)]
                      0[THEN "&E"(1), THEN "&E"(2)]; "cqt:2[lambda]")?)
    AOT_modally_strict {
      AOT_have ‹[λxy [R]yx]xy› if ‹[R]yx› for y x
        by (auto intro!: "β←C"(1) "cqt:2"
                 simp: "&I" "ex:1:a" prod_denotesI "rule-ui:3" that)
      moreover AOT_have ‹[R]yx› if ‹[λxy [R]yx]xy› for y x
        using "β→C"(1)[where φ="λ(x,y). _ (x,y)" and κ⇩1κ⇩n="(_,_)",
                        simplified, OF that, simplified].
      ultimately AOT_show ‹[λxy [R]yx]αβ ≡ [R]βα› for α β
        by (metis "deduction-theorem" "≡I")
    }
  qed
  AOT_hence ‹[λxy [R]yx] |: G ⇩1⇩-⇩1⟷⇩E F›
    using "equi:2"[THEN "≡⇩d⇩fI"] by blast
  AOT_hence ‹∃R R |: G ⇩1⇩-⇩1⟷⇩E F›
    by (rule "∃I"(1)) "cqt:2[lambda]"
  AOT_thus ‹G ≈⇩E F›
    using "equi:3"[THEN "≡⇩d⇩fI"] by blast
qed

text‹Note: not explicitly in PLM.›
AOT_theorem "eq-part:2[terms]": ‹Π ≈⇩E Π' → Π' ≈⇩E Π›
  using "eq-part:2"[unvarify F G] eq_den_1 eq_den_2 "→I" by meson
declare "eq-part:2[terms]"[THEN "→E", sym]

AOT_theorem "eq-part:3": ‹(F ≈⇩E G & G ≈⇩E H) → F ≈⇩E H›
proof (rule "→I")
  AOT_assume ‹F ≈⇩E G & G ≈⇩E H›
  then AOT_obtain R⇩1 and R⇩2 where
       ‹R⇩1 |: F ⇩1⇩-⇩1⟷⇩E G›
   and ‹R⇩2 |: G ⇩1⇩-⇩1⟷⇩E H›
    using "equi:3"[THEN "≡⇩d⇩fE"] "&E" "∃E"[rotated] by metis
  AOT_hence θ: ‹∀u ([F]u → ∃!v([G]v & [R⇩1]uv)) & ∀v ([G]v → ∃!u([F]u & [R⇩1]uv))›
        and ξ: ‹∀u ([G]u → ∃!v([H]v & [R⇩2]uv)) & ∀v ([H]v → ∃!u([G]u & [R⇩2]uv))›
    using "equi:2"[THEN "≡⇩d⇩fE", THEN "&E"(2)]
          "equi:2"[THEN "≡⇩d⇩fE", THEN "&E"(1), THEN "&E"(2)]
          "&I" by blast+
  AOT_have ‹∃R R = [λxy O!x & O!y & ∃v ([G]v & [R⇩1]xv & [R⇩2]vy)]›
    by (rule "free-thms:3[lambda]") cqt_2_lambda_inst_prover
  then AOT_obtain R where R_def: ‹R = [λxy O!x & O!y & ∃v ([G]v & [R⇩1]xv & [R⇩2]vy)]›
    using "∃E"[rotated] by blast
  AOT_have 1: ‹∃!v (([H]v & [R]uv))› if a: ‹[O!]u› and b: ‹[F]u› for u
  proof (rule "≡E"(2)[OF "equi:1"])
    AOT_obtain b where
      b_prop: ‹[O!]b & ([G]b & [R⇩1]ub & ∀v ([G]v & [R⇩1]uv → v =⇩E b))›
      using θ[THEN "&E"(1), THEN "∀E"(2), THEN "→E", THEN "→E",
              OF a b, THEN "≡E"(1)[OF "equi:1"]]
            "∃E"[rotated] by blast
    AOT_obtain c where
      c_prop: "[O!]c & ([H]c & [R⇩2]bc & ∀v ([H]v & [R⇩2]bv → v =⇩E c))"
      using ξ[THEN "&E"(1), THEN "∀E"(2)[where β=b], THEN "→E",
              OF b_prop[THEN "&E"(1)], THEN "→E",
              OF b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(1)],
              THEN "≡E"(1)[OF "equi:1"]]
    "∃E"[rotated] by blast
    AOT_show ‹∃v ([H]v & [R]uv & ∀v' ([H]v' & [R]uv' → v' =⇩E v))›
    proof (safe intro!: "&I" GEN "→I" "∃I"(2)[where β=c])
      AOT_show ‹O!c› using c_prop "&E" by blast
    next
      AOT_show ‹[H]c› using c_prop "&E" by blast
    next
      AOT_have 0: ‹[O!]u & [O!]c & ∃v ([G]v & [R⇩1]uv & [R⇩2]vc)›
        by (safe intro!: "&I" a c_prop[THEN "&E"(1)] "∃I"(2)[where β=b]
                         b_prop[THEN "&E"(1)] b_prop[THEN "&E"(2), THEN "&E"(1)]
                         c_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)])
      AOT_show ‹[R]uc›
        by (auto intro: "rule=E"[rotated, OF R_def[symmetric]]
                 intro!: "β←C"(1) "cqt:2"
                 simp: "&I" "ex:1:a" prod_denotesI "rule-ui:3" 0)
    next
      fix x
      AOT_assume ordx: ‹O!x›
      AOT_assume ‹[H]x & [R]ux›
      AOT_hence hx: ‹[H]x› and ‹[R]ux› using "&E" by blast+
      AOT_hence ‹[λxy O!x & O!y & ∃v ([G]v & [R⇩1]xv & [R⇩2]vy)]ux›
        using "rule=E"[rotated, OF R_def] by fast
      AOT_hence ‹O!u & O!x & ∃v ([G]v & [R⇩1]uv & [R⇩2]vx)›
        by (rule "β→C"(1)[where φ="λ(κ,κ'). _ κ κ'" and κ⇩1κ⇩n="(_,_)", simplified])
      then AOT_obtain z where z_prop: ‹O!z & ([G]z & [R⇩1]uz & [R⇩2]zx)›
        using "&E" "∃E"[rotated] by blast
      AOT_hence ‹z =⇩E b›
        using b_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=z]]
        using "&E" "→E" by metis
      AOT_hence ‹z = b›
        by (metis "=E-simple:2"[THEN "→E"])
      AOT_hence ‹[R⇩2]bx›
        using z_prop[THEN "&E"(2), THEN "&E"(2)] "rule=E" by fast
      AOT_thus ‹x =⇩E c›
        using c_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=x],
                     THEN "→E", THEN "→E", OF ordx]
              hx "&I" by blast
    qed
  qed
  AOT_have 2: ‹∃!u (([F]u & [R]uv))› if a: ‹[O!]v› and b: ‹[H]v› for v
  proof (rule "≡E"(2)[OF "equi:1"])
    AOT_obtain b where
      b_prop: ‹[O!]b & ([G]b & [R⇩2]bv & ∀u ([G]u & [R⇩2]uv → u =⇩E b))›
      using ξ[THEN "&E"(2), THEN "∀E"(2), THEN "→E", THEN "→E",
              OF a b, THEN "≡E"(1)[OF "equi:1"]]
            "∃E"[rotated] by blast
    AOT_obtain c where
      c_prop: "[O!]c & ([F]c & [R⇩1]cb & ∀v ([F]v & [R⇩1]vb → v =⇩E c))"
      using θ[THEN "&E"(2), THEN "∀E"(2)[where β=b], THEN "→E",
              OF b_prop[THEN "&E"(1)], THEN "→E",
              OF b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(1)],
              THEN "≡E"(1)[OF "equi:1"]]
    "∃E"[rotated] by blast
    AOT_show ‹∃u ([F]u & [R]uv & ∀v' ([F]v' & [R]v'v → v' =⇩E u))›
    proof (safe intro!: "&I" GEN "→I" "∃I"(2)[where β=c])
      AOT_show ‹O!c› using c_prop "&E" by blast
    next
      AOT_show ‹[F]c› using c_prop "&E" by blast
    next
      AOT_have ‹[O!]c & [O!]v & ∃u ([G]u & [R⇩1]cu & [R⇩2]uv)›
        by (safe intro!: "&I" a "∃I"(2)[where β=b] 
                     c_prop[THEN "&E"(1)] b_prop[THEN "&E"(1)]
                     b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(1)]
                     b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)]
                     c_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)])
      AOT_thus ‹[R]cv›
        by (auto intro: "rule=E"[rotated, OF R_def[symmetric]]
                 intro!: "β←C"(1) "cqt:2"
                 simp: "&I" "ex:1:a" prod_denotesI "rule-ui:3")
    next
      fix x
      AOT_assume ordx: ‹O!x›
      AOT_assume ‹[F]x & [R]xv›
      AOT_hence hx: ‹[F]x› and ‹[R]xv› using "&E" by blast+
      AOT_hence ‹[λxy O!x & O!y & ∃v ([G]v & [R⇩1]xv & [R⇩2]vy)]xv›
        using "rule=E"[rotated, OF R_def] by fast
      AOT_hence ‹O!x & O!v & ∃u ([G]u & [R⇩1]xu & [R⇩2]uv)›
        by (rule "β→C"(1)[where φ="λ(κ,κ'). _ κ κ'" and κ⇩1κ⇩n="(_,_)", simplified])
      then AOT_obtain z where z_prop: ‹O!z & ([G]z & [R⇩1]xz & [R⇩2]zv)›
        using "&E" "∃E"[rotated] by blast
      AOT_hence ‹z =⇩E b›
        using b_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=z]]
        using "&E" "→E" "&I" by metis
      AOT_hence ‹z = b›
        by (metis "=E-simple:2"[THEN "→E"])
      AOT_hence ‹[R⇩1]xb›
        using z_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)] "rule=E" by fast
      AOT_thus ‹x =⇩E c›
        using c_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=x],
                     THEN "→E", THEN "→E", OF ordx]
              hx "&I" by blast
    qed
  qed
  AOT_show ‹F ≈⇩E H›
    apply (rule "equi:3"[THEN "≡⇩d⇩fI"])
    apply (rule "∃I"(2)[where β=R])
    by (auto intro!: 1 2 "equi:2"[THEN "≡⇩d⇩fI"] "&I" "cqt:2[const_var]"[axiom_inst]
                     Ordinary.GEN "→I" Ordinary.ψ)
qed

text‹Note: not explicitly in PLM.›
AOT_theorem "eq-part:3[terms]": ‹Π ≈⇩E Π''› if ‹Π ≈⇩E Π'› and ‹Π' ≈⇩E Π''›
  using "eq-part:3"[unvarify F G H, THEN "→E"] eq_den_1 eq_den_2 "→I" "&I"
  by (metis that(1) that(2))
declare "eq-part:3[terms]"[trans]

AOT_theorem "eq-part:4": ‹F ≈⇩E G ≡ ∀H (H ≈⇩E F ≡ H ≈⇩E G)›
proof(rule "≡I"; rule "→I")
  AOT_assume 0: ‹F ≈⇩E G›
  AOT_hence 1: ‹G ≈⇩E F› using "eq-part:2"[THEN "→E"] by blast
  AOT_show ‹∀H (H ≈⇩E F ≡ H ≈⇩E G)›
  proof (rule GEN; rule "≡I"; rule "→I")
    AOT_show ‹H ≈⇩E G› if ‹H ≈⇩E F› for H using 0
      by (meson "&I" "eq-part:3" that "vdash-properties:6")
  next
    AOT_show ‹H ≈⇩E F› if ‹H ≈⇩E G› for H using 1
      by (metis "&I" "eq-part:3" that "vdash-properties:6")
  qed
next
  AOT_assume ‹∀H (H ≈⇩E F ≡ H ≈⇩E G)›
  AOT_hence ‹F ≈⇩E F ≡ F ≈⇩E G› using "∀E" by blast
  AOT_thus ‹F ≈⇩E G› using "eq-part:1" "≡E" by blast
qed

AOT_define MapsE :: ‹τ ⇒ τ ⇒ τ ⇒ φ› ("_ |: _ ⟶E _")
  "equi-rem:1":
  ‹R |: F ⟶E G ≡⇩d⇩f R↓ & F↓ & G↓ & ∀u ([F]u → ∃!v ([G]v & [R]uv))›

AOT_define MapsEOneToOne :: ‹τ ⇒ τ ⇒ τ ⇒ φ› ("_ |: _ ⇩1⇩-⇩1⟶E _")
  "equi-rem:2":
  ‹R |: F ⇩1⇩-⇩1⟶E G ≡⇩d⇩f
      R |: F ⟶E G & ∀t∀u∀v (([F]t & [F]u & [G]v) → ([R]tv & [R]uv → t =⇩E u))›

AOT_define MapsEOnto :: ‹τ ⇒ τ ⇒ τ ⇒ φ› ("_ |: _ ⟶⇩o⇩n⇩t⇩oE _")
  "equi-rem:3":
  ‹R |: F ⟶⇩o⇩n⇩t⇩oE G ≡⇩d⇩f R |: F ⟶E G & ∀v ([G]v → ∃u ([F]u & [R]uv))›

AOT_define MapsEOneToOneOnto :: ‹τ ⇒ τ ⇒ τ ⇒ φ› ("_ |: _ ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩oE _")
  "equi-rem:4":
  ‹R |: F ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩oE G ≡⇩d⇩f R |: F ⇩1⇩-⇩1⟶E G & R |: F ⟶⇩o⇩n⇩t⇩oE G›

AOT_theorem "equi-rem-thm":
  ‹R |: F ⇩1⇩-⇩1⟷⇩E G ≡ R |: F ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩oE G›
proof -
  AOT_have ‹R |: F ⇩1⇩-⇩1⟷⇩E G ≡ R |: [λx O!x & [F]x] ⇩1⇩-⇩1⟷ [λx O!x & [G]x]›
  proof(safe intro!: "≡I" "→I" "&I")
    AOT_assume ‹R |: F ⇩1⇩-⇩1⟷⇩E G›
    AOT_hence ‹∀u ([F]u → ∃!v ([G]v & [R]uv))›
          and ‹∀v ([G]v → ∃!u ([F]u & [R]uv))›
      using "equi:2"[THEN "≡⇩d⇩fE"] "&E" by blast+
    AOT_hence a: ‹([F]u → ∃!v ([G]v & [R]uv))›
          and b: ‹([G]v → ∃!u ([F]u & [R]uv))› for u v
      using "Ordinary.∀E" by fast+
    AOT_have ‹([λx [O!]x & [F]x]x → ∃!y ([λx [O!]x & [G]x]y & [R]xy))› for x
      apply (AOT_subst ‹[λx [O!]x & [F]x]x› ‹[O!]x & [F]x›)
       apply (rule "beta-C-meta"[THEN "→E"])
       apply "cqt:2[lambda]"
      apply (AOT_subst ‹[λx [O!]x & [G]x]x› ‹[O!]x & [G]x› for: x)
       apply (rule "beta-C-meta"[THEN "→E"])
       apply "cqt:2[lambda]"
      apply (AOT_subst ‹O!y & [G]y & [R]xy› ‹O!y & ([G]y & [R]xy)› for: y)
       apply (meson "≡E"(6) "Associativity of &" "oth-class-taut:3:a")
      apply (rule "→I") apply (frule "&E"(1)) apply (drule "&E"(2))
      by (fact a[unconstrain u, THEN "→E", THEN "→E", of x])
    AOT_hence A: ‹∀x ([λx [O!]x & [F]x]x → ∃!y ([λx [O!]x & [G]x]y & [R]xy))›
      by (rule GEN)
    AOT_have ‹([λx [O!]x & [G]x]y → ∃!x ([λx [O!]x & [F]x]x & [R]xy))› for y
      apply (AOT_subst ‹[λx [O!]x & [G]x]y› ‹[O!]y & [G]y›)
       apply (rule "beta-C-meta"[THEN "→E"])
       apply "cqt:2[lambda]"
      apply (AOT_subst ‹[λx [O!]x & [F]x]x› ‹[O!]x & [F]x› for: x)
       apply (rule "beta-C-meta"[THEN "→E"])
       apply "cqt:2[lambda]"
      apply (AOT_subst ‹O!x & [F]x & [R]xy› ‹O!x & ([F]x & [R]xy)› for: x)
       apply (meson "≡E"(6) "Associativity of &" "oth-class-taut:3:a")
      apply (rule "→I") apply (frule "&E"(1)) apply (drule "&E"(2))
      by (fact b[unconstrain v, THEN "→E", THEN "→E", of y])
    AOT_hence B: ‹∀y ([λx [O!]x & [G]x]y → ∃!x ([λx [O!]x & [F]x]x & [R]xy))›
      by (rule GEN)
    AOT_show ‹R |: [λx [O!]x & [F]x] ⇩1⇩-⇩1⟷ [λx [O!]x & [G]x]›
      by (safe intro!: "1-1-cor"[THEN "≡⇩d⇩fI"] "&I"
                       "cqt:2[const_var]"[axiom_inst] A B)
          "cqt:2[lambda]"+
  next
    AOT_assume ‹R |: [λx [O!]x & [F]x] ⇩1⇩-⇩1⟷ [λx [O!]x & [G]x]›
    AOT_hence a: ‹([λx [O!]x & [F]x]x → ∃!y ([λx [O!]x & [G]x]y & [R]xy))› and 
              b: ‹([λx [O!]x & [G]x]y → ∃!x ([λx [O!]x & [F]x]x & [R]xy))› for x y
      using "1-1-cor"[THEN "≡⇩d⇩fE"] "&E" "∀E"(2) by blast+
    AOT_have ‹[F]u → ∃!v ([G]v & [R]uv)› for u
    proof (safe intro!: "→I")
      AOT_assume fu: ‹[F]u›
      AOT_have 0: ‹[λx [O!]x & [F]x]u›
        by (auto intro!: "β←C"(1) "cqt:2" "cqt:2[const_var]"[axiom_inst]
                         Ordinary.ψ fu "&I")
      AOT_show ‹∃!v ([G]v & [R]uv)›
        apply (AOT_subst ‹[O!]x & ([G]x & [R]ux)›
                         ‹([O!]x & [G]x) & [R]ux› for: x)
         apply (simp add: "Associativity of &")
        apply (AOT_subst (reverse) ‹[O!]x & [G]x›
                                   ‹[λx [O!]x & [G]x]x› for: x)
         apply (rule "beta-C-meta"[THEN "→E"])
         apply "cqt:2[lambda]"
        using a[THEN "→E", OF 0] by blast
    qed
    AOT_hence A: ‹∀u ([F]u → ∃!v ([G]v & [R]uv))›
      by (rule Ordinary.GEN)
    AOT_have ‹[G]v → ∃!u ([F]u & [R]uv)› for v
    proof (safe intro!: "→I")
      AOT_assume gu: ‹[G]v›
      AOT_have 0: ‹[λx [O!]x & [G]x]v›
        by (auto intro!: "β←C"(1) "cqt:2" "cqt:2[const_var]"[axiom_inst]
                         Ordinary.ψ gu "&I")
      AOT_show ‹∃!u ([F]u & [R]uv)›
        apply (AOT_subst ‹[O!]x & ([F]x & [R]xv)› ‹([O!]x & [F]x) & [R]xv› for: x)
         apply (simp add: "Associativity of &")
        apply (AOT_subst (reverse) ‹[O!]x & [F]x›‹[λx [O!]x & [F]x]x›  for: x)
         apply (rule "beta-C-meta"[THEN "→E"])
         apply "cqt:2[lambda]"
        using b[THEN "→E", OF 0] by blast
    qed
    AOT_hence B: ‹∀v ([G]v → ∃!u ([F]u & [R]uv))› by (rule Ordinary.GEN)
    AOT_show ‹R |: F ⇩1⇩-⇩1⟷⇩E G›
      by (safe intro!: "equi:2"[THEN "≡⇩d⇩fI"] "&I" A B "cqt:2[const_var]"[axiom_inst])
  qed
  also AOT_have ‹… ≡ R |: F ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩oE G›
  proof(safe intro!: "≡I" "→I" "&I")
    AOT_assume ‹R |: [λx [O!]x & [F]x] ⇩1⇩-⇩1⟷ [λx [O!]x & [G]x]›
    AOT_hence a: ‹([λx [O!]x & [F]x]x → ∃!y ([λx [O!]x & [G]x]y & [R]xy))› and 
              b: ‹([λx [O!]x & [G]x]y → ∃!x ([λx [O!]x & [F]x]x & [R]xy))› for x y
      using "1-1-cor"[THEN "≡⇩d⇩fE"] "&E" "∀E"(2) by blast+
    AOT_show ‹R |: F ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩oE G›
    proof (safe intro!: "equi-rem:4"[THEN "≡⇩d⇩fI"] "&I" "equi-rem:3"[THEN "≡⇩d⇩fI"]
                        "equi-rem:2"[THEN "≡⇩d⇩fI"] "equi-rem:1"[THEN "≡⇩d⇩fI"]
                        "cqt:2[const_var]"[axiom_inst] Ordinary.GEN "→I")
      fix u
      AOT_assume fu: ‹[F]u›
      AOT_have 0: ‹[λx [O!]x & [F]x]u›
        by (auto intro!: "β←C"(1) "cqt:2" "cqt:2[const_var]"[axiom_inst]
                         Ordinary.ψ fu "&I")
      AOT_hence 1: ‹∃!y ([λx [O!]x & [G]x]y & [R]uy)›
        using a[THEN "→E"] by blast
      AOT_show ‹∃!v ([G]v & [R]uv)›
        apply (AOT_subst ‹[O!]x & ([G]x & [R]ux)› ‹([O!]x & [G]x) & [R]ux› for: x)
         apply (simp add: "Associativity of &")
        apply (AOT_subst (reverse) ‹[O!]x & [G]x› ‹[λx [O!]x & [G]x]x› for: x)
         apply (rule "beta-C-meta"[THEN "→E"])
         apply "cqt:2[lambda]"
        by (fact 1)
    next
      fix t u v
      AOT_assume ‹[F]t & [F]u & [G]v› and rtv_tuv: ‹[R]tv & [R]uv›
      AOT_hence oft: ‹[λx O!x & [F]x]t› and
                ofu: ‹[λx O!x & [F]x]u› and
                ogv: ‹[λx O!x & [G]x]v›
        by (auto intro!: "β←C"(1) "cqt:2" "&I"
                 simp: Ordinary.ψ dest: "&E")
      AOT_hence ‹∃!x ([λx [O!]x & [F]x]x & [R]xv)›
        using b[THEN "→E"] by blast
      then AOT_obtain a where
          a_prop: ‹[λx [O!]x & [F]x]a & [R]av &
                   ∀x (([λx [O!]x & [F]x]x & [R]xv) → x = a)›
        using "uniqueness:1"[THEN "≡⇩d⇩fE"] "∃E"[rotated] by blast
      AOT_hence ua: ‹u = a›
        using ofu rtv_tuv[THEN "&E"(2)] "∀E"(2) "→E" "&I" "&E"(2) by blast
      moreover AOT_have ta: ‹t = a›
        using a_prop oft rtv_tuv[THEN "&E"(1)] "∀E"(2) "→E" "&I" "&E"(2) by blast
      ultimately AOT_have ‹t = u› by (metis "rule=E" id_sym)
      AOT_thus ‹t =⇩E u›
        using "rule=E" id_sym "ord=Eequiv:1" Ordinary.ψ ta ua "→E" by fast
    next
      fix u
      AOT_assume ‹[F]u›
      AOT_hence ‹[λx O!x & [F]x]u›
        by (auto intro!: "β←C"(1) "cqt:2" "&I"
                 simp: "cqt:2[const_var]"[axiom_inst]  Ordinary.ψ)
      AOT_hence ‹∃!y ([λx [O!]x & [G]x]y & [R]uy)›
        using a[THEN "→E"] by blast
      then AOT_obtain a where
        a_prop: ‹[λx [O!]x & [G]x]a & [R]ua &
                 ∀x (([λx [O!]x & [G]x]x & [R]ux) → x = a)›
        using "uniqueness:1"[THEN "≡⇩d⇩fE"] "∃E"[rotated] by blast
      AOT_have ‹O!a & [G]a›
        by (rule "β→C"(1)) (auto simp: a_prop[THEN "&E"(1), THEN "&E"(1)])
      AOT_hence ‹O!a› and ‹[G]a› using "&E" by blast+
      moreover AOT_have ‹∀v ([G]v & [R]uv → v =⇩E a)›
      proof(safe intro!: Ordinary.GEN "→I"; frule "&E"(1); drule "&E"(2))
        fix v
        AOT_assume ‹[G]v› and ruv: ‹[R]uv›
        AOT_hence ‹[λx [O!]x & [G]x]v›
          by (auto intro!: "β←C"(1) "cqt:2" "&I" simp: Ordinary.ψ)
        AOT_hence ‹v = a›
          using a_prop[THEN "&E"(2), THEN "∀E"(2), THEN "→E", OF "&I"] ruv by blast
        AOT_thus ‹v =⇩E a›
          using "rule=E" "ord=Eequiv:1" Ordinary.ψ "→E" by fast
      qed
      ultimately AOT_have ‹O!a & ([G]a & [R]ua & ∀v' ([G]v' & [R]uv' → v' =⇩E a))›
        using "∃I" "&I" a_prop[THEN "&E"(1), THEN "&E"(2)] by simp
      AOT_hence ‹∃v ([G]v & [R]uv & ∀v' ([G]v' & [R]uv' → v' =⇩E v))›
        by (rule "∃I")
      AOT_thus ‹∃!v ([G]v & [R]uv)›
        by (rule "equi:1"[THEN "≡E"(2)])
    next
      fix v
      AOT_assume ‹[G]v›
      AOT_hence ‹[λx O!x & [G]x]v›
        by (auto intro!: "β←C"(1) "cqt:2" "&I" Ordinary.ψ)
      AOT_hence ‹∃!x ([λx [O!]x & [F]x]x & [R]xv)›
        using b[THEN "→E"] by blast
      then AOT_obtain a where
        a_prop: ‹[λx [O!]x & [F]x]a & [R]av &
                 ∀y ([λx [O!]x & [F]x]y & [R]yv → y = a)›
        using "uniqueness:1"[THEN "≡⇩d⇩fE", THEN "∃E"[rotated]] by blast
      AOT_have ‹O!a & [F]a›
        by (rule "β→C"(1)) (auto simp: a_prop[THEN "&E"(1), THEN "&E"(1)])
      AOT_hence ‹O!a & ([F]a & [R]av)›
        using a_prop[THEN "&E"(1), THEN "&E"(2)] "&E" "&I" by metis
      AOT_thus ‹∃u ([F]u & [R]uv)›
        by (rule "∃I")
    qed
  next
    AOT_assume ‹R |: F ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩oE G›
    AOT_hence 1: ‹R |: F ⇩1⇩-⇩1⟶E G›
          and 2: ‹R |: F ⟶⇩o⇩n⇩t⇩oE G›
      using "equi-rem:4"[THEN "≡⇩d⇩fE"] "&E" by blast+
    AOT_hence 3: ‹R |: F ⟶E G›
          and A: ‹∀t ∀u ∀v ([F]t & [F]u & [G]v → ([R]tv & [R]uv → t =⇩E u))›
      using "equi-rem:2"[THEN "≡⇩d⇩fE", OF 1] "&E" by blast+
    AOT_hence B: ‹∀u ([F]u → ∃!v ([G]v & [R]uv))›
      using "equi-rem:1"[THEN "≡⇩d⇩fE"] "&E" by blast
    AOT_have C: ‹∀v ([G]v → ∃u ([F]u & [R]uv))›
      using "equi-rem:3"[THEN "≡⇩d⇩fE", OF 2] "&E" by blast
    AOT_show ‹R |: [λx [O!]x & [F]x] ⇩1⇩-⇩1⟷ [λx [O!]x & [G]x]›
    proof (rule "1-1-cor"[THEN "≡⇩d⇩fI"];
           safe intro!: "&I" "cqt:2" GEN "→I")
      fix x
      AOT_assume 1: ‹[λx [O!]x & [F]x]x›
      AOT_have ‹O!x & [F]x›
        by (rule "β→C"(1)) (auto simp: 1)
      AOT_hence ‹∃!v ([G]v & [R]xv)›
        using B[THEN "∀E"(2), THEN "→E", THEN "→E"] "&E" by blast
      then AOT_obtain y where
        y_prop: ‹O!y & ([G]y & [R]xy & ∀u ([G]u & [R]xu → u =⇩E y))›
        using "equi:1"[THEN "≡E"(1)] "∃E"[rotated] by fastforce
      AOT_hence ‹[λx O!x & [G]x]y›
        by (auto intro!: "β←C"(1) "cqt:2" "&I" dest: "&E")
      moreover AOT_have ‹∀z ([λx O!x & [G]x]z & [R]xz → z = y)›
      proof(safe intro!: GEN "→I"; frule "&E"(1); drule "&E"(2))
        fix z
        AOT_assume 1: ‹[λx [O!]x & [G]x]z›
        AOT_have 2: ‹O!z & [G]z›
          by (rule "β→C"(1)) (auto simp: 1)
        moreover AOT_assume ‹[R]xz›
        ultimately AOT_have ‹z =⇩E y›
          using y_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2),
                       THEN "→E", THEN "→E", rotated, OF "&I"] "&E"
          by blast
        AOT_thus ‹z = y›
          using 2[THEN "&E"(1)] by (metis "=E-simple:2" "→E")
      qed
      ultimately AOT_have ‹[λx O!x & [G]x]y & [R]xy &
                           ∀z ([λx O!x & [G]x]z & [R]xz → z = y)›
        using y_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)] "&I" by auto
      AOT_hence ‹∃y ([λx O!x & [G]x]y & [R]xy &
                    ∀z ([λx O!x & [G]x]z & [R]xz → z = y))›
        by (rule "∃I")
      AOT_thus ‹∃!y ([λx [O!]x & [G]x]y & [R]xy)›
        using "uniqueness:1"[THEN "≡⇩d⇩fI"] by fast
    next
      fix y
      AOT_assume 1: ‹[λx [O!]x & [G]x]y›
      AOT_have oy_gy: ‹O!y & [G]y›
        by (rule "β→C"(1)) (auto simp: 1)
      AOT_hence ‹∃u ([F]u & [R]uy)›
        using C[THEN "∀E"(2), THEN "→E", THEN "→E"] "&E" by blast
      then AOT_obtain x where x_prop: ‹O!x & ([F]x & [R]xy)›
        using "∃E"[rotated] by blast
      AOT_hence ofx: ‹[λx O!x & [F]x]x›
        by (auto intro!: "β←C"(1) "cqt:2" "&I" dest: "&E")
      AOT_have ‹∃α ([λx [O!]x & [F]x]α & [R]αy &
                    ∀β ([λx [O!]x & [F]x]β & [R]βy → β = α))›
      proof (safe intro!: "∃I"(2)[where β=x] "&I" GEN "→I")
        AOT_show ‹[λx O!x & [F]x]x› using ofx.
      next
        AOT_show ‹[R]xy› using x_prop[THEN "&E"(2), THEN "&E"(2)].
      next
        fix z
        AOT_assume 1: ‹[λx [O!]x & [F]x]z & [R]zy›
        AOT_have oz_fz: ‹O!z & [F]z›
          by (rule "β→C"(1)) (auto simp: 1[THEN "&E"(1)])
        AOT_have ‹z =⇩E x›
          using A[THEN "∀E"(2)[where β=z], THEN "→E", THEN "∀E"(2)[where β=x],
                  THEN "→E", THEN "∀E"(2)[where β=y], THEN "→E",
                  THEN "→E", THEN "→E", OF oz_fz[THEN "&E"(1)],
                  OF x_prop[THEN "&E"(1)], OF oy_gy[THEN "&E"(1)], OF "&I", OF "&I",
                  OF oz_fz[THEN "&E"(2)], OF x_prop[THEN "&E"(2), THEN "&E"(1)],
                  OF oy_gy[THEN "&E"(2)], OF "&I", OF 1[THEN "&E"(2)],
                  OF x_prop[THEN "&E"(2), THEN "&E"(2)]].
        AOT_thus ‹z = x›
          by (metis "=E-simple:2" "vdash-properties:10")
      qed
      AOT_thus ‹∃!x ([λx [O!]x & [F]x]x & [R]xy)›
        by (rule "uniqueness:1"[THEN "≡⇩d⇩fI"])
    qed
  qed
  finally show ?thesis.
qed

AOT_theorem "empty-approx:1": ‹(¬∃u [F]u & ¬∃v [H]v) → F ≈⇩E H›
proof(rule "→I"; frule "&E"(1); drule "&E"(2))
  AOT_assume 0: ‹¬∃u [F]u› and 1: ‹¬∃v [H]v›
  AOT_have ‹∀u ([F]u → ∃!v ([H]v & [R]uv))› for R
  proof(rule Ordinary.GEN; rule "→I"; rule "raa-cor:1")
    fix u
    AOT_assume ‹[F]u›
    AOT_hence ‹∃u [F]u› using "Ordinary.∃I" "&I" by fast
    AOT_thus ‹∃u [F]u & ¬∃u [F]u› using "&I" 0 by blast
  qed
  moreover AOT_have ‹∀v ([H]v → ∃!u ([F]u & [R]uv))› for R
  proof(rule Ordinary.GEN; rule "→I"; rule "raa-cor:1")
    fix v
    AOT_assume ‹[H]v›
    AOT_hence ‹∃v [H]v› using "Ordinary.∃I" "&I" by fast
    AOT_thus ‹∃v [H]v & ¬∃v [H]v› using 1 "&I" by blast
  qed
  ultimately AOT_have ‹R |: F ⇩1⇩-⇩1⟷⇩E H› for R
    apply (safe intro!: "equi:2"[THEN "≡⇩d⇩fI"] "&I" GEN "cqt:2[const_var]"[axiom_inst])
    using "∀E" by blast+
  AOT_hence ‹∃R R |: F ⇩1⇩-⇩1⟷⇩E H› by (rule "∃I")
  AOT_thus ‹F ≈⇩E H›
    by (rule "equi:3"[THEN "≡⇩d⇩fI"])
qed

AOT_theorem "empty-approx:2": ‹(∃u [F]u & ¬∃v [H]v) → ¬(F ≈⇩E H)›
proof(rule "→I"; frule "&E"(1); drule "&E"(2); rule "raa-cor:2")
  AOT_assume 1: ‹∃u [F]u› and 2: ‹¬∃v [H]v›
  AOT_obtain b where b_prop: ‹O!b & [F]b›
    using 1 "∃E"[rotated] by blast
  AOT_assume ‹F ≈⇩E H›
  AOT_hence ‹∃R R |: F ⇩1⇩-⇩1⟷⇩E H›
    by (rule "equi:3"[THEN "≡⇩d⇩fE"])
  then AOT_obtain R where ‹R |: F ⇩1⇩-⇩1⟷⇩E H›
    using "∃E"[rotated] by blast
  AOT_hence θ: ‹∀u ([F]u → ∃!v ([H]v & [R]uv))›
    using "equi:2"[THEN "≡⇩d⇩fE"] "&E" by blast+
  AOT_have ‹∃!v ([H]v & [R]bv)› for u
    using θ[THEN "∀E"(2)[where β=b], THEN "→E", THEN "→E",
            OF b_prop[THEN "&E"(1)], OF b_prop[THEN "&E"(2)]].
  AOT_hence ‹∃v ([H]v & [R]bv & ∀u ([H]u & [R]bu → u =⇩E v))›
    by (rule "equi:1"[THEN "≡E"(1)])
  then AOT_obtain x where ‹O!x & ([H]x & [R]bx & ∀u ([H]u & [R]bu → u =⇩E x))›
    using "∃E"[rotated] by blast
  AOT_hence ‹O!x & [H]x› using "&E" "&I" by blast
  AOT_hence ‹∃v [H]v› by (rule "∃I")
  AOT_thus ‹∃v [H]v & ¬∃v [H]v› using 2 "&I" by blast
qed


AOT_define FminusU :: ‹Π ⇒ τ ⇒ Π› ("_⇧-⇧_")
  "F-u": ‹[F]⇧-⇧x =⇩d⇩f [λz [F]z & z ≠⇩E x]›

text‹Note: not explicitly in PLM.›
AOT_theorem "F-u[den]": ‹[F]⇧-⇧x↓›
  by (rule "=⇩d⇩fI"(1)[OF "F-u", where τ⇩1τ⇩n="(_,_)", simplified]; "cqt:2[lambda]")
AOT_theorem "F-u[equiv]": ‹[[F]⇧-⇧x]y ≡ ([F]y & y ≠⇩E x)›
  by (auto intro: "F-u"[THEN "=⇩d⇩fI"(1), where τ⇩1τ⇩n="(_,_)", simplified]
           intro!: "cqt:2" "beta-C-cor:2"[THEN "→E", THEN "∀E"(2)])

AOT_theorem eqP': ‹F ≈⇩E G & [F]u & [G]v → [F]⇧-⇧u ≈⇩E [G]⇧-⇧v›
proof (rule "→I"; frule "&E"(2); drule "&E"(1); frule "&E"(2); drule "&E"(1))
  AOT_assume ‹F ≈⇩E G›
  AOT_hence ‹∃R R |: F ⇩1⇩-⇩1⟷⇩E G›
    using "equi:3"[THEN "≡⇩d⇩fE"] by blast
  then AOT_obtain R where R_prop: ‹R |: F ⇩1⇩-⇩1⟷⇩E G›
    using "∃E"[rotated] by blast
  AOT_hence A: ‹∀u ([F]u → ∃!v ([G]v & [R]uv))›
        and B: ‹∀v ([G]v → ∃!u ([F]u & [R]uv))›
    using "equi:2"[THEN "≡⇩d⇩fE"] "&E" by blast+
  AOT_have ‹R |: F ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩oE G›
    using "equi-rem-thm"[THEN "≡E"(1), OF R_prop].
  AOT_hence ‹R |: F ⇩1⇩-⇩1⟶E G & R |: F ⟶⇩o⇩n⇩t⇩oE G›
    using "equi-rem:4"[THEN "≡⇩d⇩fE"] by blast
  AOT_hence C: ‹∀t∀u∀v (([F]t & [F]u & [G]v) → ([R]tv & [R]uv → t =⇩E u))›
    using "equi-rem:2"[THEN "≡⇩d⇩fE"] "&E" by blast
  AOT_assume fu: ‹[F]u›
  AOT_assume gv: ‹[G]v›
  AOT_have ‹[λz [Π]z & z ≠⇩E κ]↓› for Π κ
    by "cqt:2[lambda]"
  note Π_minus_κI = "rule-id-df:2:b[2]"[
      where τ=‹(λ(Π, κ). «[Π]⇧-⇧κ»)›, simplified, OF "F-u", simplified, OF this]
   and Π_minus_κE = "rule-id-df:2:a[2]"[
      where τ=‹(λ(Π, κ). «[Π]⇧-⇧κ»)›, simplified, OF "F-u", simplified, OF this]
  AOT_have Π_minus_κ_den: ‹[Π]⇧-⇧κ↓› for Π κ
    by (rule Π_minus_κI) "cqt:2[lambda]"+
  {
    fix R
    AOT_assume R_prop: ‹R |: F ⇩1⇩-⇩1⟷⇩E G›
    AOT_hence A: ‹∀u ([F]u → ∃!v ([G]v & [R]uv))›
          and B: ‹∀v ([G]v → ∃!u ([F]u & [R]uv))›
      using "equi:2"[THEN "≡⇩d⇩fE"] "&E" by blast+
    AOT_have ‹R |: F ⇩1⇩-⇩1⟶⇩o⇩n⇩t⇩oE G›
      using "equi-rem-thm"[THEN "≡E"(1), OF R_prop].
    AOT_hence ‹R |: F ⇩1⇩-⇩1⟶E G & R |: F ⟶⇩o⇩n⇩t⇩oE G›
      using "equi-rem:4"[THEN "≡⇩d⇩fE"] by blast
    AOT_hence C: ‹∀t∀u∀v (([F]t & [F]u & [G]v) → ([R]tv & [R]uv → t =⇩E u))›
      using "equi-rem:2"[THEN "≡⇩d⇩fE"] "&E" by blast

    AOT_assume Ruv: ‹[R]uv›
    AOT_have ‹R |: [F]⇧-⇧u ⇩1⇩-⇩1⟷⇩E [G]⇧-⇧v›
    proof(safe intro!: "equi:2"[THEN "≡⇩d⇩fI"] "&I" "cqt:2[const_var]"[axiom_inst]
                       Π_minus_κ_den Ordinary.GEN "→I")
      fix u'
      AOT_assume ‹[[F]⇧-⇧u]u'›
      AOT_hence 0: ‹[λz [F]z & z ≠⇩E u]u'›
        using Π_minus_κE by fast
      AOT_have 0: ‹[F]u' & u' ≠⇩E u›
        by (rule "β→C"(1)[where κ⇩1κ⇩n="AOT_term_of_var (Ordinary.Rep u')"]) (fact 0)
      AOT_have ‹∃!v ([G]v & [R]u'v)›
        using A[THEN "Ordinary.∀E"[where α=u'], THEN "→E", OF 0[THEN "&E"(1)]].
      then AOT_obtain v' where
        v'_prop: ‹[G]v' & [R]u'v' & ∀ t ([G]t & [R]u't → t =⇩E v')›
        using "equi:1"[THEN "≡E"(1)] "Ordinary.∃E"[rotated] by fastforce

      AOT_show ‹∃!v' ([[G]⇧-⇧v]v' & [R]u'v')›
      proof (safe intro!: "equi:1"[THEN "≡E"(2)] "Ordinary.∃I"[where β=v']
                          "&I" Ordinary.GEN "→I")
        AOT_show ‹[[G]⇧-⇧v]v'›
        proof (rule Π_minus_κI; 
               safe intro!: "β←C"(1) "cqt:2" "&I" "thm-neg=E"[THEN "≡E"(2)])
          AOT_show ‹[G]v'› using v'_prop "&E" by blast
        next
          AOT_show ‹¬v' =⇩E v›
          proof (rule "raa-cor:2")
            AOT_assume ‹v' =⇩E v›
            AOT_hence ‹v' = v› by (metis "=E-simple:2" "→E")
            AOT_hence Ruv': ‹[R]uv'› using "rule=E" Ruv id_sym by fast
            AOT_have ‹u' =⇩E u›
              by (rule C[THEN "Ordinary.∀E", THEN "Ordinary.∀E",
                         THEN "Ordinary.∀E"[where α=v'], THEN "→E", THEN "→E"])
                 (safe intro!: "&I" 0[THEN "&E"(1)] fu
                               v'_prop[THEN "&E"(1), THEN "&E"(1)]
                               Ruv' v'_prop[THEN "&E"(1), THEN "&E"(2)])
            moreover AOT_have ‹¬(u' =⇩E u)›
              using "0" "&E"(2) "≡E"(1) "thm-neg=E" by blast
            ultimately AOT_show ‹u' =⇩E u & ¬u' =⇩E u› using "&I" by blast
          qed
        qed
      next
        AOT_show ‹[R]u'v'› using v'_prop "&E" by blast
      next
        fix t
        AOT_assume t_prop: ‹[[G]⇧-⇧v]t & [R]u't›
        AOT_have gt_t_noteq_v: ‹[G]t & t ≠⇩E v›
          apply (rule "β→C"(1)[where κ⇩1κ⇩n="AOT_term_of_var (Ordinary.Rep t)"])
          apply (rule Π_minus_κE)
          by (fact t_prop[THEN "&E"(1)])
        AOT_show ‹t =⇩E v'›
          using v'_prop[THEN "&E"(2), THEN "Ordinary.∀E", THEN "→E",
                        OF "&I", OF gt_t_noteq_v[THEN "&E"(1)],
                        OF t_prop[THEN "&E"(2)]].
      qed
    next
      fix v'
      AOT_assume G_minus_v_v': ‹[[G]⇧-⇧v]v'›
      AOT_have gt_t_noteq_v: ‹[G]v' & v' ≠⇩E v›
        apply (rule "β→C"(1)[where κ⇩1κ⇩n="AOT_term_of_var (Ordinary.Rep v')"])
        apply (rule Π_minus_κE)
        by (fact G_minus_v_v')
      AOT_have ‹∃!u([F]u & [R]uv')›
        using B[THEN "Ordinary.∀E", THEN "→E", OF gt_t_noteq_v[THEN "&E"(1)]].
      then AOT_obtain u' where
        u'_prop: ‹[F]u' & [R]u'v' & ∀t ([F]t & [R]tv' → t =⇩E u')›
        using "equi:1"[THEN "≡E"(1)] "Ordinary.∃E"[rotated] by fastforce
      AOT_show ‹∃!u' ([[F]⇧-⇧u]u' & [R]u'v')›
      proof (safe intro!: "equi:1"[THEN "≡E"(2)] "Ordinary.∃I"[where β=u'] "&I"
                          u'_prop[THEN "&E"(1), THEN "&E"(2)] Ordinary.GEN "→I")
        AOT_show ‹[[F]⇧-⇧u]u'›
        proof (rule Π_minus_κI;
               safe intro!: "β←C"(1) "cqt:2" "&I" "thm-neg=E"[THEN "≡E"(2)]
               u'_prop[THEN "&E"(1), THEN "&E"(1)]; rule "raa-cor:2")
          AOT_assume u'_eq_u: ‹u' =⇩E u›
          AOT_hence ‹u' = u›
            using "=E-simple:2" "vdash-properties:10" by blast
          AOT_hence Ru'v: ‹[R]u'v› using "rule=E" Ruv id_sym by fast
          AOT_have ‹v' ≠⇩E v›
            using "&E"(2) gt_t_noteq_v by blast
          AOT_hence v'_noteq_v: ‹¬(v' =⇩E v)› by (metis "≡E"(1) "thm-neg=E")
          AOT_have ‹∃u ([G]u & [R]u'u & ∀v ([G]v & [R]u'v → v =⇩E u))›
            using A[THEN "Ordinary.∀E", THEN "→E",
                    OF u'_prop[THEN "&E"(1), THEN "&E"(1)],
                    THEN "equi:1"[THEN "≡E"(1)]].
          then AOT_obtain t where
            t_prop: ‹[G]t & [R]u't & ∀v ([G]v & [R]u'v → v =⇩E t)›
            using "Ordinary.∃E"[rotated] by meson
          AOT_have ‹v =⇩E t› if ‹[G]v› and ‹[R]u'v› for v
            using t_prop[THEN "&E"(2), THEN "Ordinary.∀E", THEN "→E",
                         OF "&I", OF that].
          AOT_hence ‹v' =⇩E t› and ‹v =⇩E t›
            by (auto simp: gt_t_noteq_v[THEN "&E"(1)] Ru'v gv
                           u'_prop[THEN "&E"(1), THEN "&E"(2)])
          AOT_hence ‹v' =⇩E v›
            using "rule=E" "=E-simple:2" id_sym "→E" by fast
          AOT_thus ‹v' =⇩E v & ¬v' =⇩E v›
            using v'_noteq_v "&I" by blast
        qed
      next
        fix t
        AOT_assume 0: ‹[[F]⇧-⇧u]t & [R]tv'›
        moreover AOT_have ‹[F]t & t ≠⇩E u›
          apply (rule "β→C"(1)[where κ⇩1κ⇩n="AOT_term_of_var (Ordinary.Rep t)"])
          apply (rule Π_minus_κE)
          by (fact 0[THEN "&E"(1)])
        ultimately AOT_show ‹t =⇩E u'›
          using u'_prop[THEN "&E"(2), THEN "Ordinary.∀E", THEN "→E", OF "&I"]
                "&E" by blast
      qed
    qed
    AOT_hence ‹∃R R |: [F]⇧-⇧u ⇩1⇩-⇩1⟷⇩E [G]⇧-⇧v›
      by (rule "∃I")
  } note 1 = this
  moreover {
    AOT_assume not_Ruv: ‹¬[R]uv›
    AOT_have ‹∃!v ([G]v & [R]uv)›
      using A[THEN "Ordinary.∀E", THEN "→E", OF fu].
    then AOT_obtain b where
      b_prop: ‹O!b & ([G]b & [R]ub & ∀t([G]t & [R]ut → t =⇩E b))›
      using "equi:1"[THEN "≡E"(1)] "∃E"[rotated] by fastforce
    AOT_hence ob: ‹O!b› and gb: ‹[G]b› and Rub: ‹[R]ub›
      using "&E" by blast+
    AOT_have ‹O!t → ([G]t & [R]ut → t =⇩E b)› for t
      using b_prop "&E"(2) "∀E"(2) by blast
    AOT_hence b_unique: ‹t =⇩E b› if ‹O!t› and ‹[G]t› and ‹[R]ut› for t
      by (metis Adjunction "modus-tollens:1" "reductio-aa:1" that)
    AOT_have not_v_eq_b: ‹¬(v =⇩E b)›
    proof(rule "raa-cor:2")
      AOT_assume ‹v =⇩E b›
      AOT_hence 0: ‹v = b›
        by (metis "=E-simple:2" "→E")
      AOT_have ‹[R]uv›
        using b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)]
              "rule=E"[rotated, OF 0[symmetric]] by fast
      AOT_thus ‹[R]uv & ¬[R]uv›
        using not_Ruv "&I" by blast
    qed
    AOT_have not_b_eq_v: ‹¬(b =⇩E v)›
      using "modus-tollens:1" not_v_eq_b "ord=Eequiv:2" by blast
    AOT_have ‹∃!u ([F]u & [R]uv)›
      using B[THEN "Ordinary.∀E", THEN "→E", OF gv].
    then AOT_obtain a where
      a_prop: ‹O!a & ([F]a & [R]av & ∀t([F]t & [R]tv → t =⇩E a))›
      using "equi:1"[THEN "≡E"(1)] "∃E"[rotated] by fastforce
    AOT_hence Oa: ‹O!a› and fa: ‹[F]a› and Rav: ‹[R]av›
      using "&E" by blast+
    AOT_have ‹O!t → ([F]t & [R]tv → t =⇩E a)› for t
      using a_prop "&E" "∀E"(2) by blast
    AOT_hence a_unique: ‹t =⇩E a› if ‹O!t› and ‹[F]t› and ‹[R]tv› for t
      by (metis Adjunction "modus-tollens:1" "reductio-aa:1" that) 
    AOT_have not_u_eq_a: ‹¬(u =⇩E a)›
    proof(rule "raa-cor:2")
      AOT_assume ‹u =⇩E a›
      AOT_hence 0: ‹u = a›
        by (metis "=E-simple:2" "→E")
      AOT_have ‹[R]uv›
        using a_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)]
              "rule=E"[rotated, OF 0[symmetric]] by fast
      AOT_thus ‹[R]uv & ¬[R]uv›
        using not_Ruv "&I" by blast
    qed
    AOT_have not_a_eq_u: ‹¬(a =⇩E u)›
      using "modus-tollens:1" not_u_eq_a "ord=Eequiv:2" by blast
    let ?R = ‹«[λu'v' (u' ≠⇩E u & v' ≠⇩E v & [R]u'v') ∨
                      (u' =⇩E a & v' =⇩E b) ∨
                      (u' =⇩E u & v' =⇩E v)]»›
    AOT_have ‹[«?R»]↓› by "cqt:2[lambda]"
    AOT_hence ‹∃ β β = [«?R»]›
      using "free-thms:1" "≡E"(1) by fast
    then AOT_obtain R⇩1 where R⇩1_def: ‹R⇩1 = [«?R»]›
      using "∃E"[rotated] by blast
    AOT_have Rxy1: ‹[R]xy› if ‹[R⇩1]xy› and ‹x ≠⇩E u› and ‹x ≠⇩E a› for x y
    proof -
      AOT_have 0: ‹[«?R»]xy›
        by (rule "rule=E"[rotated, OF R⇩1_def]) (fact that(1))
      AOT_have ‹(x ≠⇩E u & y ≠⇩E v & [R]xy) ∨ (x =⇩E a & y =⇩E b) ∨ (x =⇩E u & y =⇩E v)›
        using "β→C"(1)[OF 0] by simp
      AOT_hence ‹x ≠⇩E u & y ≠⇩E v & [R]xy› using that(2,3)
        by (metis "∨E"(3) "Conjunction Simplification"(1) "≡E"(1)
                  "modus-tollens:1" "thm-neg=E")
      AOT_thus ‹[R]xy› using "&E" by blast+
    qed
    AOT_have Rxy2: ‹[R]xy›  if ‹[R⇩1]xy› and ‹y ≠⇩E v› and ‹y ≠⇩E b› for x y
    proof -
      AOT_have 0: ‹[«?R»]xy›
        by (rule "rule=E"[rotated, OF R⇩1_def]) (fact that(1))
      AOT_have ‹(x ≠⇩E u & y ≠⇩E v & [R]xy) ∨ (x =⇩E a & y =⇩E b) ∨ (x =⇩E u & y =⇩E v)›
        using "β→C"(1)[OF 0] by simp
      AOT_hence ‹x ≠⇩E u & y ≠⇩E v & [R]xy›
        using that(2,3)
        by (metis "∨E"(3) "Conjunction Simplification"(2) "≡E"(1)
                  "modus-tollens:1" "thm-neg=E")
      AOT_thus ‹[R]xy› using "&E" by blast+
    qed
    AOT_have R⇩1xy: ‹[R⇩1]xy› if ‹[R]xy› and ‹x ≠⇩E u› and ‹y ≠⇩E v› for x y
      by (rule "rule=E"[rotated, OF R⇩1_def[symmetric]])
         (auto intro!: "β←C"(1) "cqt:2"
                 simp: "&I" "ex:1:a" prod_denotesI "rule-ui:3" that "∨I"(1))
    AOT_have R⇩1ab: ‹[R⇩1]ab›
      apply (rule "rule=E"[rotated, OF R⇩1_def[symmetric]])
      apply (safe intro!: "β←C"(1) "cqt:2" prod_denotesI "&I")
      by (meson a_prop b_prop "&I" "&E"(1) "∨I"(1) "∨I"(2) "ord=Eequiv:1" "→E")
    AOT_have R⇩1uv: ‹[R⇩1]uv›
      apply (rule "rule=E"[rotated, OF R⇩1_def[symmetric]])
      apply (safe intro!: "β←C"(1) "cqt:2" prod_denotesI "&I")
      by (meson "&I" "∨I"(2) "ord=Eequiv:1" Ordinary.ψ "→E")
    moreover AOT_have ‹R⇩1 |: F ⇩1⇩-⇩1⟷⇩E G›
    proof (safe intro!: "equi:2"[THEN "≡⇩d⇩fI"] "&I" "cqt:2" Ordinary.GEN "→I")
      fix u'
      AOT_assume fu': ‹[F]u'›
      {
        AOT_assume not_u'_eq_u: ‹¬(u' =⇩E u)› and not_u'_eq_a: ‹¬(u' =⇩E a)›
        AOT_hence u'_noteq_u: ‹u' ≠⇩E u› and u'_noteq_a: ‹u' ≠⇩E a›
          by (metis "≡E"(2) "thm-neg=E")+
        AOT_have ‹∃!v ([G]v & [R]u'v)›
          using A[THEN "Ordinary.∀E", THEN "→E", OF fu'].
        AOT_hence ‹∃v ([G]v & [R]u'v & ∀t ([G]t & [R]u't → t =⇩E v))›
          using "equi:1"[THEN "≡E"(1)] by simp
        then AOT_obtain v' where
          v'_prop: ‹[G]v' & [R]u'v' & ∀t ([G]t & [R]u't → t =⇩E v')›
          using "Ordinary.∃E"[rotated] by meson
        AOT_hence gv': ‹[G]v'› and Ru'v': ‹[R]u'v'›
          using "&E" by blast+
        AOT_have not_v'_eq_v: ‹¬v' =⇩E v›
        proof (rule "raa-cor:2")
          AOT_assume ‹v' =⇩E v›
          AOT_hence ‹v' = v›
            by (metis "=E-simple:2" "→E")
          AOT_hence Ru'v: ‹[R]u'v›
            using "rule=E" Ru'v' by fast
          AOT_have ‹u' =⇩E a›
            using a_unique[OF Ordinary.ψ, OF fu', OF Ru'v].
          AOT_thus ‹u' =⇩E a & ¬u' =⇩E a›
            using not_u'_eq_a "&I" by blast
        qed
        AOT_hence v'_noteq_v: ‹v' ≠⇩E v›
          using "≡E"(2) "thm-neg=E" by blast
        AOT_have ‹∀t ([G]t & [R]u't → t =⇩E v')›
          using v'_prop "&E" by blast
        AOT_hence ‹[G]t & [R]u't → t =⇩E v'› for t
          using "Ordinary.∀E" by meson
        AOT_hence v'_unique: ‹t =⇩E v'› if ‹[G]t› and ‹[R]u't› for t
          by (metis "&I" that "→E")

        AOT_have ‹[G]v' & [R⇩1]u'v' & ∀t ([G]t & [R⇩1]u't → t =⇩E v')›
        proof (safe intro!: "&I" gv' R⇩1xy Ru'v' u'_noteq_u u'_noteq_a "→I"
                            Ordinary.GEN "thm-neg=E"[THEN "≡E"(2)] not_v'_eq_v)
          fix t
          AOT_assume 1: ‹[G]t & [R⇩1]u't›
          AOT_have ‹[R]u't›
            using Rxy1[OF 1[THEN "&E"(2)], OF u'_noteq_u, OF u'_noteq_a].
          AOT_thus ‹t =⇩E v'›
            using v'_unique 1[THEN "&E"(1)] by blast
        qed
        AOT_hence ‹∃v ([G]v & [R⇩1]u'v & ∀t ([G]t & [R⇩1]u't → t =⇩E v))›
          by (rule "Ordinary.∃I")
        AOT_hence ‹∃!v ([G]v & [R⇩1]u'v)›
          by (rule "equi:1"[THEN "≡E"(2)])
      }
      moreover {
        AOT_assume 0: ‹u' =⇩E u›
        AOT_hence u'_eq_u: ‹u' = u›
          using "=E-simple:2" "→E" by blast
        AOT_have ‹∃!v ([G]v & [R⇩1]u'v)›
        proof (safe intro!: "equi:1"[THEN "≡E"(2)] "Ordinary.∃I"[where β=v]
                            "&I" Ordinary.GEN "→I" gv)
          AOT_show ‹[R⇩1]u'v›
            apply (rule "rule=E"[rotated, OF R⇩1_def[symmetric]])
            apply (safe intro!: "β←C"(1) "cqt:2" "&I" prod_denotesI)
            by (safe intro!: "∨I"(2) "&I" 0 "ord=Eequiv:1"[THEN "→E", OF Ordinary.ψ])
        next
          fix v'
          AOT_assume ‹[G]v' & [R⇩1]u'v'›
          AOT_hence 0: ‹[R⇩1]uv'›
            using "rule=E"[rotated, OF u'_eq_u] "&E"(2) by fast
          AOT_have 1: ‹[«?R»]uv'›
            by (rule "rule=E"[rotated, OF R⇩1_def]) (fact 0)
          AOT_have 2: ‹(u ≠⇩E u & v' ≠⇩E v & [R]uv') ∨
                       (u =⇩E a & v' =⇩E b) ∨
                       (u =⇩E u & v' =⇩E v)›
            using "β→C"(1)[OF 1] by simp
          AOT_have ‹¬u ≠⇩E u›
            using "≡E"(4) "modus-tollens:1" "ord=Eequiv:1" Ordinary.ψ
                  "reductio-aa:2" "thm-neg=E" by blast
          AOT_hence ‹¬((u ≠⇩E u & v' ≠⇩E v & [R]uv') ∨ (u =⇩E a & v' =⇩E b))›
            using not_u_eq_a
            by (metis "∨E"(2) "Conjunction Simplification"(1)
                      "modus-tollens:1" "reductio-aa:1")
          AOT_hence ‹(u =⇩E u & v' =⇩E v)›
            using 2 by (metis "∨E"(2))
          AOT_thus ‹v' =⇩E v›
            using "&E" by blast
        qed
      }
      moreover {
        AOT_assume 0: ‹u' =⇩E a›
        AOT_hence u'_eq_a: ‹u' = a›
          using "=E-simple:2" "→E" by blast
        AOT_have ‹∃!v ([G]v & [R⇩1]u'v)›
        proof (safe intro!: "equi:1"[THEN "≡E"(2)] "∃I"(2)[where β=b] "&I"
                            Ordinary.GEN "→I" b_prop[THEN "&E"(1)]
                            b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(1)])
          AOT_show ‹[R⇩1]u'b›
            apply (rule "rule=E"[rotated, OF R⇩1_def[symmetric]])
            apply (safe intro!: "β←C"(1) "cqt:2" "&I" prod_denotesI)
            apply (rule "∨I"(1); rule "∨I"(2); rule "&I")
             apply (fact 0)
            using b_prop "&E"(1) "ord=Eequiv:1" "→E" by blast
        next
          fix v'
          AOT_assume gv'_R1u'v': ‹[G]v' & [R⇩1]u'v'›
          AOT_hence 0: ‹[R⇩1]av'›
            using u'_eq_a by (meson "rule=E" "&E"(2))
          AOT_have 1: ‹[«?R»]av'›
            by (rule "rule=E"[rotated, OF R⇩1_def]) (fact 0)
          AOT_have ‹(a ≠⇩E u & v' ≠⇩E v & [R]av') ∨
                    (a =⇩E a & v' =⇩E b) ∨
                    (a =⇩E u & v' =⇩E v)›
            using "β→C"(1)[OF 1] by simp
          moreover {
            AOT_assume 0: ‹a ≠⇩E u & v' ≠⇩E v & [R]av'›
            AOT_have ‹∃!v ([G]v & [R]u'v)›
              using A[THEN "Ordinary.∀E", THEN "→E", OF fu'].
            AOT_hence ‹∃!v ([G]v & [R]av)›
              using u'_eq_a "rule=E" by fast
            AOT_hence ‹∃v ([G]v & [R]av & ∀t ([G]t & [R]at → t =⇩E v))›
              using "equi:1"[THEN "≡E"(1)] by fast
            then AOT_obtain s where
              s_prop: ‹[G]s & [R]as & ∀t ([G]t & [R]at → t =⇩E s)›
              using "Ordinary.∃E"[rotated] by meson
            AOT_have ‹v' =⇩E s›
              using s_prop[THEN "&E"(2), THEN "Ordinary.∀E"]
                    gv'_R1u'v'[THEN "&E"(1)] 0[THEN "&E"(2)]
              by (metis "&I" "vdash-properties:10")
            moreover AOT_have ‹v =⇩E s›
              using s_prop[THEN "&E"(2), THEN "Ordinary.∀E"] gv Rav
              by (metis "&I" "→E")
            ultimately AOT_have ‹v' =⇩E v›
              by (metis "&I" "ord=Eequiv:2" "ord=Eequiv:3" "→E")
            moreover AOT_have ‹¬(v' =⇩E v)›
              using 0<