--- a/OD.agda	Fri Jul 03 21:39:10 2020 +0900
+++ b/OD.agda	Fri Jul 03 21:58:01 2020 +0900
@@ -308,7 +308,12 @@
                 infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
 
     infinite : HOD 
-    infinite = record { od = record { def = λ x → infinite-d x } ; odmax = {!!} ; <odmax = {!!} }
+    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 {n} (isuc i) = {!!} where
+            lemma1 = proj2 next-limit
+
 
     _=h=_ : (x y : HOD) → Set n
     x =h= y  = od x == od y