# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668679446 -32400
# Node ID e5f46d08c074cfb5554d1e8261ea1c28e06dfa0d
# Parent  908369b2d08b8082d51d04002273d200b0eeb8d9
...

diff -r 908369b2d08b -r e5f46d08c074 src/zorn.agda
--- a/src/zorn.agda	Thu Nov 17 17:04:47 2022 +0900
+++ b/src/zorn.agda	Thu Nov 17 19:04:06 2022 +0900
@@ -1072,10 +1072,12 @@
                       ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) --   x o< b
                       z51 : FClosure A f (supf1 px) w
                       z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
+                      spx=px : supf1 px ≡ px
+                      spx=px = trans (sf1=sf0 o≤-refl) ( ZChain.sup=u zc (subst (λ k → odef A k) ? ?)  o≤-refl ? )
                       cp1 : ChainP A f mf ay supf1 px
                       cp1 = record { fcy<sup = λ {z} fc → ? 
                                ; order =  λ {s} {z} s<u fc  → ? 
-                               ; supu=u = ? }
+                               ; supu=u = spx=px }
                  ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) --  px o< a o< b o≤ x
 
                  zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z