--- a/generic-filter.agda	Sat Jul 25 17:36:27 2020 +0900
+++ b/generic-filter.agda	Sun Jul 26 21:10:37 2020 +0900
@@ -84,15 +84,27 @@
 
 HODω2 :  HOD
 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
-    ω<next : {y : Ordinal} → infinite-d y → y o< next o∅
-    ω<next = ω<next-o∅ ho<
-    lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x
-    lemma = {!!}
+    P  : (i j : Nat) (x : Ordinal ) → HOD
+    P  i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , ord→od x
+    nat0 : (i : Nat) → od→ord (nat→ω i) o< next o∅ 
+    nat0 i = <odmax infinite (ω∋nat→ω {i})
+    lemma3 : (i j : Nat) → od→ord ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) o< next o∅ 
+    lemma3 i j = pair-<xy (pair-<xy (nat0 i) (nat0 i) ) (pair-<xy (nat0 i) (nat0 j) )
+    lemma1 : (i j : Nat) (x : Ordinal ) → osuc (od→ord (P i j x)) o< next x
+    lemma1 i j x = osuc<nx ( next< lemma2 ho<  ) where
+       lemma2 :  odmax (((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , ord→od x) o< next x
+       lemma2 with trio<  (od→ord ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j))) (od→ord (ord→od x))
+           |   inspect (omax (od→ord ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)))) (od→ord (ord→od x))
+       lemma2 | tri< a ¬b ¬c | _ = osuc<nx (subst (λ k → k o< next x ) (sym diso) x<nx )
+       lemma2 | tri≈ ¬a b ¬c | record { eq = eq1 } = subst₂ (λ j k → j o< next k ) (trans (omax≡  _ _ b ) eq1 ) diso (osuc<nx x<nx)
+       lemma2 | tri> ¬a ¬b c | record { eq = eq1 } =  osuc<nx ( next< nexto∅ (lemma3 i j))
+    lemma : (i j : Nat) (x : Ordinal ) → od→ord (Union (P i j x)) o< next x
+    lemma i j x = next< (lemma1 i j x ) ho<
     odmax0 :  {y : Ordinal} → Hω2r y → y o< next o∅ 
     odmax0 {y} r with hω2 r
     ... | hφ = x<nx
-    ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x})
-    ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x})
+    ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma i 0 x)
+    ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma i 1 x)
     ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
 
 3→Hω2 : List (Maybe Two) → HOD