# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564411800 -32400
# Node ID 57be355d133687499edd66206456a016cd46dc89
# Parent  68eecbb011efb183b95b60de17fadd793024dfa3
ε-induction again

diff -r 68eecbb011ef -r 57be355d1336 OD.agda
--- a/OD.agda	Mon Jul 29 20:02:08 2019 +0900
+++ b/OD.agda	Mon Jul 29 23:50:00 2019 +0900
@@ -563,27 +563,17 @@
                 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 = lemma-ord (od→ord X) lemma-init 
-           where
+         choice-func' X ∋-p not = lemma-ord (od→ord X) (subst (λ k → <-not {X} k ) (sym diso) lemma-init )
+            where
             <-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 = {!!}
+            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)
             lemma-init y lt lt2 with osuc-≡< lt
             lemma-init y lt lt2 | case1 refl = o<¬≡ refl ( o<-subst (c<→o< {suc n} {_} {X} lt2) diso refl )
             lemma-init y lt lt2 | case2 lt1 = o<> lt1 ( o<-subst (c<→o< lt2) diso refl )
-            lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox → choiced X
-            lemma-ord  ox not = lemma1 (lv ox) (ord ox) not where
-                lemma1 : (lx : Nat) ( ox : OrdinalD lx ) → <-not {X} record {lv = lx ; ord = ox} → choiced X
-                lemma1 lx ox not with ∋-p X (ord→od record { lv = lx ; ord = ox})
-                ... | yes p = record { a-choice = ord→od record { lv = lx ; ord = ox} ; is-in = p }
-                lemma1 Zero (Φ 0) not | no ¬p = {!!}
-                lemma1 lx (OSuc lx ox) not | no ¬p = lemma1 lx ox {!!}
-                lemma1 (Suc lx) (Φ (Suc lx)) not | no ¬p = lemma1 lx (Φ lx) lemmaΦ where
-                    -- not : ( y : Ordinal {suc n}) →  (record { lv = Suc lx ; ord = Φ (Suc lx) }) o< osuc y → ¬ (X ∋ (ord→od y))
-                    -- we also have lemma1 lx any
-                    lemmaΦ : ( y : Ordinal {suc n}) → (record { lv = lx ; ord = Φ lx }) o< osuc y → ¬ (X ∋ (ord→od y))
-                    lemmaΦ y lt with trio<  (record { lv = Suc lx ; ord = Φ (Suc lx) }) (osuc y )
-                    lemmaΦ y lt | tri< a ¬b ¬c = not y a
-                    --  record { lv = lx ; ord = Φ lx }  o< osuc y o< record { lv = Suc lx ; ord = Φ (Suc lx) }
-                    lemmaΦ y lt | tri> ¬a ¬b c = {!!}
-