--- a/src/zorn.agda	Wed Nov 23 18:03:23 2022 +0900
+++ b/src/zorn.agda	Wed Nov 23 19:30:29 2022 +0900
@@ -539,27 +539,10 @@
 
    fc-inject : {x y : Ordinal }  →  (mf< : <-monotonic-f A f) → x o≤ z → y o≤ z → supf x o< z → supf y o< z
       →  { wx wy  : Ordinal} →  FClosure A f (supf x) wx  →  FClosure A f (supf y) wy → wx ≡ wy → supf x ≡ supf y
-   fc-inject mf< x≤z y≤z sx<z sy<z (init xa eqa) (init ya eqb) refl = trans eqa (sym eqb)
-   fc-inject {x} {y} mf< x≤z y≤z sx<z sy<z (init xa eqx) (fsuc ya fcy) eq = 
-     ⊥-elim ( supf-¬hp x≤z (λ xa → proj1 (mf< _ xa)) record { ax = asupf ; y = ya ; ay = z53 ; x=fy = trans eqx eq } ) where
-        sy<sx : supf y << supf x
-        sy<sx =  ftrans<=-<  (≤to<= (s≤fc (supf y) f mf fcy)) (subst₂ (λ j k → j << k ) refl (trans (sym eq) (sym eqx)) 
-            (proj1 ( mf< _ (A∋fc (supf y) f mf fcy) )))
-        z53 : odef (UnionCF A f mf ay supf x) ya
-        z53 = cfcs mf< (supf-inject (supf-<inject sy<sx)) x≤z sy<z fcy
-   fc-inject {x} {y} mf< x≤z y≤z sx<z sy<z (fsuc xa fcx) (init ya eqy) eq = 
-     ⊥-elim ( supf-¬hp y≤z (λ xa → proj1 (mf< _ xa)) record { ax = asupf ; y = xa ; ay = z53 ; x=fy = trans eqy (sym eq) } ) where
-        sx<sy : supf x << supf y
-        sx<sy =  ftrans<=-<  (≤to<= (s≤fc (supf x) f mf fcx)) (subst₂ (λ j k → j << k ) refl (trans eq (sym eqy)) 
-            (proj1 ( mf< _ (A∋fc (supf x) f mf fcx) )))
-        z53 : odef (UnionCF A f mf ay supf y) xa
-        z53 = cfcs mf< (supf-inject (supf-<inject sx<sy))  y≤z sx<z fcx
-   fc-inject mf< x≤z y≤z sx<z sy<z (fsuc xa fcx) (fsuc ya fcy) eq = fc-inject mf< x≤z y≤z sx<z sy<z  fcx fcy (z54 eq)  where
-        z54 : f xa ≡ f ya  → xa ≡ ya
-        z54 fa=fb with trio< xa ya
-        ... | tri< a ¬b ¬c = ?
-        ... | tri≈ ¬a b ¬c = b
-        ... | tri> ¬a ¬b c = ?
+   fc-inject mf< x≤z y≤z sx<z sy<z = ? where
+        z53 : {x y : Ordinal } →  supf x o< supf y → FClosure A f (supf x) wx  →  wx << supf y
+        z53 = ?
+
 
 supf-unique :  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {y xa xb : Ordinal} → (ay : odef A y) →  (xa o≤ xb ) → (za : ZChain A f mf ay xa ) (zb : ZChain A f mf ay xb ) 
@@ -1484,7 +1467,11 @@
                        fc1m : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) u) w
                        fc1m = fc1
                        fc2 : FClosure A f (supf1 u) w
-                       fc2 = ?
+                       fc2 = subst (λ k → FClosure A f k w) (trans (sym (zeq _ _ zc57 (o<→≤ <-osuc))) (sym (sf1=sf (ordtrans≤-< u<x m<x))) )  fc1 where
+                           zc57 : osuc u o≤ osuc m 
+                           zc57 = osucc u<x
+                       fc1a : FClosure A f (ZChain.supf (pzc (ob<x lim a<x)) a) w
+                       fc1a = fc
                ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
                ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))