--- a/src/zorn.agda	Tue Jul 19 18:35:38 2022 +0900
+++ b/src/zorn.agda	Wed Jul 20 11:38:00 2022 +0900
@@ -501,7 +501,26 @@
               * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b = chain-mono2 x ? o≤-refl m04 where
+                 m12 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → odef (UnionCF A f mf ay (ZChain.supf zc) x) z1
+                 m12 = ?
+                 m11 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
+                 m11 {sup1} {z1} s<b fc with IsSup.x<sup is-sup (m12 s<b fc)
+                 ... | t = ?
+                 m07 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b
+                 m07 {y} (init ay1) = ?
+                 m07 {.(f x)} (fsuc x fc) with proj1 (mf x (A∋fc y f mf  fc))
+                 ... | case1 eq = subst ( λ k → k << ZChain.supf zc b) (subst₂ (λ j k → j ≡ k) &iso  &iso (cong (&) eq))  (m07 fc)
+                 ... | case2 lt  with ODC.p∨¬p O ( f x << ZChain.supf zc b )
+                 ... | case1 p = p
+                 ... | case2 np = ? where
+                     m08 : x <<　ZChain.supf zc b
+                     m08 = m07 fc
+                     m09 : ⊥
+                     m09 = fcn-imm y f mf ? ? ⟪ m08 , ?  ⟫
+                     m10 : ? ∨ ( ? <<  b )
+                     m10 = IsSup.x<sup is-sup ? -- (proj2 (mf x (A∋fc y f mf  fc)))
                  m05 : b ≡ ZChain.supf zc b
+                 m10 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
                  m05 = sym (ZChain.sup=u ? ab is-sup)   -- ZChain on x
                  m06 : ChainP A f mf ay (ZChain.supf zc) b b
                  m06 = record { fcy<sup = ? ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = ? }