--- a/ordinal-definable.agda	Thu May 23 20:24:15 2019 +0900
+++ b/ordinal-definable.agda	Fri May 24 08:21:41 2019 +0900
@@ -73,7 +73,7 @@
    ... | t with t (case2 (s< s<refl ) )
    c3 lx (OSuc .lx x₁) d not | t | ()
    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)}))) 
+   ... | t with t (case2 (s< ℵΦ<   )) 
    c3 .(Suc lx) (ℵ lx) d not | t | ()
 
 -- find : {n : Level} → ( x : Ordinal {n} ) → o∅ o< x → Ordinal {n}  
@@ -90,16 +90,25 @@
    lemma0 :  def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) →  def z (od→ord x)
    lemma0 dz  = def-subst {n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso)
 
-ominimal : {n : Level} → (x : Ordinal {n} ) → o∅ o< x → Ordinal {n}
+record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where
+  field
+     mino : Ordinal {n}
+     min<x :  mino o< x
+  defmin : def ( ord→od x ) mino
+  defmin = lemma ( o<→c< min<x ) where
+     lemma : def (ord→od x) (od→ord ( ord→od mino))  → def ( ord→od x ) mino
+     lemma m< = def-subst {n} {ord→od x} m< refl diso
+
+ominimal : {n : Level} → (x : Ordinal {n} ) → o∅ o< x → Minimumo {n} x
 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case1 ())
 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case2 ())
 ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case1 ())
-ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case2 Φ<) = record { lv = Zero ; ord = Φ 0 }
-ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case1 (s≤s x)) = record { lv = lv ; ord = Φ lv }
+ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case2 Φ<) = record { mino = record { lv = Zero ; ord = Φ 0 } ; min<x = case2 Φ< }
+ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case1 (s≤s x)) = record { mino = record { lv = lv ; ord = Φ lv } ; min<x = case1 (s≤s ≤-refl)}
 ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case2 ())
-ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case1 (s≤s x)) = record { lv = (Suc lv) ; ord = ord }
+ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case1 (s≤s x)) = record { mino = record { lv = (Suc lv) ; ord = ord } ; min<x = case2 s<refl}
 ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case2 ())
-ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case1 (s≤s z≤n)) = record { lv = lv ; ord = Φ lv }
+ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case1 (s≤s z≤n)) = record { mino = record { lv = Suc lv ; ord = Φ (Suc lv) } ; min<x = case2 ℵΦ<  }
 ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case2 ())
 
 ∅4 : {n : Level} →  ( x : OD {n} )  →  x  ≡ od∅ {n}  → od→ord x ≡ o∅ {n}
@@ -205,6 +214,7 @@
        ;   replacement = {!!}
      } where
          open _∧_ 
+         open Minimumo
          pair : (A B : OD {n} ) → Lift (suc n) ((A , B) ∋ A) ∧ Lift (suc n) ((A , B) ∋ B)
          proj1 (pair A B ) = lift ( case1 refl )
          proj2 (pair A B ) = lift ( case2 refl )
@@ -214,10 +224,18 @@
          union→ X x y (lift X∋x) (lift x∋y) = lift {!!}  where
             lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y
             lemma {z} X∋z = {!!}
+         minord : (x : OD {n} ) → ¬ x ≡ od∅ → Minimumo (od→ord x)
+         minord x not = ominimal (od→ord x) (∅9 x not)
          minimul : (x : OD {n} ) → ¬ x ≡ od∅ → OD {n} 
-         minimul x  not = ord→od ( ominimal (od→ord x) (∅9 x not) )
+         minimul x  not = ord→od ( mino (minord x not))
+         minimul<x : (x : OD {n} ) →  (not :  ¬ x ≡ od∅ ) → x ∋ minimul x not
+         minimul<x x not = lemma0 where
+            lemma :  def x (mino (minord x not))
+            lemma = def-subst (defmin (minord x not)) oiso refl
+            lemma0 : def x (od→ord (ord→od (mino (minord x not))))
+            lemma0 = def-subst {n} {x} lemma refl {!!}
          regularity : (x : OD) → (not : ¬ x ≡ od∅ ) →
                 Lift (suc n) (x ∋ minimul x not ) ∧
                 (Select x (λ x₁ → Lift (suc n) ( minimul x not ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅)
-         proj1 ( regularity x non ) = {!!}
+         proj1 ( regularity x non ) = lift ( minimul<x x non )
          proj2 ( regularity x non ) = {!!}