# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658211290 -32400
# Node ID 3c3e3a1291bb11e578c091ec2950a03891343bb8
# Parent  5dacaf73eba85eed402d4d50d2d5335163eff288
...

diff -r 5dacaf73eba8 -r 3c3e3a1291bb src/zorn.agda
--- a/src/zorn.agda	Tue Jul 19 13:44:33 2022 +0900
+++ b/src/zorn.agda	Tue Jul 19 15:14:50 2022 +0900
@@ -475,8 +475,8 @@
                  px<x : px o< x
                  px<x = subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc
                  m01 : odef (UnionCF A f mf ay (ZChain.supf zc) x) b
-                 m01 with trio< b px 
-                 ... | tri> ¬a ¬b c = ⊥-eim ()
+                 m01 with trio< b px    --- px  < b < x
+                 ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫)
                  ... | tri< b<px ¬b ¬c = chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl m04 where
                     m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a
                     m03 = ?