--- a/OD.agda	Wed Jul 31 15:29:51 2019 +0900
+++ b/OD.agda	Wed Jul 31 17:17:24 2019 +0900
@@ -104,6 +104,9 @@
 otrans : {n : Level} {a x y : Ordinal {n} } → def (Ord a) x → def (Ord x) y → def (Ord a) y
 otrans x<a y<x = ordtrans y<x x<a
 
+def→o< : {n : Level } {X : OD {suc n}} → {x : Ordinal {suc n}} → def X x → x o< od→ord X 
+def→o< {n} {X} {x} lt = o<-subst {suc n} {_} {_} {x} {od→ord X} ( c<→o< ( def-subst {suc n} {X} {x}  lt (sym oiso) (sym diso) )) diso diso
+
 ∅3 : {n : Level} →  { x : Ordinal {suc n}}  → ( ∀(y : Ordinal {suc n}) → ¬ (y o< x ) ) → x ≡ o∅ {suc n}
 ∅3 {n} {x} = TransFinite {n} c2 c3 x where
    c0 : Nat →  Ordinal {suc n}  → Set (suc n)
@@ -561,12 +564,34 @@
                 a-choice : OD {suc n}
                 is-in : X ∋ a-choice
          choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → choiced X
-         choice-func' X ∋-p not = {!!} where
-            lemma-ord : ( lx : Nat ) (ox : OrdinalD lx ) → {ly : Nat} → {oy : OrdinalD ly }
-                → ordinal ly oy o< ordinal lx ox  → choiced X ∨ ( ¬ ( def X (ordinal ly oy) ))
-            lemma-ord lx (OSuc lx ox) y<x with ∋-p X (ord→od (ordinal lx (OSuc lx ox)))
-            lemma-ord lx (OSuc lx ox) y<x | yes p = case1 ( record { a-choice = (ord→od (ordinal lx (OSuc lx ox))) ; is-in = p } )
-            lemma-ord lx (OSuc lx ox) y<x | no ¬p with osuc-≡< y<x
-            lemma-ord lx (OSuc lx ox) y<x | no ¬p | case1 refl = {!!}
-            lemma-ord lx (OSuc lx ox) y<x | no ¬p | case2 t = lemma-ord lx ox t
-            lemma-ord (Suc lx) (Φ (Suc lx)) (case1 x) = {!!}
+         choice-func' X ∋-p not = lemma0 
+           where
+            <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n)
+            <-not {X} ox =  ( y : Ordinal {suc n}) → y o< ox → ¬ (X ∋ (ord→od y)) 
+            lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox ∨ choiced X
+            lemma-ord  ox = TransFinite {n} {suc (suc n)} {λ ox → <-not {X} ox ∨  choiced X  } caseΦ caseOSuc ox where
+               caseΦ : (lx : Nat) → ((x : Ordinal) → x o< ordinal lx (Φ lx) → <-not {X} x ∨ choiced X) →
+                    <-not {X} (record { lv = lx ; ord = Φ lx }) ∨ choiced X
+               caseΦ lx prev with ∋-p X ( ord→od (ordinal lx (Φ lx) ))
+               caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
+               caseΦ lx prev | no ¬p = {!!}
+               caseOSuc : (lx : Nat) (x : OrdinalD lx) → (<-not {X} (record { lv = lx ; ord = x }) ∨ choiced X) →
+                    <-not {X} (record { lv = lx ; ord = OSuc lx x }) ∨ choiced X
+               caseOSuc lx x prev with ∋-p X (ord→od record { lv = lx ; ord = x } )
+               caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
+               caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where
+                    lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X (od→ord (ord→od y)) → ⊥
+                    lemma y lt with trio< y (ordinal lx x )
+                    lemma y lt | tri< a ¬b ¬c = not_found y a
+                    lemma y lt | tri≈ ¬a refl ¬c = ¬p
+                    lemma y lt | tri> ¬a ¬b c with osuc-≡< lt
+                    lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
+                    lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
+               caseOSuc lx x (case2 found) | no ¬p = case2 found
+            lemma0 : choiced X
+            lemma0 with lemma-ord (od→ord X )
+            lemma0 | case1 not_found = ⊥-elim ( not ( record {
+                eq→ = λ {x} lt → ⊥-elim (not_found x (def→o< lt)  (def-subst {suc n} {_} {_} {X} {_} lt refl (sym diso ))) ;
+                eq← = λ lt → ⊥-elim (¬x<0 lt) } ) )
+            lemma0 | case2 found = found
+