# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657899938 -32400
# Node ID 6c9fed204440cb83ebd4defdb0d3b0913a84e18c
# Parent  b0cad3ec7da08ea684ebab3fb02ff37a98eaed62
...

diff -r b0cad3ec7da0 -r 6c9fed204440 src/zorn.agda
--- a/src/zorn.agda	Fri Jul 15 21:39:32 2022 +0900
+++ b/src/zorn.agda	Sat Jul 16 00:45:38 2022 +0900
@@ -628,10 +628,6 @@
                       ... | tri≈ ¬a b ¬c = ? where
                           zc13 : odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) (HasPrev.y pr)
                           zc13 = HasPrev.ay pr 
-                          zc12 : ?
-                          zc12 with proj1 (mf _ (A∋fcs _ f mf fc ) ) | zc13  -- u is sup and has prev
-                          ... | case1 x | ⟪ apz , ach ⟫ = ?
-                          ... | case2 x | ⟪ apz , ach ⟫ = ?
                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
                 ... | tri≈ ¬a b=px ¬c = zc15 where
                        zc14 : f (HasPrev.y pr) ≡ b
@@ -666,7 +662,9 @@
                             HasPrev A pchain ab f ∨ IsSup A pchain   ab →
                             * a < * b → odef pchain b
                 z18 {a} {b} za b<x ab P a<b with trio< b px
-                ... | tri< lt ¬b ¬c = zcp za (chain-≡ ? ) lt ab P a<b 
+                ... | tri< lt ¬b ¬c = ? where
+                    z20 : odef pchain b
+                    z20 = chain-mono ( ZChain.is-max zc ? lt ab ? a<b )
                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
                 ... | tri≈ ¬a b=px ¬c with P
                 ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )