# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1666570549 -32400
# Node ID 409ac0af7b3b0fdcb9938538f09c94d49529549d
# Parent  b1899e33e2c7e0287fd108246b741f8782ac75dc
...

diff -r b1899e33e2c7 -r 409ac0af7b3b src/zorn1.agda
--- a/src/zorn1.agda	Mon Oct 24 06:41:01 2022 +0900
+++ b/src/zorn1.agda	Mon Oct 24 09:15:49 2022 +0900
@@ -735,8 +735,17 @@
           sd=d : supf d ≡ d
           sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
 
-          sc<<sd : supf mc << supf d
-          sc<<sd = ? 
+          sc<<d : {mc : Ordinal } → {asc : odef A (supf mc)} → (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
+             → supf mc << MinSUP.sup spd
+          sc<<d {mc} {asc} spd = z25 where
+                d1 :  Ordinal
+                d1 = MinSUP.sup spd
+                z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 )
+                z24 = MinSUP.x<sup spd (init asc refl)
+                z25 : supf mc << d1
+                z25 with z24
+                ... | case2 lt = lt
+                ... | case1 eq = ?
 
           sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d
           sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) )
@@ -746,7 +755,8 @@
           sms<sa : supf mc o< supf (& A)
           sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) ))
           ... | case2 lt = lt
-          ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd sc<<sd ) ( ZChain.supf-mono zc (o<→≤ d<A ))))
+          ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} {asc} spd)) ) 
+              ( ZChain.supf-mono zc (o<→≤ d<A ))))
 
           ss<sa : supf c o< supf (& A)
           ss<sa = subst (λ k → supf k o< supf (& A)) (sym c=mc) sms<sa