--- a/LEMC.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/LEMC.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -20,6 +20,13 @@
 open OD.OD
 open OD._==_
 open ODAxiom odAxiom
+import OrdUtil
+import ODUtil
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
 
 open import zfc
 
@@ -89,7 +96,7 @@
                  ψ : ( ox : Ordinal ) → Set n
                  ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ odef X x )) ∨ choiced (& X)
                  lemma-ord : ( ox : Ordinal  ) → ψ ox
-                 lemma-ord  ox = TransFinite {ψ} induction ox where
+                 lemma-ord  ox = TransFinite0 {ψ} induction ox where
                     ∀-imply-or :  {A : Ordinal  → Set n } {B : Set n }
                         → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
                     ∀-imply-or  {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM
@@ -107,13 +114,15 @@
                          lemma1 y with ∋-p X (* y)
                          lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } )
                          lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (d→∋ X y<X) )
-                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (& X)
+                         lemma :  ((y : Ordinal) → y o< x → odef X y → ⊥) ∨ choiced (& X)
                          lemma = ∀-imply-or lemma1
+                 odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< & X 
+                 odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {& X} ( c<→o< ( subst₂ (λ j k → odef j k )  (sym *iso) (sym &iso)  lt )) &iso &iso
                  have_to_find : choiced (& X)
                  have_to_find = dont-or  (lemma-ord (& X )) ¬¬X∋x where
                      ¬¬X∋x : ¬ ((x : Ordinal) → x o< (& X) → odef X x → ⊥)
                      ¬¬X∋x nn = not record {
-                            eq→ = λ {x} lt → ⊥-elim  (nn x (odef→o< lt) lt) 
+                            eq→ = λ {x} lt → ⊥-elim  (nn x (odef→o< lt)  lt) 
                           ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
                         }
 
@@ -154,7 +163,7 @@
               min2 : Minimal u
               min2 = prev (proj1 y1prop) u (proj2 y1prop)
          Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u 
-         Min2 x u u∋x = (ε-induction1 {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
+         Min2 x u u∋x = (ε-induction {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
          cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced (& x )
          cx {x} nx = choice-func x nx
          minimal : (x : HOD  ) → ¬ (x =h= od∅ ) → HOD