--- a/ordinal-definable.agda	Tue May 21 18:17:24 2019 +0900
+++ b/ordinal-definable.agda	Wed May 22 11:52:49 2019 +0900
@@ -15,30 +15,8 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 
-
--- X' = { x ∈ X |  ψ  x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
-
 -- Ordinal Definable Set
 
--- o∋  : {n : Level} → {A : Ordinal {n}} → (OrdinalDefinable {n} A ) → (x : Ordinal {n} ) → (x o< A) → Set n
--- o∋ a x x<A  = def a x x<A
-
--- TC u : Transitive Closure of OD u
---
---    all elements of u or elements of elements of u, etc...
---
--- TC Zero = u
--- TC (suc n) = ∪ (TC n)
---
--- TC u = TC ω u = ∪ ( TC n ) n ∈ ω
--- 
---     u ∪ ( ∪ u ) ∪ ( ∪ (∪ u ) ) ....
---
--- Heritic Ordinal Definable
---
---    ( HOD = {x | TC x ⊆ OD } ) ⊆ OD     x ∈ OD here
--- 
-
 record OD {n : Level}  : Set (suc n) where
   field
     def : (x : Ordinal {n} ) → Set n
@@ -95,10 +73,11 @@
    ... | t with t (case2 Φ< )
    c3 lx (Φ .lx) d not | t | ()
    c3 lx (OSuc .lx x₁) d not with not (  record { lv = lx ; ord = OSuc lx x₁ } )
-   ... | t with t (case2 (s< {!!} ) )
---   x d< OSuc lx x is bad on ℵ case
+   ... | t with t (case2 (s< s<refl ) )
    c3 lx (OSuc .lx x₁) d not | t | ()
-   c3 .(Suc lv) (ℵ lv) not = {!!}
+   c3 (Suc lx) (ℵ lx) d not with not ( record { lv = Suc lx ; ord = OSuc (Suc lx) (Φ (Suc lx)) }  )
+   ... | t with t (case2 (s< (ℵΦ< {_} {_} {Φ (Suc lx)}))) 
+   c3 .(Suc lx) (ℵ lx) d not | t | ()
 
 ∅2 : {n : Level} →  od→ord ( od∅ {n} ) ≡ o∅ {n}
 ∅2 {n}  = {!!}