--- a/src/ODUtil.agda	Sat May 20 18:28:22 2023 +0900
+++ b/src/ODUtil.agda	Mon May 22 19:06:25 2023 +0900
@@ -75,11 +75,15 @@
    lemma {z} (case1 refl) = case1 refl
    lemma {z} (case2 refl) = case1 refl
 
-pair-<xy : {x y : HOD} → {n : Ordinal}  → & x o< next n →  & y o< next n  → & (x , y) o< next n
-pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
-... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho<
-... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho<
-... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho<
+-- pair-<xy : {x y : HOD} → {z : Ordinal}  → & x o< next z →  & y o< next z  → & (x , y) o< next z
+-- pair-<xy {x} {y} {z} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
+-- ... | tri< a ¬b ¬c | record { eq = eq1 } = ? where
+--     ll1 : omax (& x) (& y) o< next z
+--     ll1 = subst (λ k → k o< next z ) (sym eq1) (osuc<nx y<nn) 
+--     ll2 : & (x , y) o< next (omax (& x) (& y)) 
+--     ll2 = ho<
+-- ... | tri> ¬a ¬b c | record { eq = eq1 } = ? -- next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho<
+-- ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ? -- next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho<
 
 --  another form of infinite
 -- pair-ord< :  {x : Ordinal } → Set n
@@ -115,7 +119,7 @@
     ; proj2 = λ x⊆A lt → ⟪ x⊆A lt , lt ⟫
    }
 
-ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
+ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< infinite-odmax
 ω<next-o∅ {y} lt = <odmax infinite lt
 
 nat→ω : Nat → HOD