--- a/OD.agda	Sun Jul 28 14:50:56 2019 +0900
+++ b/OD.agda	Mon Jul 29 08:41:16 2019 +0900
@@ -500,14 +500,6 @@
          choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
          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 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 
          --
@@ -566,3 +558,19 @@
                                lx ≡ ly → ly ≡ lv (od→ord z)  → ψ z 
                           lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl)
 
+         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 = c
+           where
+             ψ :  (y : OD {suc n} ) →  Set (suc (suc n))
+             ψ y =  OD {suc n} 
+             lemma : ( x : OD {suc n} )  →  ({ y : OD {suc n} } →  x ∋ y → ψ y)   → ψ x
+             lemma x prev = lemma1 (od→ord X) <-osuc  where
+                 lemma1 : (ox : Ordinal {suc n}) → ox o< osuc (od→ord X)  → OD {suc n}
+                 lemma1 ox lt with ∋-p X (ord→od ox)
+                 lemma1 ox lt | yes p = ord→od ox
+                 lemma1 record { lv = Zero ; ord = (Φ .0) } lt | no ¬p = {!!}
+                 lemma1 record { lv = Zero ; ord = (OSuc .0 ord₁) } lt | no ¬p = lemma1 record { lv = Zero ; ord = ord₁ } {!!} 
+                 lemma1 record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } lt | no ¬p = {!!}
+                 lemma1 record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } lt | no ¬p = lemma1 record { lv = Suc lv₁ ; ord = ord₁ } {!!} 
+             c : OD {suc n}
+             c = ε-induction (λ {x} → lemma x) X