# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1663386831 -32400
# Node ID 7f03e1d2496107d278b4cfb5990a1a8389bc3f2b
# Parent  852bdf4a2df3b00ce68512242bc07e0552b40acf
...

diff -r 852bdf4a2df3 -r 7f03e1d24961 src/zorn.agda
--- a/src/zorn.agda	Sat Sep 17 10:11:54 2022 +0900
+++ b/src/zorn.agda	Sat Sep 17 12:53:51 2022 +0900
@@ -423,7 +423,11 @@
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
 
    csupf1 : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 
-   csupf1 {b} sb<z = ⟪ ? , ch-is-sup (supf b) ? record { fcy<sup = fcy<sup ? ; order = ? ; supu=u = ? }  (init ? ? ) ⟫
+   csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf b) sb<z record { fcy<sup = fcy<sup ? ; order = ? ; supu=u = ? }  (init (subst (λ k → odef A k) ? asb)  (supf-idem) ) ⟫ where
+        b<z : b o< z
+        b<z = supf-inject0 supf-mono ( ordtrans<-≤ sb<z (x≤supfx z) )
+        asb : odef A (supf b)
+        asb = supf∈A (o<→≤ b<z)
 
    -- ordering is not proved here but in ZChain1