--- a/OD.agda	Fri Jul 03 22:54:45 2020 +0900
+++ b/OD.agda	Sat Jul 04 12:53:40 2020 +0900
@@ -315,15 +315,20 @@
         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 = lemma } where
-        lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 
-        lemma {o∅} iφ = proj1 next-limit
-        lemma (isuc {x} i) = lemma1 where -- proj2 next-limit ? ( lemma i )
-           lemma1 : od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅
-           lemma1 = {!!}
-
-
+    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
 
     _=h=_ : (x y : HOD) → Set n
     x =h= y  = od x == od y