--- a/OPair.agda	Wed Jul 15 08:42:30 2020 +0900
+++ b/OPair.agda	Fri Jul 17 16:33:30 2020 +0900
@@ -143,11 +143,29 @@
     checkAB : { p : Ordinal } → def ZFProduct p → Set n
     checkAB (pair x y) = odef A x ∧ odef B y
     pmax : Ordinal
-    pmax = omax (odmax A)  (odmax B)
-    <pmax : {y : Ordinal} → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< omax (odmax A)  (odmax B)
-    <pmax {y} = TransFinite {λ y → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< omax (odmax A)  (odmax B)} ind y where
-        ind : (x : Ordinal)
-            → ((y₁ : Ordinal) → y₁ o< x → def ZFProduct y₁ ∧ ({x₁ : Ordinal} (p : def ZFProduct x₁) → checkAB p) → y₁ o< (omax (odmax A) (odmax B)))
-            → def ZFProduct x ∧ ({x₁ : Ordinal} (p : def ZFProduct x₁) → checkAB p) → x o< (omax (HOD.odmax A) (HOD.odmax B))
-        ind = {!!}
+    pmax =  next (omax (od→ord A)  (od→ord B))
+    <pmax : {y : Ordinal} → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< next (omax (od→ord A)  (od→ord B))
+    <pmax {y} prod = {!!} where
+         prod-odmax : ( x y : HOD) → Ordinal
+         prod-odmax x y = omax (od→ord (x , x)) (od→ord (x , y))
+         lemma : {x y z : HOD } → ((x , x ) , (x , y )) ∋ z → od→ord z o< osuc (osuc (od→ord (x , y) ))
+         lemma {x} {y} {z} = {!!}
+         lemma1 : {x y  : HOD } → A ∋ x → B ∋ y → od→ord (x , y) o< omax (odmax A) (odmax B)
+         lemma1 {x} {y} A∋x  B∋y with trio< (odmax A) (odmax B)
+         lemma1 {x} {y} A∋x B∋y | tri< a ¬b ¬c = begin
+                 od→ord (x , y)
+              ≤⟨ {!!} ⟩
+                 odmax B
+              ∎ where open o≤-Reasoning O
+         lemma1 {x} {y} A∋x B∋y | tri≈ ¬a b ¬c = {!!}
+         lemma1 {x} {y} A∋x B∋y | tri> ¬a ¬b c = {!!}
 
+--            lemma2 : od→ord (x , y) o< osuc (omax (odmax A) (odmax B))
+--            lemma2 = begin
+--                 {!!}
+--              ≤⟨ {!!} ⟩
+--                 {!!}
+--              ∎ where open o≤-Reasoning O
+         a = π1 (subst (λ k → def ZFProduct k) (sym diso) (proj1 prod))
+         b = π2 (subst (λ k → def ZFProduct k) (sym diso) (proj1 prod))
+