--- a/src/zorn.agda	Sat Jul 09 17:52:43 2022 +0900
+++ b/src/zorn.agda	Sat Jul 09 18:36:23 2022 +0900
@@ -261,10 +261,10 @@
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
    field
       psup :  Ordinal → Ordinal 
-      psup<z : (x : Ordinal ) →   psup x o< & A 
+      p≤z : (x : Ordinal ) →   odef A (psup x)
       chainf : (x : Ordinal) → HOD
       is-chain : (x w : Ordinal) → odef (chainf x) w → Chain A f mf ay (psup x ) w 
-      psup-mono : (x y : Ordinal) → (x≤z : x o≤ z ) → chainf x ⊆' chainf z 
+      psup-mono : (x : Ordinal) → (x≤z : x o≤ z ) → chainf x ⊆' chainf z 
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)  
           (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where
@@ -428,44 +428,37 @@
           sc : ZChain1 A f mf ay px
           sc = prev px px<x
           pchain : HOD
-          pchain  = record { od = record { def = λ x → odef A x ∧ Chain A f mf ay (ZChain1.psup sc ? ) x } 
-             ; odmax = & A ; <odmax =  λ {y} sy → ∈∧P→o< sy } 
+          pchain  = chainf sc px
 
+          no-ext : ZChain1 A f mf ay x
+          no-ext = record { psup = ZChain1.psup sc ; p≤z = ZChain1.p≤z sc ; chainf = ZChain1.chainf sc 
+              ; is-chain = ZChain1.is-chain sc ; psup-mono = sc0 } where
+            sc0 : (z : Ordinal) → z o≤ x → chainf sc z ⊆' chainf sc x
+            sc0 = ?
           sc4 : ZChain1 A f mf ay x
-          sc4 with o≤? x o∅
-          ... | yes x=0 = record { psup =  ? ; p≤z = ? ; p≤a = ? ; chainf = ? }
-          ... | no 0<x with ODC.∋-p O A (* x)
-          ... | no noax = record { psup = ZChain1.psup sc ; p≤z = ? ; p≤a = ? ; chainf = ? }
+          sc4 with ODC.∋-p O A (* x)
+          ... | no noax = record { psup = ZChain1.psup sc ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? }
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
-          ... | case1 pr = record { psup = ZChain1.psup sc ; p≤z = ? ; p≤a = ? ; chainf = ? }
+          ... | case1 pr = record { psup = ZChain1.psup sc ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? }
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { psup = ?  ; p≤z = ? ; p≤a = ? ; chainf = ? } where
+          ... | case1 is-sup = record { psup = ? ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? } where
                 schain : HOD
                 schain = ? -- record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) } 
                     -- ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
-                sc7 : ¬ HasPrev A ? (subst (λ k → odef A k) &iso ax) f
-                sc7 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) }
-                -- sc9 : Chain A f mf ay x schain
-                -- sc9 = ? -- ch-is-sup op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc7
-                    -- record { x<sup = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k )) &iso (IsSup.x<sup is-kjjkjjsup lt) }
-          ... | case2 ¬x=sup = record { psup = ZChain1.psup sc ; p≤z = ? ; p≤a = ? ; chainf = ? } where
-                sc17 : ¬ HasPrev A ? (subst (λ k → odef A k) &iso ax) f
-                sc17 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) }
-                sc10 : ¬ IsSup A ? (subst (λ k → odef A k) &iso ax)
-                sc10 not = ¬x=sup ( record { x<sup  = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k ) ) (sym &iso) ( IsSup.x<sup not lt ) }  )
+          ... | case2 ¬x=sup = record { psup = ZChain1.psup sc ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? }
      ... | no ¬ox = sc4 where
-          chainf : (z : Ordinal) → z o< x → HOD
-          chainf z z<x = ? -- Chain1.chain ( prev z z<x )
-          -- chainq : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x )
-          -- chainq z z<x = ? -- ZChain1.chain-uniq ( prev z z<x)
+          pchainf : (z : Ordinal) → z o< x → HOD
+          pchainf z z<x = ZChain1.chainf (prev z z<x) z
+          UZ : HOD
+          UZ = UnionCF A x pchainf
           sc4 : ZChain1 A f mf ay x
           sc4 with o≤? x o∅
-          ... | yes x=0 = record { psup =  ? ; p≤z = ? ; p≤a = ? ; chainf = ? }
+          ... | yes x=0 = record { psup = ? ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? }
           ... | no 0<x with ODC.∋-p O A (* x)
-          ... | no noax = record { psup = ? ; p≤z = ? ; p≤a = ? ; chainf = ? } 
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (UnionCF A x chainf) ax f )   
-          ... | case1 pr = record { psup = ? ; p≤z = ? ; p≤a = ? ; chainf = ? } 
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (UnionCF A x chainf) ax )
+          ... | no noax = record { psup = ? ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? }
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A (UnionCF A x pchainf) ax f )   
+          ... | case1 pr = record { psup = ? ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? }
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (UnionCF A x pchainf) ax )
           ... | case1 is-sup = ?
           ... | case2 ¬x=sup = ?