--- a/src/OD.agda	Sat May 20 18:28:22 2023 +0900
+++ b/src/OD.agda	Mon May 22 19:06:25 2023 +0900
@@ -261,6 +261,8 @@
     lemma {t} (case1 refl) = omax-x  _ _
     lemma {t} (case2 refl) = omax-y  _ _
 
+-- {x y : HOD} → & (x , y) ≡ omax (& x) (& y) 
+
 pair<y : {x y : HOD } → y ∋ x  → & (x , x) o< osuc (& y)
 pair<y {x} {y} y∋x = ⊆→o≤ lemma where
    lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
@@ -460,28 +462,37 @@
 --
 --  Since we have Ord (next o∅), we don't need this, but ZF axiom requires this and ho<
 
+infinite-od : OD
+infinite-od = record { def = λ x → infinite-d x } 
+
+postulate 
+    infinite-odmax : Ordinal 
+    infinite-odmax< : {z : Ordinal } → def infinite-od z → z o< infinite-odmax
+
 infinite : HOD
-infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
-    u : (y : Ordinal ) → HOD
-    u y = Union (* y , (* y , * y))
-    --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
-    lemma8 : {y : Ordinal} → & (* y , * y) o< next (odmax (* y , * y))
-    lemma8 = ho<
-    ---           (x,y) < next (omax x y) < next (osuc y) = next y
-    lemmaa : {x y : HOD} → & x o< & y → & (x , y) o< next (& y)
-    lemmaa {x} {y} x<y = subst (λ k → & (x , y) o< k ) (sym nexto≡) (subst (λ k → & (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
-    lemma81 : {y : Ordinal} → & (* y , * y) o< next (& (* y))
-    lemma81 {y} = nexto=n (subst (λ k →  & (* y , * y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
-    lemma9 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y , * y))
-    lemma9 = lemmaa (c<→o< (case1 refl))
-    lemma71 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y))
-    lemma71 = next< lemma81 lemma9
-    lemma1 : {y : Ordinal} → & (u y) o< next (osuc (& (* y , (* y , * y))))
-    lemma1 = ho<
-    --- main recursion
-    lemma : {y : Ordinal} → infinite-d y → y o< next o∅
-    lemma {o∅} iφ = x<nx
-    lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1))
+infinite = record { od = record { def = λ x → infinite-d x } ; odmax = infinite-odmax ; <odmax = infinite-odmax< }  
+
+-- where
+--    u : (y : Ordinal ) → HOD
+--    u y = Union (* y , (* y , * y))
+--    --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
+--    lemma8 : {y : Ordinal} → & (* y , * y) o< next (odmax (* y , * y))
+--    lemma8 = ho<
+--    ---           (x,y) < next (omax x y) < next (osuc y) = next y
+--    lemmaa : {x y : HOD} → & x o< & y → & (x , y) o< next (& y)
+--    lemmaa {x} {y} x<y = subst (λ k → & (x , y) o< k ) (sym nexto≡) (subst (λ k → & (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
+--    lemma81 : {y : Ordinal} → & (* y , * y) o< next (& (* y))
+--    lemma81 {y} = nexto=n (subst (λ k →  & (* y , * y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
+--    lemma9 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y , * y))
+--    lemma9 = lemmaa (c<→o< (case1 refl))
+--    lemma71 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y))
+--    lemma71 = ? -- next< lemma81 lemma9
+--    lemma1 : {y : Ordinal} → & (u y) o< next (osuc (& (* y , (* y , * y))))
+--    lemma1 = ho<
+--    --- main recursion
+--    lemma : {y : Ordinal} → infinite-d y → y o< next o∅
+--    lemma {o∅} iφ = x<nx
+--    lemma (isuc {y} x) = ? -- next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1))
 
 empty : (x : HOD  ) → ¬  (od∅ ∋ x)
 empty x = ¬x<0