# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670414572 -32400
# Node ID e6b9de04d0cad2137ace052acb945970199aef94
# Parent  a8d6ac036d882da88d0db41c6dc295717136bd80
...

diff -r a8d6ac036d88 -r e6b9de04d0ca src/zorn.agda
--- a/src/zorn.agda	Wed Dec 07 20:56:57 2022 +0900
+++ b/src/zorn.agda	Wed Dec 07 21:02:52 2022 +0900
@@ -1154,12 +1154,13 @@
                      zc36 : sp1 ≡ x   -- this cannot heppen because 
                      zc36 with osuc-≡< zc31
                      ... | case1 eq = trans eq (sym x=b)
-                     ... | case2 sp1<b = ⊥-elim ? where
+                     ... | case2 sp1<b = ⊥-elim (¬p<x<op ⟪ ? , ? ⟫ ) where
                         --   sp1 o< x → ⊥
                         --   supf0 px o≤ sp1 o< x → supf0 px o≤ px
                         --        px o≤ supf0 px → px ≡ spuf0 px o≤ spuf1 x o< x
+                        --        px ≡ supf1 x
                         sp1<x : sp1 o<  x
-                        sp1<x = subst (λ k → sp1 o< k ) ? sp1<b
+                        sp1<x = subst (λ k → sp1 o< k ) (sym x=b) sp1<b
                         zc38 : supf0 px o≤ px
                         zc38 = begin
                            supf0 px  ≡⟨ sym (sf1=sf0 o≤-refl)  ⟩