--- a/OD.agda	Tue Jul 28 14:15:33 2020 +0900
+++ b/OD.agda	Tue Jul 28 17:48:28 2020 +0900
@@ -498,9 +498,17 @@
 -- postulate f-extensionality : { n m : Level}  → HE.Extensionality n m
 
 ω-prev-eq1 : {x y : Ordinal} →  od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → ¬ (x o< y)
-ω-prev-eq1 {x} {y} eq not with eq→ (ord→== eq) {od→ord (ord→od y , ord→od y)} (λ not2 → not2 (od→ord (ord→od y , ord→od y))
-      record { proj1 = case2 refl ; proj2 = subst (λ k → odef k (od→ord (ord→od y))) {!!} (case1 refl) } )
-... | t = {!!}
+ω-prev-eq1 {x} {y} eq x<y = eq→ (ord→== eq) {od→ord (ord→od y)} (λ not2 → not2 (od→ord (ord→od y , ord→od y))
+      record { proj1 = case2 refl ; proj2 = subst (λ k → odef k (od→ord (ord→od y))) (sym oiso) (case1 refl)} ) (λ u → lemma u ) where
+   lemma : (u : Ordinal) → ¬ def (od (ord→od x , (ord→od x , ord→od x))) u ∧ def (od (ord→od u)) (od→ord (ord→od y))
+   lemma u t with proj1 t
+   lemma u t | case1 u=x = o<> (c<→o< {ord→od y} {ord→od u} (proj2 t)) (subst₂ (λ j k → j o< k )
+        (trans (sym diso) (trans (sym u=x) (sym diso)) ) (sym diso) x<y ) -- x ≡ od→ord (ord→od u)
+   lemma u t | case2 u=xx = o<> x<y (subst (λ k → k o< x ) diso {!!} )
+         --  x <  y <  u = (x , x ) 
+          --(ordtrans {!!} (subst₂ (λ j k → j o< k ) {!!} {!!} (c<→o< {ord→od y} {ord→od u} (proj2 t))  ) )) where
+         -- lemma1 : od→ord (ord→od u) o< x
+         --  lemma1 = {!!}
 
 ω-prev-eq : {x y : Ordinal} →  od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → x ≡ y
 ω-prev-eq {x} {y} eq with trio< x y