# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564293056 -32400
# Node ID 38ecc75d93ceb33b9ad762e79d9fe52e00a210a7
# Parent  9eb6a8691f02a466f0910533a5c749e87b15bf71
does not work

diff -r 9eb6a8691f02 -r 38ecc75d93ce OD.agda
--- a/OD.agda	Sun Jul 28 14:07:08 2019 +0900
+++ b/OD.agda	Sun Jul 28 14:50:56 2019 +0900
@@ -501,14 +501,12 @@
          choice X {A} X∋A not = x∋minimul A not
 
          choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → OD {suc n}
-         choice-func' X ∋-p not = lemma (lv (od→ord X )) (ord (od→ord X)) where
-             lemma : (lx : Nat ) ( ox : OrdinalD lx )  → OD {suc n}
-             lemma lx ox  with ∋-p X (ord→od record { lv = lx ; ord = ox })
-             lemma lx ox | yes p = (ord→od record { lv = lx ; ord = ox })
-             lemma Zero (Φ 0)  | no ¬p = od∅
-             lemma Zero (OSuc 0 ox)  | no ¬p = lemma  Zero ox 
-             lemma (Suc lx) (Φ (Suc lx))  | no ¬p = {!!}
-             lemma (Suc lx) (OSuc (Suc lx) ox)  | no ¬p = lemma ( Suc lx ) ox 
+         choice-func' X ∋-p not = lemma o∅  {!!} {!!} where
+             lemma : (ox : Ordinal {suc n} ) → ( ox o< osuc (od→ord X) ) → ((oy : Ordinal ) → oy o< ox → ¬ ( X ∋ ord→od oy ) )  → OD {suc n}
+             lemma ox lt l∅ with ∋-p X (ord→od ox)
+             lemma ox lt l∅ | yes p = ord→od ox
+             lemma ox (case1 x) l∅ | no ¬p = lemma (record { lv = Suc (lv ox); ord = Φ (Suc (lv ox))}) (case1 {!!}) {!!}
+             lemma ox (case2 x) l∅ | no ¬p = lemma (record { lv = lv ox; ord = OSuc (lv ox) (ord ox)}) {!!} {!!}
 
          --
          -- another form of regularity