# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656131417 -32400
# Node ID 4f48fe1b884a33c8b29d7feb9b003b26db4d0d82
# Parent  18e45e419a6886f43dc019367e5f7c2addc1aee9
...

diff -r 18e45e419a68 -r 4f48fe1b884a src/ordinal.agda
--- a/src/ordinal.agda	Fri Jun 24 13:29:11 2022 +0900
+++ b/src/ordinal.agda	Sat Jun 25 13:30:17 2022 +0900
@@ -1,13 +1,13 @@
-open import Level
+open import Level 
 module ordinal where
 
 open import logic
 open import nat
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ; _⊔_ to _n⊔_ ) 
 open import Data.Empty
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Definitions
-open import Data.Nat.Properties 
+open import Data.Nat.Properties as NP
 open import Relation.Nullary
 open import Relation.Binary.Core
 
@@ -16,30 +16,30 @@
 -- Countable Ordinals
 --
 
-data OrdinalD {n : Level} :  (lv : Nat) → Set n where
-   Φ : (lv : Nat) → OrdinalD  lv
-   OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
+data OrdinalD {n : Level} :  (lv : ℕ) → Set n where
+   Φ : (lv : ℕ) → OrdinalD  lv
+   OSuc : (lv : ℕ) → OrdinalD {n} lv → OrdinalD lv
 
 record Ordinal {n : Level} : Set n where
    constructor ordinal  
    field
-     lv : Nat
+     lv : ℕ
      ord : OrdinalD {n} lv
 
-data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
-   Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
-   s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
+data _d<_ {n : Level} :   {lx ly : ℕ} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
+   Φ<  : {lx : ℕ} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
+   s<  : {lx : ℕ} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
 
 open Ordinal
 
 _o<_ : {n : Level} ( x y : Ordinal ) → Set n
 _o<_ x y =  (lv x < lv y )  ∨ ( ord x d< ord y )
 
-s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x
+s<refl : {n : Level } {lx : ℕ } { x : OrdinalD {n} lx } → x d< OSuc lx x
 s<refl {n} {lv} {Φ lv}  = Φ<
 s<refl {n} {lv} {OSuc lv x}  = s< s<refl 
 
-trio<> : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
+trio<> : {n : Level} →  {lx : ℕ} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
 trio<>  {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t
 trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< ()
 
@@ -56,16 +56,16 @@
       lv x  ≡ lv y → ord x ≅ ord y →  x ≡ y
 ordinal-cong refl refl = refl
 
-≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
+≡→¬d< : {n : Level} →  {lv : ℕ} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
 ≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t
 
-trio<≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → x d< y → ⊥
+trio<≡ : {n : Level} →  {lx : ℕ} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → x d< y → ⊥
 trio<≡ refl = ≡→¬d<
 
-trio>≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → y d< x → ⊥
+trio>≡ : {n : Level} →  {lx : ℕ} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → y d< x → ⊥
 trio>≡ refl = ≡→¬d<
 
-triOrdd : {n : Level} →  {lx : Nat}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
+triOrdd : {n : Level} →  {lx : ℕ}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
 triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
 triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
 triOrdd  {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
@@ -97,7 +97,7 @@
 o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< y<x)) (case2 (s< x<y)) = 
    o<> (case2 y<x) (case2 x<y)
 
-orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
+orddtrans : {n : Level} {lx : ℕ} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
 orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< 
 orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )
 
@@ -163,11 +163,11 @@
 open _∧_
 
 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
-  → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx)  → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
-  → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x)  → ψ y )   → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
+  → ( ∀ (lx : ℕ ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx)  → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
+  → ( ∀ (lx : ℕ ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x)  → ψ y )   → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
   →  ∀ (x : Ordinal)  → ψ x
 TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where
-  TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox  → ψ x ) )
+  TransFinite1 : (lx : ℕ) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox  → ψ x ) )
   TransFinite1 Zero (Φ 0) = ⟪  caseΦ Zero lemma , lemma1 ⟫ where
       lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
       lemma x (case1 ())
@@ -176,9 +176,9 @@
       lemma1 x (case1 ())
       lemma1 x (case2 ())
   TransFinite1 (Suc lx) (Φ (Suc lx)) = ⟪ caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) , (λ x → lemma (lv x) (ord x)) ⟫ where
-      lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal lx (Φ lx) → ψ (ordinal ly oy)
+      lemma0 : (ly : ℕ) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal lx (Φ lx) → ψ (ordinal ly oy)
       lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt
-      lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy)
+      lemma : (ly : ℕ) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy)
       lemma lx1 ox1            (case1 lt) with <-∨ lt
       lemma lx (Φ lx)          (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) )
       lemma lx (Φ lx)          (case1 lt) | case2 lt1 = lemma0  lx (Φ lx) (case1 lt1)
@@ -200,17 +200,34 @@
       lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) 
       lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
 
-open import Data.Nat.Properties as DP
 OrdIrr : {n : Level } {x y : Ordinal {suc n} } {lt lt1 : x o< y} → lt ≡ lt1
-OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (DP.<-irrelevant _ _ )
+OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (NP.<-irrelevant _ _ )
 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case2 x₁} = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x )
 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case2 x} {case1 x₁} = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ )
 OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} {case2 Φ<} {case2 Φ<} = refl
 OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} {case2 (s< x)} {case2 (s< x₁)} = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where
-      lemma1 : {lx : Nat} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y
+      lemma1 : {lx : ℕ} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y
       lemma1 {lx} .(Φ lx) .(OSuc lx _) Φ< Φ< = refl
       lemma1 {lx} (OSuc lx a) (OSuc lx b) (s< x) (s< y) = cong s< (lemma1 {lx} a b x y )
+
+TransFinite3 : {n m : Level} { ψ : Ordinal {suc n} → Set m }
+          → ( (x : Ordinal {suc n})  → ( (y : Ordinal {suc n}  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : Ordinal {suc n} )  → ψ x
+TransFinite3 {n} {m} {ψ} ind x = TransFinite {n} {m} {ψ} caseΦ caseOSuc x where
+        caseΦ : (lx : ℕ) → ((x₁ : Ordinal {suc n}) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
+            ψ (record { lv = lx ; ord = Φ lx })
+        caseΦ lx prev = ind (ordinal lx (Φ lx) ) prev
+        caseOSuc :  (lx : ℕ) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
+            ψ (record { lv = lx ; ord = OSuc lx x₁ })
+        caseOSuc lx ox prev = ind (ordinal lx (OSuc lx ox)) prev 
+
+TP : {n m l : Level} → {Q : Ordinal {suc n} → Set m} {P : { x y : Ordinal {suc n} } → Q x → Q y → Set l}  
+    → ( ind : (x : Ordinal {suc n})  → ( (y : Ordinal  {suc n} ) → y o< x → Q y ) → Q x )                                                                 
+    → ( (x : Ordinal {suc n} )  → ( prev : (y : Ordinal {suc n} ) → y o< x → Q y ) → {y : Ordinal {suc n}} → (y<x : y o< x)  → P (prev y y<x) (ind x prev)  )  
+    →  {x z : Ordinal {suc n} } → (z≤x : z o< osuc x ) → P (TransFinite3 {n} {m} { λ x → Q x } ind z  )  (TransFinite3 {n} {m} { λ x → Q x } ind x  )
+TP {n} {m} {l} {Q} {P} ind indP {x} {z} z≤x = ?
  
+
 open import Ordinals 
 
 C-Ordinal : {n : Level} →  Ordinals {suc n} 
@@ -250,7 +267,7 @@
          lemma2 (ordinal Zero (OSuc 0 dx)) (case2 (s< x)) (case1 (s≤s z≤n)) not = not _ refl
          lemma2 (ordinal (Suc lx) (OSuc (Suc lx) ox)) y<x (case1 (s≤s (s≤s lt))) not = not _ refl
          lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where
-             lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
+             lemma3 : {n l : ℕ} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
              lemma3   (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n
      open Oprev
      Oprev-p  : (x : Ordinal) → Dec ( Oprev (Ordinal {suc n})  osuc x )
@@ -263,13 +280,13 @@
      TransFinite2 : { ψ : ord1  → Set (suc (suc n)) }
           → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord1)  → ψ x
-     TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
-        caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
+     TransFinite2 {ψ} ind x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
+        caseΦ : (lx : ℕ) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
             ψ (record { lv = lx ; ord = Φ lx })
-        caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
-        caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
+        caseΦ lx prev = ind (ordinal lx (Φ lx) ) prev
+        caseOSuc :  (lx : ℕ) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
             ψ (record { lv = lx ; ord = OSuc lx x₁ })
-        caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
+        caseOSuc lx ox prev = ind (ordinal lx (OSuc lx ox)) prev 
 
 
 -- H-Ordinal : {n : Level} → Ordinals {suc n} →  Ordinals {suc n}  →  Ordinals {suc n} 
diff -r 18e45e419a68 -r 4f48fe1b884a src/zorn.agda
--- a/src/zorn.agda	Fri Jun 24 13:29:11 2022 +0900
+++ b/src/zorn.agda	Sat Jun 25 13:30:17 2022 +0900
@@ -241,6 +241,7 @@
    field
       chain⊆A : chain ⊆' A
       chain∋x : odef chain x
+      mono : {y : Ordinal} → y o≤ z →  supf y ⊆' supf z 
       initial : {y : Ordinal } → odef chain y → * x ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
@@ -392,7 +393,7 @@
      ys {y} ay f mf = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = {!!} }
      init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x
      init-chain {y} {x} ay f mf x≤y = record { chain⊆A = λ fx →  A∋fc y f mf fx
-                     ; f-next = λ {x} sx → fsuc x sx  ; supf = λ _ → ys ay f mf 
+                     ; f-next = λ {x} sx → fsuc x sx  ; supf = λ _ → ys ay f mf  ; mono = ? 
                      ; initial = {!!} ; chain∋x  = init ay ; is-max = is-max } where
                i-total : IsTotalOrderSet (ys ay f mf )
                i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb)
@@ -469,7 +470,7 @@
                             * a < * b → odef (ZChain.chain zc) b ) → ZChain A y f x
           no-extenion is-max = record { supf = supf0 ;  chain⊆A = subst (λ k → k ⊆' A ) seq (ZChain.chain⊆A zc)
                      ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) seq (ZChain.initial zc)
-                     ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) seq (ZChain.f-next zc) 
+                     ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) seq (ZChain.f-next zc)  ; mono = ? 
                      ; chain∋x  = subst (λ k → odef k y ) seq (ZChain.chain∋x  zc)
                              ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
                                  HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) seq is-max } where
@@ -509,7 +510,7 @@
                 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  chain⊆A = {!!} ; f-next = {!!} 
+                record {  chain⊆A = {!!} ; f-next = {!!}  ; mono = ?
                      ; initial = {!!} ; chain∋x  = {!!} ; is-max = {!!}   ; supf = supf0 } where
                 sup0 : SUP A (ZChain.chain zc) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
@@ -623,7 +624,7 @@
      ... | no ¬ox with trio< x y
      ... | tri< a ¬b ¬c = init-chain ay f mf {!!}
      ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!}
-     ... | tri> ¬a ¬b y<x = record { supf = supf0 ; chain⊆A = {!!} ; f-next = {!!} 
+     ... | tri> ¬a ¬b y<x = record { supf = supf0 ; chain⊆A = {!!} ; f-next = {!!} ; mono = ?
                      ; initial = {!!} ; chain∋x  = {!!} ; is-max = {!!} }   where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
             field
@@ -668,7 +669,7 @@
              um00 : odef  (ZChain.supf (prev z a ) z) i → odef  (ZChain.supf (prev w a₁ ) w) i 
              um00 = {!!}
              um01 : odef  (ZChain.supf (prev z a ) z) i → odef  (ZChain.supf (prev z {!!} ) w) i 
-             um01 = {!!} -- ZChain.chain-mono (prev z a ay) {!!} {!!}
+             um01 = ? -- ZChain.mono (prev z a ) ?  ?
          ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = λ lt → record { u = z ; u<x = a ; chain∋z = lt }
          ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim ( osuc-< w≤x c )
          ... | tri≈ ¬a z=x ¬c | tri< w<x ¬b ¬c₁ = ⊥-elim ( osuc-< z≤w (subst (λ k → w o< k ) (sym z=x) w<x ) )
@@ -706,12 +707,12 @@
          ... | tri≈ ¬a b ¬c = {!!}
          ... | tri> ¬a ¬b y<x = {!!}
 
-     T⊆ : { ψ : Ordinal  → HOD }
-          → ( (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → {z : Ordinal} → z o≤ y  → ψ z ⊆' ψ y ) → {z : Ordinal} → z o≤ x  → ψ z ⊆' ψ x ) 
-          →  ∀ (x : Ordinal)  → {z : Ordinal} → z o≤ x  → ψ z ⊆' ψ x 
-     T⊆ {ψ} prev x {z} z≤x = TransFinite0 (λ x prev → indt x prev  ) x {z} z≤x where
-         indt : (x : Ordinal) → ( (y : Ordinal) → y o< x →  {z : Ordinal} → z o≤ y  → ψ z ⊆' ψ y ) →  {z : Ordinal} → z o≤ x  → ψ z ⊆' ψ x 
-         indt x prev {z} z≤x {i} zi = prev ? ? {z} z≤x zi
+     T⊆ : ( ind : (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → HOD ) → HOD ) 
+          → ( (x : Ordinal)  → ( prev : (y : Ordinal  ) → y o< x → HOD ) → {y : Ordinal } → (y<x : y o< x)  → prev y y<x ⊆' ind x prev  ) 
+          →  {x z : Ordinal} → z o≤ x  → TransFinite ind z ⊆' TransFinite ind x 
+     T⊆ = ? where -- {ψ} ind p⊆ {x} {z} z≤x = ? where -- TransFinite0 (λ x prev → indt x prev  ) x {z} z≤x where
+         -- indt : (x : Ordinal) → ( (y : Ordinal) → y o< x →  {z : Ordinal} → z o≤ y  → ψ z ⊆' ψ y ) →  {z : Ordinal} → z o≤ x  → ψ z ⊆' ψ x 
+         -- indt x prev {z} z≤x {i} zi = prev {!!} {!!} {z} z≤x zi
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM