# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1671296685 -32400
# Node ID 7ec55b1bdfc21ea00b0a50dec94fd5c98bdf4207
# Parent  424af168622fe28386a14cc6085f6edb0a0a81ef
Zorn done

diff -r 424af168622f -r 7ec55b1bdfc2 src/zorn.agda
--- a/src/zorn.agda	Sat Dec 17 21:20:49 2022 +0900
+++ b/src/zorn.agda	Sun Dec 18 02:04:45 2022 +0900
@@ -1349,11 +1349,7 @@
           IC⊆ : {a b : Ordinal } (ia : IChain ay supfz a ) (ib : IChain ay supfz b )
               → IChain-i ia o< IChain-i ib → odef (ZChain.chain (pzc (pic<x ib))) a
           IC⊆ {a} {b} (ic-init fc ) ib ia<ib = ⟪ A∋fc _ f mf fc , ch-init fc ⟫
-          IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-init fcb ) ia<ib = ⊥-elim ( o<> ia<ib ic01 ) where
-               ic02 : o∅ o< supfz i<x
-               ic02 = ?
-               ic01 : o∅ o< i
-               ic01 = ordtrans<-≤ ic02 sa<x
+          IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-init fcb ) ia<ib = ⊥-elim ( ¬x<0 ia<ib  )
           IC⊆ {a} {b} (ic-isup i i<x sa<x fc ) (ic-isup j j<x sb<x fcb ) ia<ib
               = ZChain.cfcs (pzc (ob<x lim j<x) ) (o<→≤ ia<ib) o≤-refl (OrdTrans (ZChain.supf-mono (pzc (ob<x lim j<x)) (o<→≤ ia<ib)) sb<x)
                   (subst (λ k → FClosure A f k a) (zeq _ _ (osucc (o<→≤ ia<ib)) (o<→≤ <-osuc)) fc )