--- a/OD.agda	Sat Jul 04 12:53:40 2020 +0900
+++ b/OD.agda	Sat Jul 04 18:18:17 2020 +0900
@@ -132,6 +132,7 @@
    lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y
    lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt )
 
+
 _∋_ : ( a x : HOD  ) → Set n
 _∋_  a x  = odef a ( od→ord x )
 
@@ -240,6 +241,9 @@
     ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } 
    } 
 
+od⊆→o≤  : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
+od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))
+
 power< : {A x : HOD  } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x
 power< {A} {x} x⊆A = ⊆→o≤  (λ {y} x∋y → subst (λ k →  def (od A) k) diso (lemma y x∋y ) ) where
     lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y))
@@ -247,7 +251,7 @@
 
 open import Data.Unit
 
-ε-induction : { ψ : HOD  → Set (suc n)}
+ε-induction : { ψ : HOD  → Set n}
    → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
    → (x : HOD ) → ψ x
 ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
@@ -315,20 +319,24 @@
         isuc : {x : Ordinal  } →   infinite-d  x  →
                 infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
 
-    is-ω : (x : Ordinal) → Dec (infinite-d x )
-    is-ω x = {!!}
-
     infinite : HOD 
-    infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma1 } where
-        lemma : {y : Ordinal} → Lift (suc n) (infinite-d y → y o< next o∅ )
-        lemma {y} = TransFinite {λ x → Lift (suc n) (infinite-d x → x o<  next o∅) } ind y where
-           ind : (x : Ordinal) → ((z : Ordinal) → z o< x → Lift (suc n) (infinite-d z → z o< (next o∅)))  →
-                Lift (suc n) (infinite-d x → x o< (next  o∅))
-           ind x prev with {!!}
-           ... | ttt = {!!}
-        lemma1 : {y : Ordinal} → infinite-d y → y o< next o∅ 
-        lemma1 {y} with lemma {y}
-        lemma1 {y} | lift p = p
+    infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where
+        u : HOD → HOD
+        u x = Union (x , (x , x))
+        lemma1 : {x : HOD} → u x ⊆ Union (u x , (u x , u x))   
+        lemma1 {x} = record { incl = λ {y} lt → lemma2 y lt } where
+            lemma2 : (y : HOD) → u x ∋ y → ((z : Ordinal) → (z ≡ od→ord (u x)) ∨ (z ≡ od→ord (u x , u x)) ∧ def (od (ord→od z)) (od→ord y) → ⊥) → ⊥
+            lemma2 y lt not = not (od→ord (u x)) record { proj1 = case1 refl ; proj2 = subst (λ k → def (od k) (od→ord y) ) (sym oiso) lt }
+        lemma3 : {x : HOD} → od→ord (u x) o< osuc (od→ord ( Union (u x , (u x , u x))   ))
+        lemma3 {x} = od⊆→o≤ lemma1
+        lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 
+        lemma {y} = TransFinite {λ x → infinite-d x → x o<  next o∅ } ind y where
+           ind : (x : Ordinal) → ((z : Ordinal) → z o< x → infinite-d z → z o< (next o∅))  →
+                infinite-d x → x o< (next  o∅)
+           ind o∅  prev iφ = proj1 next-limit
+           ind x prev (isuc lt) = lemma0 where
+              lemma0 : {x : Ordinal} → od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅
+              lemma0 {x} = {!!}
 
     _=h=_ : (x y : HOD) → Set n
     x =h= y  = od x == od y