# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564416744 -32400
# Node ID a1a7caa8b30522eb8b332738b4422833b2b40f3b
# Parent  57be355d133687499edd66206456a016cd46dc89
...

diff -r 57be355d1336 -r a1a7caa8b305 OD.agda
--- a/OD.agda	Mon Jul 29 23:50:00 2019 +0900
+++ b/OD.agda	Tue Jul 30 01:12:24 2019 +0900
@@ -568,9 +568,15 @@
             <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n)
             <-not {X} ox =  ( y : Ordinal {suc n}) → ox o< osuc y → ¬ (X ∋ (ord→od y)) 
             ind : {x : OD} → ({y : OD} → x ∋ y → <-not {X} (od→ord y) → choiced X) → <-not {X} (od→ord x) → choiced X
-            ind {y} ψ nox with ∋-p X y
-            ind {y} ψ nox | yes p = record { a-choice = y ; is-in = p }
-            ind {y} ψ nox | no ¬p = {!!}
+            ind {x} ψ nox = lemma (od→ord x) nox where
+                 lemma : (ox : Ordinal {suc n}) → <-not {X} ox → choiced X
+                 lemma ox nox with ∋-p X (ord→od ox)
+                 ... | yes p = record { a-choice = ord→od ox ; is-in = p }
+                 lemma record { lv = Zero ; ord = (Φ 0) } nox | no ¬p = {!!}
+                 lemma record { lv = lx ; ord = (OSuc lx ox) } nox | no ¬p = lemma record { lv = lx ; ord = ox } {!!}
+                 lemma record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } nox | no ¬p = lemma  record { lv = lx ; ord = Φ lx } lemma2 where
+                      lemma2 : ( y : Ordinal {suc n}) → record { lv = lx ; ord = Φ lx } o< osuc y → ¬ (X ∋ (ord→od y))
+                      lemma2 y lt = {!!}
             lemma-ord : ( x : Ordinal {suc n} ) → (<-not {X} (od→ord (ord→od x))) → choiced X
             lemma-ord x = ε-induction {n} {suc (suc n)} { λ x → (<-not {X} (od→ord x)) → choiced X} ind (ord→od x)
             lemma-init : (y : Ordinal) → od→ord X o< osuc y → ¬ (X ∋ ord→od y)