--- a/OD.agda	Fri Jul 03 21:58:01 2020 +0900
+++ b/OD.agda	Fri Jul 03 22:22:59 2020 +0900
@@ -311,8 +311,10 @@
     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
+        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 = ?
+
 
 
     _=h=_ : (x y : HOD) → Set n