# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665571860 -32400
# Node ID 0d8d230e4b2b2371f0b7bfd6a5b1d561afbb62e2
# Parent  d5293a7c2ec4da860f49e759b51229724d9a268f
this csupf is bad

diff -r d5293a7c2ec4 -r 0d8d230e4b2b src/zorn.agda
--- a/src/zorn.agda	Wed Oct 12 14:45:53 2022 +0900
+++ b/src/zorn.agda	Wed Oct 12 19:51:00 2022 +0900
@@ -1120,12 +1120,14 @@
                  csupfp : {w z : Ordinal } → supf1 w o< z → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 w) 
                  csupfp {w} {z} sw1<z z≤x with osuc-≡< z≤x
                  ... | case1 refl = csupf1 sw1<z
-                 ... | case2 lt with trio< (supf0 w) z
-                 ... | tri< sw<z ¬b ¬c = ? where
-                     csupfpx : odef (UnionCF A f mf ay supf0 z) (supf0 w) 
-                     csupfpx = ZChain.csupf zc sw<z (subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) lt )
-                 ... | tri≈ ¬a b ¬c = ?
-                 ... | tri> ¬a ¬b c =  ?
+                 ... | case2 lt = ? where
+                     csupfpx : supf0 w o< z → odef (UnionCF A f mf ay supf0 z) (supf0 w) 
+                     csupfpx sw<z = ZChain.csupf zc sw<z (subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) lt )
+                     cs10 : odef (UnionCF A f mf ay supf1 z) (supf1 w) 
+                     cs10 with trio< w px
+                     ... | tri< sw<z ¬b ¬c = ? 
+                     ... | tri≈ ¬a b ¬c = ?
+                     ... | tri> ¬a ¬b c =  ?
 
           zc4 : ZChain A f mf ay x     --- x o≤ supf px 
           zc4 with trio< x (supf0 px)