# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669587199 -32400
# Node ID 07ffcf16a3d4455969bab7a3ffdc80022d8f3136
# Parent  d1eecfc6cdfa838225744386e7ea02a8fe64cb28
ChainP removal

diff -r d1eecfc6cdfa -r 07ffcf16a3d4 src/zorn.agda
--- a/src/zorn.agda	Sun Nov 27 20:19:18 2022 +0900
+++ b/src/zorn.agda	Mon Nov 28 07:13:19 2022 +0900
@@ -265,23 +265,6 @@
       x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
 --
---  sup and its fclosure is in a chain HOD
---    chain HOD is sorted by sup as Ordinal and <-ordered
---    whole chain is a union of separated Chain
---    minimum index is sup of y not ϕ
---
-
-record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u : Ordinal) : Set n where
-   field
-      fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u )
-      order    : {s z1 : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
-      supu=u   : supf u ≡ u
-
-data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
-       (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where
-    ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
-    ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : u o< x) ( is-sup : ChainP A f mf ay supf u )
-        ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 
 --
 --         f (f ( ... (supf y))) f (f ( ... (supf z1)))
@@ -301,91 +284,34 @@
      fc00 :  * b ≤ * (f b)
      fc00 = proj1 (mf _ (subst (λ k → odef A k) a=b aa ))
 
---
--- data UChain is total
-
-chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
-   {s s1 a b : Ordinal } ( ca : UChain A f mf ay supf s a ) ( cb : UChain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
-chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
-     ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
-     ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb
-     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) with ChainP.fcy<sup supb fca
-     ... | case1 eq with s≤fc (supf ub) f mf fcb
-     ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-          ct00 : * a ≡ * b
-          ct00 = trans (cong (*) eq) eq1
-     ... | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
-          ct01 : * a < * b
-          ct01 = subst (λ k → * k < * b ) (sym eq) lt
-     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub u<x supb fcb) | case2 lt = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
-          ct00 : * a < * (supf ub)
-          ct00 = lt
-          ct01 : * a < * b
-          ct01 with s≤fc (supf ub) f mf fcb
-          ... | case1 eq =  subst (λ k → * a < k ) eq ct00
-          ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) with ChainP.fcy<sup supa fcb
-     ... | case1 eq with s≤fc (supf ua) f mf fca
-     ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
+fc-total : (A : HOD ) ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) (supf : Ordinal → Ordinal )
+    (order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y)
+   {s s1 a b : Ordinal } ( fa : FClosure A f (supf s) a )( fb : FClosure A f (supf s1) b )  → Tri (* a < * b) (* a ≡ * b) (* b < * a )
+fc-total A f mf supf order {xa} {xb} {a} {b} ca cb with trio< xa xb
+... | tri< a₁ ¬b ¬c with order a₁ ? 
+... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
-          ct00 = sym (trans (cong (*) eq) eq1 )
-     ... | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
-          ct01 : * b < * a
-          ct01 = subst (λ k → * k < * a ) (sym eq) lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua u<x supa fca) (ch-init fcb) | case2 lt = tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
-          ct00 : * b < * (supf ua)
-          ct00 = lt
-          ct01 : * b < * a
-          ct01 with s≤fc (supf ua) f mf fca
-          ... | case1 eq =  subst (λ k → * b < k ) eq ct00
-          ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< ua ub
-     ... | tri< a₁ ¬b ¬c with ChainP.order supb  (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supa )) (sym (ChainP.supu=u supb )) a₁)  fca
-     ... | case1 eq with s≤fc (supf ub) f mf fcb
-     ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-          ct00 : * a ≡ * b
-          ct00 = trans (cong (*) eq) eq1
-     ... | case2 lt =  tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
+          ct00 = ? -- trans (cong (*) eq) eq1
+... | case2 lt =  tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
           ct02 : * a < * b
-          ct02 = subst (λ k → * k < * b ) (sym eq) lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri< a₁ ¬b ¬c | case2 lt = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
-          ct03 : * a < * (supf ub)
-          ct03 = lt
-          ct02 : * a < * b
-          ct02 with s≤fc (supf ub) f mf fcb
-          ... | case1 eq =  subst (λ k → * a < k ) eq ct03
-          ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x  supb fcb) | tri≈ ¬a  eq ¬c
-         = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (cong supf (sym eq)) fcb )
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supb )) (sym (ChainP.supu=u supa )) c) fcb
-     ... | case1 eq with s≤fc (supf ua) f mf fca
-     ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-          ct00 : * a ≡ * b
-          ct00 = sym (trans (cong (*) eq) eq1)
-     ... | case2 lt =  tri> (λ lt → <-irr (case2 ct02) lt) (λ eq → <-irr (case1 eq) ct02) ct02    where
-          ct02 : * b < * a
-          ct02 = subst (λ k → * k < * a ) (sym eq) lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c | case2 lt = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
-          ct05 : * b < * (supf ua)
-          ct05 = lt
-          ct04 : * b < * a
-          ct04 with s≤fc (supf ua) f mf fca
-          ... | case1 eq =  subst (λ k → * b < k ) eq ct05
-          ... | case2 lt =  IsStrictPartialOrder.trans POO ct05 lt
+          ct02 = ? -- subst (λ k → * k < * b ) (sym eq) lt
+fc-total f mf supf {xa} {xb} {a} {b} ca cb | tri< a₁ ¬b ¬c = ?
+
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
 
 -- Union of supf z which o< x
 --
-UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
-    ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
-UnionCF A f mf ay supf x
-   = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
+-- UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
+--     ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
+-- UnionCF A f supf x
+--    = record { od = record { def = λ z → odef A z ∧ UChain A f supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
-UnionCF' : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
-    ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
-UnionCF' A f mf ay supf x
+--      order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y
+--
+UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal )  ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
+UnionCF A f supf x
    = record { od = record { def = λ z → odef A z ∧ ( { s : Ordinal} → s o< x → FClosure A f (supf s) z ) } ;   
        odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
@@ -412,12 +338,12 @@
 
 M→S  : { A : HOD } { f : Ordinal → Ordinal } {mf : ≤-monotonic-f A f} {y : Ordinal} {ay : odef A y}  { x : Ordinal }
       →  (supf : Ordinal → Ordinal )
-      →  MinSUP A (UnionCF A f mf ay supf x)
-      → SUP A (UnionCF A f mf ay supf x)
+      →  MinSUP A (UnionCF A f supf x)
+      → SUP A (UnionCF A f supf x)
 M→S {A} {f} {mf} {y} {ay} {x} supf ms = record { sup = * (MinSUP.sup ms)
         ; as = subst (λ k → odef A k) (sym &iso) (MinSUP.asm ms) ; x≤sup = ms00 } where
    msup = MinSUP.sup ms
-   ms00 : {z : HOD} → UnionCF A f mf ay supf x ∋ z → (z ≡ * msup) ∨ (z < * msup)
+   ms00 : {z : HOD} → UnionCF A f supf x ∋ z → (z ≡ * msup) ∨ (z < * msup)
    ms00 {z} uz with MinSUP.x≤sup ms uz
    ... | case1 eq = case1 (subst (λ k → k ≡ _) *iso ( cong (*) eq))
    ... | case2 lt = case2 (subst₂ (λ j k →  j < k ) *iso refl lt )
@@ -425,11 +351,8 @@
 
 chain-mono : {A : HOD}  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
    (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b
-        → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c
-chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ =
-        ⟪ ua , ch-init fc  ⟫
-chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ =
-        ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b) is-sup fc  ⟫
+        → odef (UnionCF A f supf a) c → odef (UnionCF A f supf b) c
+chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa , ch-is-sup  ⟫ = ?
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
@@ -437,44 +360,39 @@
       supf :  Ordinal → Ordinal
 
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
-           → IsSUP A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) f b ) → supf b ≡ b
+           → IsSUP A (UnionCF A f supf b) ab ∧ (¬ HasPrev A (UnionCF A f supf b) f b ) → supf b ≡ b
       cfcs : (mf< : <-monotonic-f A f)
-         {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f mf ay supf b) w
+         {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f supf b) w
       order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y
 
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
 
-      minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x)
+      minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f supf x)
       supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
 
    chain : HOD
-   chain = UnionCF A f mf ay supf z
+   chain = UnionCF A f supf z
    chain⊆A : chain ⊆' A
    chain⊆A = λ lt → proj1 lt
 
-   sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
+   sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f supf x)
    sup {x} x≤z = M→S supf (minsup x≤z)
 
    s=ms : {x : Ordinal } → (x≤z : x o≤ z ) → & (SUP.sup (sup x≤z)) ≡ MinSUP.sup (minsup x≤z)
    s=ms {x} x≤z = &iso
 
    chain∋init : odef chain y
-   chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
-   f-next : {a z : Ordinal} → odef (UnionCF A f mf ay supf z) a → odef (UnionCF A f mf ay supf z) (f a)
-   f-next {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-   f-next {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u<x is-sup (fsuc _ fc ) ⟫
+   chain∋init = ⟪ ay , ?   ⟫
+   f-next : {a z : Ordinal} → odef (UnionCF A f supf z) a → odef (UnionCF A f supf z) (f a)
+   f-next {a} ⟪ aa , ch-is-sup  ⟫ = ?
    initial : {z : Ordinal } → odef chain z → * y ≤ * z
-   initial {a} ⟪ aa , ua ⟫  with  ua
-   ... | ch-init fc = s≤fc y f mf fc
-   ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
-        zc7 : y <= supf u
-        zc7 = ChainP.fcy<sup is-sup (init ay refl)
+   initial {a} ⟪ aa , ua ⟫  = ?
    f-total : IsTotalOrderSet chain
    f-total {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay supf ( (proj2 ca)) ( (proj2 cb))
+               uz01 = ? -- chain-total A f supf ( (proj2 ca)) ( (proj2 cb))
 
    supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y
    supf-inject {x} {y} sx<sy with trio< x y
@@ -488,21 +406,20 @@
    supf<A = z09 asupf
 
    csupf : (mf< : <-monotonic-f A f) {b : Ordinal } 
-      → supf b o< supf z → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
+      → supf b o< supf z → supf b o< z → odef (UnionCF A f supf z) (supf b) -- supf z is not an element of this chain
    csupf mf< {b} sb<sz sb<z = cfcs mf< (supf-inject sb<sz) o≤-refl sb<z (init asupf refl)
 
    fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf
-   fcy<sup  {u} {w} u≤z fc with MinSUP.x≤sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)
-       , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫
+   fcy<sup  {u} {w} u≤z fc with MinSUP.x≤sup (minsup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc) , ? ⟫ 
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans eq (sym (supf-is-minsup u≤z ) ) ))
    ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt )
 
    -- ordering is not proved here but in ZChain1
 
    IsMinSUP→NotHasPrev : {x sp : Ordinal } → odef A sp
-       → ({y : Ordinal} → odef (UnionCF A f mf ay supf x) y → (y ≡ sp ) ∨ (y << sp ))
+       → ({y : Ordinal} → odef (UnionCF A f supf x) y → (y ≡ sp ) ∨ (y << sp ))
        → ( {a : Ordinal } → odef A a → a << f a )
-       → ¬ ( HasPrev A (UnionCF A f mf ay supf x) f sp )
+       → ¬ ( HasPrev A (UnionCF A f supf x) f sp )
    IsMinSUP→NotHasPrev {x} {sp} asp is-sup <-mono-f hp = ⊥-elim (<-irr ( <=to≤  fsp≤sp) sp<fsp ) where
        sp<fsp : sp << f sp
        sp<fsp = <-mono-f asp
@@ -514,32 +431,29 @@
 
    supf-¬hp : {x  : Ordinal } → x o≤ z 
        → ( {a : Ordinal } → odef A a → a << f a )
-       → ¬ ( HasPrev A (UnionCF A f mf ay supf x) f (supf x) )
+       → ¬ ( HasPrev A (UnionCF A f supf x) f (supf x) )
    supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw → 
        (subst (λ k → w <= k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp
 
    supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
    supf-idem  mf< {b} b≤z sfb≤x = z52 where
-       z54 :  {w : Ordinal} → odef (UnionCF A f mf ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
-       z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
-       z54 {w} ⟪ aw , ch-is-sup u u<x is-sup fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k )) 
-                   (sym (supf-is-minsup b≤z)) 
-                   (MinSUP.x≤sup (minsup b≤z) (cfcs mf< u<b b≤z (subst (λ k → k o< b) (sym (ChainP.supu=u is-sup)) u<b) fc )) where
-               u<b : u o< b
-               u<b = supf-inject ( subst (λ k → k o< supf b) (sym (ChainP.supu=u is-sup)) u<x )
+       z54 :  {w : Ordinal} → odef (UnionCF A f supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
+       z54 {w} ⟪ aw , fc ⟫ = order ? ? where
+               u<b : supf b o< b
+               u<b = ?
        z52 : supf (supf b) ≡ supf b
        z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
 
-   -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → ChainP A f mf ay supf (supf b)
+   -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → ChainP A f supf (supf b)
    --    the condition of cfcs is satisfied, this is obvious
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc
    field
-      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z  → (ab : odef A b)
-          → HasPrev A (UnionCF A f mf ay supf z) f b ∨  IsSUP A (UnionCF A f mf ay supf b) ab
-          → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
+      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f supf z) a ) → b o< z  → (ab : odef A b)
+          → HasPrev A (UnionCF A f supf z) f b ∨  IsSUP A (UnionCF A f supf b) ab
+          → * a < * b  → odef ((UnionCF A f supf z)) b
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -548,8 +462,8 @@
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
 init-uchain : (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y )
-    { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y
-init-uchain A f mf ay = ⟪ ay , ch-init (init ay refl)   ⟫
+    { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f supf x) y
+init-uchain A f mf ay = ⟪ ay , ?   ⟫
 
 record IChain  (A : HOD)  ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
   field
@@ -586,25 +500,8 @@
                  spa ≡⟨ sym sax=spa ⟩ 
                  supfa x ∎ ) a ) where 
                     open o≤-Reasoning O
-                    z53 : {z : Ordinal } →  odef (UnionCF A f mf ay (ZChain.supf zb) x) z →  odef (UnionCF A f mf ay (ZChain.supf za) x) z
-                    z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 
-                    z53 {z} ⟪ as , ch-is-sup u u<x is-sup fc ⟫ =  ⟪ as , ch-is-sup u u<x z54 z55  ⟫ where
-                        ua=ub : supfa u ≡ supfb u
-                        ua=ub = prev u u<x (ordtrans u<x x≤xa )
-                        order :  {s z1 : Ordinal} → ZChain.supf za s o< ZChain.supf za u → FClosure A f (ZChain.supf za s) z1 →
-                            (z1 ≡ ZChain.supf za u) ∨ (z1 << ZChain.supf za u)
-                        order {s} {z1} lt fc = subst (λ k → z1 <= k) (sym ua=ub) 
-                             (ChainP.order is-sup (subst₂ ( λ j k → j o< k ) z56 ua=ub lt ) (subst (λ k → FClosure A f k z1 ) z56 fc )) where
-                             s<x : s o< x
-                             s<x = ordtrans (ZChain.supf-inject za lt) u<x
-                             z56 : supfa s ≡ supfb s
-                             z56 = prev s s<x (ordtrans s<x x≤xa)
-                        z54 : ChainP A f mf ay (ZChain.supf za) u  
-                        z54 = record { fcy<sup = λ {w} fc → subst (λ k → w <= k ) (sym ua=ub) (ChainP.fcy<sup is-sup fc )
-                          ; order = order
-                          ; supu=u = trans ua=ub (ChainP.supu=u is-sup) } 
-                        z55 : FClosure A f (ZChain.supf za u) z
-                        z55 = subst (λ k → FClosure A f k z ) (sym ua=ub) fc
+                    z53 : {z : Ordinal } →  odef (UnionCF A f (ZChain.supf zb) x) z →  odef (UnionCF A f (ZChain.supf za) x) z
+                    z53 {z} ⟪ as , cp ⟫ =  ⟪ as , ?  ⟫ 
            ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (
                begin
                  supfa x  ≡⟨ sax=spa ⟩
@@ -612,37 +509,18 @@
                  spb  ≡⟨ sym sbx=spb ⟩
                  supfb x ∎ ) c ) where 
                     open o≤-Reasoning O
-                    z53 : {z : Ordinal } →  odef (UnionCF A f mf ay (ZChain.supf za) x) z →  odef (UnionCF A f mf ay (ZChain.supf zb) x) z
-                    z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 
-                    z53 {z} ⟪ as , ch-is-sup u u<x is-sup fc ⟫ =  ⟪ as , ch-is-sup u u<x z54 z55  ⟫ where
-                        ub=ua : supfb u ≡ supfa u
-                        ub=ua = sym ( prev u u<x (ordtrans u<x x≤xa ))
-                        order :  {s z1 : Ordinal} → ZChain.supf zb s o< ZChain.supf zb u → FClosure A f (ZChain.supf zb s) z1 →
-                            (z1 ≡ ZChain.supf zb u) ∨ (z1 << ZChain.supf zb u)
-                        order {s} {z1} lt fc = subst (λ k → z1 <= k) (sym ub=ua) 
-                             (ChainP.order is-sup (subst₂ ( λ j k → j o< k ) z56 ub=ua lt ) (subst (λ k → FClosure A f k z1 ) z56 fc )) where
-                             s<x : s o< x
-                             s<x = ordtrans (ZChain.supf-inject zb lt) u<x
-                             z56 : supfb s ≡ supfa s
-                             z56 = sym (prev s s<x (ordtrans s<x x≤xa))
-                        z54 : ChainP A f mf ay (ZChain.supf zb) u  
-                        z54 = record { fcy<sup = λ {w} fc → subst (λ k → w <= k ) (sym ub=ua) (ChainP.fcy<sup is-sup fc )
-                          ; order = order
-                          ; supu=u = trans ub=ua (ChainP.supu=u is-sup) } 
-                        z55 : FClosure A f (ZChain.supf zb u) z
-                        z55 = subst (λ k → FClosure A f k z ) (sym ub=ua) fc
+                    z53 : {z : Ordinal } →  odef (UnionCF A f (ZChain.supf za) x) z →  odef (UnionCF A f (ZChain.supf zb) x) z
+                    z53 {z} ⟪ as , cp ⟫ =  ⟪ as , ?  ⟫ 
 
 UChain-eq : { A : HOD }    { f : Ordinal → Ordinal }  {mf : ≤-monotonic-f A f}
         {z y : Ordinal} {ay : odef A y}  { supf0 supf1 : Ordinal → Ordinal }
         → (seq : {x : Ordinal } →  x o<  z  → supf0 x ≡ supf1 x )
-        → UnionCF A f mf ay supf0 z ≡ UnionCF A f mf ay supf1 z
+        → UnionCF A f supf0 z ≡ UnionCF A f supf1 z
 UChain-eq {A} {f} {mf} {z} {y} {ay} {supf0} {supf1} seq = ==→o≡  record { eq← = ueq← ; eq→ = ueq→ } where
-      ueq← :  {x : Ordinal} → odef A x ∧ UChain A f mf ay supf1 z x → odef A x ∧ UChain A f mf ay supf0 z x
-      ueq← {z} ⟪ ab , ch-init fc ⟫ = ⟪ ab , ch-init fc ⟫
-      ueq← {z} ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , ch-is-sup u u<x ? ? ⟫ 
-      ueq→  : {x : Ordinal} → odef A x ∧ UChain A f mf ay supf0 z x → odef A x ∧ UChain A f mf ay supf1 z x
-      ueq→ {z} ⟪ ab , ch-init fc ⟫ = ⟪ ab , ch-init fc ⟫
-      ueq→ {z} ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , ch-is-sup u u<x ? ? ⟫ 
+      ueq← :  {x : Ordinal} → odef A x ∧ ? → odef A x ∧ ?
+      ueq← {z} ⟪ ab , cp ⟫ = ⟪ ab , ? ⟫ 
+      ueq→  : {x : Ordinal} → odef A x ∧ ? → odef A x ∧ ?
+      ueq→ {z} ⟪ ab , cp ⟫ = ⟪ ab , ? ⟫ 
 
 Zorn-lemma : { A : HOD }
     → o∅ o< & A
@@ -755,15 +633,13 @@
         {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → x o≤ & A → ZChain1 A f mf ay zc x
      SZ1 f mf mf< {y} ay zc x x≤A = zc1 x x≤A  where
         chain-mono1 :  {a b c : Ordinal} → a o≤ b
-            → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
+            → odef (UnionCF A f (ZChain.supf zc) a) c → odef (UnionCF A f (ZChain.supf zc) b) c
         chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b
-        is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → (ab : odef A b)
-            → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) f b
-            → * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
+        is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f (ZChain.supf zc) x) a → (ab : odef A b)
+            → HasPrev A (UnionCF A f (ZChain.supf zc) x) f b
+            → * a < * b → odef (UnionCF A f (ZChain.supf zc) x) b
         is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev
-        ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫
-        ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
-                      (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc))  ⟫
+        ... | ⟪ ab0 , cp ⟫ = ⟪ ab , ? ⟫
 
         supf = ZChain.supf zc
 
@@ -771,25 +647,25 @@
         zc1 x x≤A with Oprev-p x  
         ... | yes op = record { is-max = is-max } where
                px = Oprev.oprev op
-               is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
+               is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f supf x) a →
                   b o< x → (ab : odef A b) →
-                  HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
-                  * a < * b → odef (UnionCF A f mf ay supf x) b
+                  HasPrev A (UnionCF A f supf x) f b  ∨ IsSUP A (UnionCF A f supf b) ab →
+                  * a < * b → odef (UnionCF A f supf x) b
                is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
                is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
                is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
                ... | case2 sb<sx = m10 where
                   b<A : b o< & A
                   b<A = z09 ab
-                  m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
+                  m04 : ¬ HasPrev A (UnionCF A f supf b) f b
                   m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                         chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
                   m05 : ZChain.supf zc b ≡ b
                   m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
-                  m10 : odef (UnionCF A f mf ay supf x) b
+                  m10 : odef (UnionCF A f supf x) b
                   m10 = ZChain.cfcs zc mf< b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
-                  m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x )
+                  m17 : MinSUP A (UnionCF A f supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
                   m18 : supf x ≡ MinSUP.sup m17 
                   m18 = ZChain.supf-is-minsup zc x≤A
@@ -797,39 +673,39 @@
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
-                          m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
+                          m04 : ¬ HasPrev A (UnionCF A f supf b) f b
                           m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                                 chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
                           m05 : ZChain.supf zc b ≡ b
                           m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
                           m14 : ZChain.supf zc b o< x
                           m14 = subst (λ k → k o< x ) (sym m05)  b<x
-                          m13 :  odef (UnionCF A f mf ay supf x) z
+                          m13 :  odef (UnionCF A f supf x) z
                           m13 = ZChain.cfcs zc mf< b<x x≤A m14 fc
 
         ... | no lim = record { is-max = is-max }  where
-               is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
+               is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f supf x) a →
                   b o< x → (ab : odef A b) →
-                  HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
-                  * a < * b → odef (UnionCF A f mf ay supf x) b
+                  HasPrev A (UnionCF A f supf x) f b  ∨ IsSUP A (UnionCF A f supf b) ab →
+                  * a < * b → odef (UnionCF A f supf x) b
                is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
                is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
                is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
-               ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
+               ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ?  ⟫
                ... | case2 y<b with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
                ... | case2 sb<sx = m10 where
                   m09 : b o< & A
                   m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-                  m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
+                  m04 : ¬ HasPrev A (UnionCF A f supf b) f b
                   m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                           chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp)
                      ; x=fy = HasPrev.x=fy nhp } )
                   m05 : ZChain.supf zc b ≡ b
                   m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
-                  m10 : odef (UnionCF A f mf ay supf x) b
+                  m10 : odef (UnionCF A f supf x) b
                   m10 = ZChain.cfcs zc mf< b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
-                  m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x )
+                  m17 : MinSUP A (UnionCF A f supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
                   m18 : supf x ≡ MinSUP.sup m17 
                   m18 = ZChain.supf-is-minsup zc x≤A
@@ -837,14 +713,14 @@
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
-                          m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
+                          m04 : ¬ HasPrev A (UnionCF A f supf b) f b
                           m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                                 chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
                           m05 : ZChain.supf zc b ≡ b
                           m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
                           m14 : ZChain.supf zc b o< x
                           m14 = subst (λ k → k o< x ) (sym m05)  b<x
-                          m13 :  odef (UnionCF A f mf ay supf x) z
+                          m13 :  odef (UnionCF A f supf x) z
                           m13 = ZChain.cfcs zc mf< b<x x≤A m14 fc
 
      uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
@@ -895,7 +771,7 @@
 
           supf0 = ZChain.supf zc
           pchain  : HOD
-          pchain   = UnionCF A f mf ay supf0 px
+          pchain   = UnionCF A f supf0 px
 
           supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b
           supf-mono = ZChain.supf-mono zc
@@ -913,13 +789,13 @@
           --
 
           pchainpx : HOD
-          pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z )
+          pchainpx = record { od = record { def = λ z →  (odef A z ∧ ? )
                 ∨ FClosure A f (supf0 px) z  } ; odmax = & A ; <odmax = zc00 } where
-               zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → z o< & A
+               zc00 : {z : Ordinal } → (odef A z ∧ ? ) ∨ FClosure A f (supf0 px) z → z o< & A
                zc00 {z} (case1 lt) = z07 lt
                zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf fc )
 
-          zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f (supf0 px) b → a <= b
+          zc02 : { a b : Ordinal } → odef A a ∧ ? → FClosure A f (supf0 px) b → a <= b
           zc02 {a} {b} ca fb = zc05 fb where
              zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ supf0 px
              zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) refl
@@ -928,13 +804,13 @@
              ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
              ... | case2 lt = <=-trans (zc05 fb) (case2 lt)
              zc05 (init b1 refl) with MinSUP.x≤sup (ZChain.minsup zc o≤-refl)
-                (subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca )
+                (subst (λ k → odef A k ∧ ?) (sym &iso) ca )
              ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq )
              ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt )
 
           ptotal : IsTotalOrderSet pchainpx
           ptotal (case1 a) (case1 b) =  subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso
-                   (chain-total A f mf ay supf0 (proj2 a) (proj2 b))
+                   ?
           ptotal {a0} {b0} (case1 a) (case2 b) with zc02 a b
           ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where
                eq1 : a0 ≡ b0
@@ -1009,18 +885,18 @@
                  ... | tri≈ ¬a b ¬c =  subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (subst (λ k → a o≤ k) b a≤b))) refl ( supf-mono a≤b )
                  supf1-mono {a} {b} a≤b | tri> ¬a ¬b c with trio< a px
                  ... | tri< a<px ¬b ¬c = zc19 where
-                       zc21 : MinSUP A (UnionCF A f mf ay supf0 a)
+                       zc21 : MinSUP A (UnionCF A f supf0 a)
                        zc21 = ZChain.minsup zc (o<→≤ a<px)
-                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
+                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
                        zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ a<px) ux ) )
                        zc19 : supf0 a o≤ sp1
                        zc19 = subst (λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc  (o<→≤ a<px))) ( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
                  ... | tri≈ ¬a b ¬c = zc18 where
-                       zc21 : MinSUP A (UnionCF A f mf ay supf0 a)
+                       zc21 : MinSUP A (UnionCF A f supf0 a)
                        zc21 = ZChain.minsup zc (o≤-refl0 b)
                        zc20 : MinSUP.sup zc21 ≡ supf0 a
                        zc20 = sym (ZChain.supf-is-minsup zc (o≤-refl0 b))
-                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f mf ay supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
+                       zc24 : {x₁ : Ordinal} → odef (UnionCF A f supf0 a) x₁ → (x₁ ≡ sp1) ∨ (x₁ << sp1)
                        zc24 {x₁} ux = MinSUP.x≤sup sup1 (case1 (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o≤-refl0 b) ux ) )
                        zc18 : supf0 a o≤ sp1
                        zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 )
@@ -1042,7 +918,7 @@
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
                  cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
-                     → a o< b → b o≤ x → supf1 a o< b  → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
+                     → a o< b → b o≤ x → supf1 a o< b  → FClosure A f (supf1 a) w → odef (UnionCF A f supf1 b) w
                  cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with zc43 (supf0 a) px
                  ... | case2 px≤sa = z50 where
                       a<x : a o< x
@@ -1051,9 +927,9 @@
                       a≤px = subst (λ k → a o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)
                       --  supf0 a ≡ px we cannot use previous cfcs, it is in the chain because
                       --       supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
-                      z50 : odef (UnionCF A f mf ay supf1 b) w
+                      z50 : odef (UnionCF A f supf1 b) w
                       z50 with osuc-≡< px≤sa
-                      ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 cp (subst (λ k → FClosure A f k w) z52 fc)  ⟫ where
+                      ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ?  ⟫ where
                           sa≤px : supf0 a o≤ px
                           sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x
                           spx=sa : supf0 px ≡ supf0 a
@@ -1071,7 +947,7 @@
                                 supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px)  ⟩ 
                                 supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩ 
                                 supf1 (supf0 px) ∎ where open ≡-Reasoning
-                          m : MinSUP A (UnionCF A f mf ay supf0 px)
+                          m : MinSUP A (UnionCF A f supf0 px)
                           m = ZChain.minsup zc o≤-refl
                           m=spx : MinSUP.sup m ≡ supf1 (supf0 px)
                           m=spx = begin 
@@ -1086,11 +962,9 @@
                                 supf1 (supf0 a)  ≡⟨ sf1=sf0 sa≤px ⟩ 
                                 supf0 (supf0 a)  ≡⟨ sym ( cong supf0 px=sa ) ⟩ 
                                 supf0 px  ∎  where open ≡-Reasoning 
-                          cp : ChainP A f mf ay supf1 (supf0 px)
-                          cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=spx (MinSUP.x≤sup m ⟪  A∋fc _ f mf fc , ch-init fc ⟫ )  
-                            ; order = order 
-                            ; supu=u = z53 } where
-                             uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
+                          cp : ?
+                          cp = ? where
+                             uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f supf0 px) z1
                              uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<px o≤-refl ss<px (subst (λ k → FClosure A f k z1) 
                                      (sf1=sf0 (o<→≤ s<px))  fc ) where
                                 s<spx : s o< supf0 px
@@ -1117,36 +991,12 @@
                           z53  = ordtrans<-≤ sa<b b≤x
                  ... | case1 sa<px with trio< a px
                  ... | tri< a<px ¬b ¬c = z50 where
-                      z50 : odef (UnionCF A f mf ay supf1 b) w
+                      z50 : odef (UnionCF A f supf1 b) w
                       z50 with osuc-≡< b≤x
                       ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc  
-                      ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                      ... | ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc u≤px )  ⟫  where -- u o< px → u o< b ?
-                           u≤px : u o≤ px
-                           u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op))  (ordtrans<-≤ u<b b≤x )
-                           u<x : u o< x
-                           u<x = ordtrans<-≤ u<b b≤x 
-                           cp1 : ChainP A f mf ay supf1 u
-                           cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) (ChainP.fcy<sup is-sup fc )  
-                               ; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) 
-                                  (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) 
-                                   (sym (sf=eq u<x)) s<u)  
-                                    (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc ))
-                               ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup)  }
+                      ... | ⟪ az , cp ⟫ = ⟪ az , ?  ⟫  -- u o< px → u o< b ?
                       z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl sa<px fc  
-                      ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                      ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc (o<→≤ u<px)) ⟫  where -- u o< px → u o< b ?
-                           u<b : u o< b
-                           u<b = subst (λ k → u o< k ) (trans (Oprev.oprev=x op) (sym eq) ) (ordtrans u<px <-osuc )
-                           u<x : u o< x
-                           u<x = subst (λ k → u o< k ) (Oprev.oprev=x op) ( ordtrans u<px <-osuc )
-                           cp1 : ChainP A f mf ay supf1 u
-                           cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) (ChainP.fcy<sup is-sup fc )  
-                               ; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) 
-                                  (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) 
-                                   (sym (sf=eq u<x)) s<u)  
-                                    (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc ))
-                               ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup)  }
+                      ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫  where -- u o< px → u o< b ?
                  ... | tri≈ ¬a a=px ¬c = csupf1 where
                       -- a ≡ px , b ≡ x, sp o≤ x 
                       px<b : px o< b
@@ -1160,9 +1010,9 @@
                       z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc
                       z53 : odef A w
                       z53 = A∋fc {A} _ f mf fc
-                      csupf1 : odef (UnionCF A f mf ay supf1 b) w
+                      csupf1 : odef (UnionCF A f supf1 b) w
                       csupf1 with trio< (supf0 px) x
-                      ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) cp1 fc1 ⟫  where
+                      ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ? ⟫  where
                           spx = supf0 px
                           spx≤px : supf0 px o≤ px
                           spx≤px = zc-b<x _ sfpx<x
@@ -1185,11 +1035,6 @@
                                             supf1 spx  ≡⟨ sf1=sf0 spx≤px  ⟩
                                             supf0 spx  ≤⟨ ZChain.supf-mono zc spx≤px ⟩
                                             supf0 px  ∎  ) where open o≤-Reasoning O
-                          cp1 : ChainP A f mf ay supf1 spx
-                          cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ (z << k )) (sym (sf1=sf0 spx≤px )) 
-                                  ( ZChain.fcy<sup zc spx≤px fc )
-                                       ; order =  order
-                                       ; supu=u = z52 }
                       ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where 
                           -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case
                           m12 : supf0 px ≡ sp1
@@ -1203,37 +1048,17 @@
                       ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans sfpx≤sp1 sp≤x)))   -- x o< supf0 px o≤ sp1 ≤ x
                  ... | 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
-                 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
-                 zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc21 fc where
-                    u≤px : u o≤ px
-                    u≤px = zc-b<x _ u<x
-                    zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1
+                 zc11 : {z : Ordinal} → odef (UnionCF A f supf1 x) z → odef pchainpx z
+                 zc11 {z} ⟪ az , cp ⟫ = zc21 ? where
+                    zc21 : {z1 : Ordinal } → FClosure A f (supf1 ?) z1 → odef pchainpx z1
                     zc21 {z1} (fsuc z2 fc ) with zc21 fc
-                    ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-                    ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
+                    ... | case1 ⟪ ua1 , cp  ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ? ⟫
                     ... | case2 fc = case2 (fsuc _ fc)
-                    zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) | inspect supf1 u
-                    ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u u<px record {fcy<sup = zc13 ; order = zc17
-                         ; supu=u = trans (sym (sf1=sf0 (o<→≤ u<px))) (ChainP.supu=u is-sup) } (init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where
-                        u<px :  u o< px
-                        u<px =  ZChain.supf-inject zc a
-                        asp0 : odef A (supf0 u)
-                        asp0 = ZChain.asupf zc
-                        zc17 :  {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u →
-                            FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
-                        zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 u≤px)) ( ChainP.order is-sup
-                         (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 u≤px)) ss<spx) (fcpu fc zc18) ) where
-                            zc18 : s o≤ px
-                            zc18 = ordtrans (ZChain.supf-inject zc ss<spx) u≤px
-                        zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u )
-                        zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ u<px)) ( ChainP.fcy<sup is-sup fc )
-                    ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b )))
-                    ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫ )
+                    zc21 (init asp refl ) = ?
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
-                         tsup : MinSUP A (UnionCF A f mf ay supf1 z)
+                         tsup : MinSUP A (UnionCF A f supf1 z)
                          tsup=sup : supf1 z ≡ MinSUP.sup tsup
 
                  sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
@@ -1241,27 +1066,26 @@
                  ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m
                          ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where
                     m = ZChain.minsup zc (o<→≤ a)
-                    ms00 :  {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
-                    ms00 {w} ⟪ az , ch-init fc ⟫ = MinSUP.x≤sup m ?
-                    ms00 {w} ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = MinSUP.x≤sup m ⟪ az , ch-is-sup u ? ? ? ⟫ 
+                    ms00 :  {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
+                    ms00 {w} ⟪ az , cp ⟫ = MinSUP.x≤sup m ⟪ az , ? ⟫ 
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
-                        odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
+                        odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m us ?
                  ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m  ; asm = MinSUP.asm m
                          ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b))  } where
                     m = ZChain.minsup zc (o≤-refl0 b)
-                    ms00 :  {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
+                    ms00 :  {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
                     ms00 {x} ux = MinSUP.x≤sup m ?
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
-                        odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
+                        odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m us ?
                  ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1
                          ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where
                     m = sup1
-                    ms00 :  {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
+                    ms00 :  {x : Ordinal} → odef (UnionCF A f supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m)
                     ms00 {x} ux = MinSUP.x≤sup m ?
                     ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} →
-                        odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
+                        odef (UnionCF A f supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m us ?
 
 
@@ -1272,7 +1096,7 @@
                  --     supf1 x ≡ supf0 px because of supfmax
 
                  cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
-                     → a o< b → b o≤ x →  supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f mf ay supf0 b) w
+                     → a o< b → b o≤ x →  supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f supf0 b) w
                  cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with trio< b px 
                  ... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) sa<b fc
                  ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl sa<b fc 
@@ -1288,8 +1112,8 @@
                      --      supf a ≡ px    -- a o< px → odef U w
                      --                        a ≡ px → supf px ≡ px → odef U w
 
-                     cfcs0 : a ≡ px → odef (UnionCF A f mf ay supf0 b) w
-                     cfcs0 a=px = ⟪  A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) spx<b cp fc1 ⟫ where
+                     cfcs0 : a ≡ px → odef (UnionCF A f supf0 b) w
+                     cfcs0 a=px = ⟪  A∋fc {A} _ f mf fc , ? ⟫ where
                          spx<b : supf0 px o< b
                          spx<b = subst (λ k → supf0 k o< b) a=px sa<b
                          cs01 : supf0 a ≡ supf0 (supf0 px)
@@ -1297,64 +1121,36 @@
                               (subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ spx<b b≤x))))
                          fc1 : FClosure A f (supf0 (supf0 px)) w
                          fc1 = subst (λ k → FClosure A f k w) cs01 fc
-                         m : MinSUP A (UnionCF A f mf ay supf0 (supf0 px))
+                         m : MinSUP A (UnionCF A f supf0 (supf0 px))
                          m = ZChain.minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x))
                          m=sa : MinSUP.sup m ≡ supf0 (supf0 px)
                          m=sa = begin 
                                 MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc (zc-b<x _ (ordtrans<-≤ spx<b b≤x) ))  ⟩ 
                                 supf0 (supf0 px)  ∎  where open ≡-Reasoning 
-                         cp : ChainP A f mf ay supf0 (supf0 px)
-                         cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m ⟪ A∋fc _ f mf fc , ch-init fc ⟫ )
-                            ; order = order 
-                            ; supu=u = sym (trans (cong supf0 (sym a=px)) cs01) } where
-                             uz : {s z1 : Ordinal } → supf0 s o< supf0 (supf0 px) → FClosure A f (supf0 s) z1 
-                                 → odef (UnionCF A f mf ay supf0 (supf0 px)) z1
-                             uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<spx spx≤px 
-                                         (subst (λ k → supf0 s o< k) (sym (trans (cong supf0 (sym a=px)) cs01) ) ss<sp) fc where
-                                 s<spx : s o< supf0 px
-                                 s<spx = ZChain.supf-inject zc ss<sp 
-                                 spx≤px : supf0 px o≤ px
-                                 spx≤px = zc-b<x _ (ordtrans<-≤ spx<b b≤x)
-                             order : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 (supf0 px) →
-                                    FClosure A f (supf0 s) z1 → (z1 ≡ supf0 (supf0 px)) ∨ (z1 << supf0 (supf0 px))
-                             order {s} {z} s<u fc  = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m (uz s<u fc) )
 
 
-                     cfcs1 : odef (UnionCF A f mf ay supf0 b) w
+                     cfcs1 : odef (UnionCF A f supf0 b) w
                      cfcs1 with trio< a px
                      ... | tri< a<px ¬b ¬c = cfcs2 where
                          sa<x : supf0 a o< x
                          sa<x = ordtrans<-≤ sa<b b≤x
-                         cfcs2 : odef (UnionCF A f mf ay supf0 b) w
+                         cfcs2 : odef (UnionCF A f supf0 b) w
                          cfcs2 with trio< (supf0 a) px
                          ... | tri< sa<x ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) 
                              ( ZChain.cfcs zc mf< a<px o≤-refl sa<x fc ) 
                          ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ sa<x)  ⟫ )
                          ... | tri≈ ¬a sa=px ¬c with trio< a px
-                         ... | tri< a<px ¬b ¬c = ⟪  A∋fc {A} _ f mf fc , ch-is-sup (supf0 a) sa<b cp fc1 ⟫ where
+                         ... | tri< a<px ¬b ¬c = ⟪  A∋fc {A} _ f mf fc , ? ⟫ where
                               cs01 : supf0 a ≡ supf0 (supf0 a)
                               cs01 =  sym ( ZChain.supf-idem zc mf< (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x)))  
                               fc1 : FClosure A f (supf0 (supf0 a)) w
                               fc1 = subst (λ k → FClosure A f k w) cs01 fc
-                              m : MinSUP A (UnionCF A f mf ay supf0 (supf0 a))
+                              m : MinSUP A (UnionCF A f supf0 (supf0 a))
                               m = ZChain.minsup zc (o≤-refl0 sa=px)
                               m=sa : MinSUP.sup m ≡ supf0 (supf0 a)
                               m=sa = begin 
                                     MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc (o≤-refl0 sa=px) )  ⟩ 
                                     supf0 (supf0 a)  ∎  where open ≡-Reasoning 
-                              cp : ChainP A f mf ay supf0 (supf0 a)
-                              cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m ⟪  A∋fc _ f mf fc  , ch-init fc ⟫ )  
-                                ; order = order 
-                                ; supu=u = sym cs01 } where
-                                 uz : {s z1 : Ordinal } → supf0 s o< supf0 (supf0 a) → FClosure A f (supf0 s) z1 
-                                     → odef (UnionCF A f mf ay supf0 (supf0 a)) z1
-                                 uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< (ZChain.supf-inject zc ss<sp) 
-                                         (zc-b<x _ (ordtrans<-≤ sa<b b≤x)) ss<sa fc where
-                                    ss<sa : supf0 s o< supf0 a
-                                    ss<sa = subst (λ k → supf0 s o< k ) (sym cs01) ss<sp 
-                                 order : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 (supf0 a) →
-                                        FClosure A f (supf0 s) z1 → (z1 ≡ supf0 (supf0 a)) ∨ (z1 << supf0 (supf0 a))
-                                 order {s} {z} s<u fc  = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=sa (MinSUP.x≤sup m (uz s<u fc) )
                          ... | tri≈ ¬a a=px ¬c = cfcs0 a=px
                          ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ (ordtrans<-≤ a<b b≤x) )  ⟫ )
                      ... | tri≈ ¬a a=px ¬c = cfcs0 a=px
@@ -1368,26 +1164,12 @@
                       zc177 : supf0 z ≡ supf0 px
                       zc177 = ZChain.supfmax zc px<z  -- px o< z, px o< supf0 px
 
-                 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) z → odef pchainpx z
-                 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
-                 zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc21 fc where
-                    u≤px : u o≤ px
-                    u≤px = zc-b<x _ u<x
-                    zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef pchainpx z1
-                    zc21 {z1} (fsuc z2 fc ) with zc21 fc
-                    ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-                    ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
-                    ... | case2 fc = case2 (fsuc _ fc)
-                    zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) | inspect supf0 u
-                    ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u u<px is-sup (init asp refl ) ⟫ where
-                        u<px :  u o< px
-                        u<px =  ZChain.supf-inject zc a
-                    ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym  b ))
-                    ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫ )
+                 zc11 : {z : Ordinal} → odef (UnionCF A f supf0 x) z → odef pchainpx z
+                 zc11 {z} ⟪ az , cp ⟫ = ? where
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
-                         tsup : MinSUP A (UnionCF A f mf ay supf0 z)
+                         tsup : MinSUP A (UnionCF A f supf0 z)
                          tsup=sup : supf0 z ≡ MinSUP.sup tsup
 
                  sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x
@@ -1400,7 +1182,7 @@
                      ... | case1 eq = eq
                      ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                      zc32 = ZChain.sup zc o≤-refl
-                     zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
+                     zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
                      zc34 ne {w} lt = ?
                      zc33 : supf0 z ≡ & (SUP.sup zc32)
                      zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-minsup zc o≤-refl  )
@@ -1411,10 +1193,10 @@
                      ... | tri< a ¬b ¬c = zc36 ¬b
                      ... | tri> ¬a ¬b c = zc36 ¬b
                      ... | tri≈ ¬a b ¬c = record { tsup = ? ; tsup=sup = ?  } where
-                          zc37 : MinSUP A (UnionCF A f mf ay supf0 z)
+                          zc37 : MinSUP A (UnionCF A f supf0 z)
                           zc37 = record { sup = ? ; asm = ? ; x≤sup = ? ; minsup = ? }
                  sup=u : {b : Ordinal} (ab : odef A b) →
-                    b o≤ x → IsMinSUP A (UnionCF A f mf ay supf0 b) supf0 ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf0 b) f b ) → supf0 b ≡ b
+                    b o≤ x → IsMinSUP A (UnionCF A f supf0 b) supf0 ab ∧ (¬ HasPrev A (UnionCF A f supf0 b) f b ) → supf0 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
                  ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫
                  ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) ⟪ record { x≤sup = λ lt → IsMinSUP.x≤sup (proj1 is-sup) lt } , proj2 is-sup ⟫
@@ -1489,14 +1271,14 @@
           ... | tri> ¬a ¬b c = spu
 
           pchain : HOD
-          pchain = UnionCF A f mf ay supf1 x
+          pchain = UnionCF A f supf1 x
 
           -- pchain ⊆ pchainx
 
           ptotal : IsTotalOrderSet pchain
           ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb))
+               uz01 = ? --  chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb))
 
           sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc  (ob<x lim a)) z  
           sf1=sf {z} z<x with trio< z x
@@ -1533,7 +1315,7 @@
           ... | tri> ¬a ¬b c = ?
 
           cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
-                 → a o< b → b o≤ x →  supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
+                 → a o< b → b o≤ x →  supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f supf1 b) w
           cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x
           ... | case1 b=x with trio< a x 
           ... | tri< a<x ¬b ¬c = zc40 where
@@ -1557,37 +1339,11 @@
                sam<m = subst (λ k → k o< m ) (supf-unique A f mf ay zc42 (pzc (ob<x lim a<x)) (pzc (ob<x lim m<x)) (o<→≤ <-osuc)) ( omax-y _ _ )
                fcm : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) a) w
                fcm = subst (λ k → FClosure A f k w ) (zeq (ob<x lim a<x) (ob<x lim m<x) zc42 (o<→≤ <-osuc) ) fc
-               zcm : odef (UnionCF A f mf ay (ZChain.supf (pzc  (ob<x lim m<x))) (osuc (omax a sa))) w
+               zcm : odef (UnionCF A f (ZChain.supf (pzc  (ob<x lim m<x))) (osuc (omax a sa))) w
                zcm = ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
-               zc40 : odef (UnionCF A f mf ay supf1 b) w
+               zc40 : odef (UnionCF A f supf1 b) w
                zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
-               ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-               ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<b cp fc2 ⟫  where 
-                   zc55 : u o< osuc m
-                   zc55 = u<x
-                   u<b : u o< b 
-                   u<b = subst (λ k → u o< k ) (sym b=x) ( ordtrans u<x (ob<x lim m<x))
-                   fc1m : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) u) w
-                   fc1m = fc1
-                   fc1a : FClosure A f (ZChain.supf (pzc (ob<x lim a<x)) a) w
-                   fc1a = fc
-                   fc2 : FClosure A f (supf1 u) w
-                   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
-                   sb=sa : {a : Ordinal } → a o≤ m → supf1 a ≡ ZChain.supf (pzc (ob<x lim m<x)) a 
-                   sb=sa {a} a≤m = trans (sf1=sf (ordtrans≤-< a≤m m<x)) (zeq _ _ (osucc a≤m) (o<→≤ <-osuc))
-                   cp : ChainP A f mf ay supf1 u
-                   cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (sb=sa u<x)) (ChainP.fcy<sup is-sup fc )  
-                        ; order = order 
-                        ; supu=u = trans (sb=sa u<x ) (ChainP.supu=u is-sup)  } where
-                         order : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u →
-                                FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
-                         order {s} {z} s<u fc  = subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (sb=sa u<x)) 
-                           (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sb=sa s≤m) (sb=sa u<x) s<u)  
-                              (subst (λ k → FClosure A f k z) (sb=sa s≤m ) fc )) where
-                              s≤m : s o≤ m 
-                              s≤m = ordtrans (supf-inject0 supf-mono  s<u ) u<x
+               ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫  
           ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           cfcs mf< {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where
@@ -1597,26 +1353,14 @@
                fcb : FClosure A f (supfb a) w
                fcb = subst (λ k → FClosure A f k w) (sb=sa a<b) fc 
                --  supfb a o< b assures it is in Union b
-               zcb : odef (UnionCF A f mf ay supfb b) w
+               zcb : odef (UnionCF A f supfb b) w
                zcb = ZChain.cfcs (pzc (ob<x lim b<x)) mf< a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb
-               zc40 : odef (UnionCF A f mf ay supf1 b) w
+               zc40 : odef (UnionCF A f supf1 b) w
                zc40 with zcb
-               ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-               ... | ⟪ az , ch-is-sup u u<x is-sup fc1 ⟫ = ⟪ az , ch-is-sup u u<x cp (subst (λ k → FClosure A f k w) (sym (sb=sa u<x)) fc1 ) ⟫ where
-                   cp : ChainP A f mf ay supf1 u
-                   cp = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (sb=sa u<x)) (ChainP.fcy<sup is-sup fc )  
-                        ; order = order
-                        ; supu=u = trans (sb=sa u<x) (ChainP.supu=u is-sup)  } where
-                         order : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u →
-                                FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
-                         order {s} {z} s<u fc  = subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sym (sb=sa u<x)) 
-                           (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sb=sa s<b) (sb=sa u<x) s<u)  
-                              (subst (λ k → FClosure A f k z) (sb=sa s<b ) fc )) where
-                              s<b : s o< b 
-                              s<b = ordtrans (supf-inject0 supf-mono  s<u ) u<x
+               ... | ⟪ az , cp  ⟫ = ⟪ az , ? ⟫ 
 
           sup=u : {b : Ordinal} (ab : odef A b) →
-                b o≤ x → IsMinSUP A (UnionCF A f mf ay supf1 b) supf1 ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) f b ) → supf1 b ≡ b
+                b o≤ x → IsMinSUP A (UnionCF A f supf1 b) supf1 ab ∧ (¬ HasPrev A (UnionCF A f supf1 b) f b ) → supf1 b ≡ b
           sup=u {b} ab b≤x is-sup with osuc-≡< b≤x
           ... | case1 b=x = ? where
                  zc31 : spu o≤ b
@@ -1633,8 +1377,8 @@
 
      msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
          → (zc : ZChain A f mf ay x )
-         → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x)
-     msp0 f mf {x} ay zc = minsupP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) (ZChain.f-total zc)
+         → MinSUP A (UnionCF A f (ZChain.supf zc) x)
+     msp0 f mf {x} ay zc = minsupP (UnionCF A f (ZChain.supf zc) x) (ZChain.chain⊆A zc) (ZChain.f-total zc)
 
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (mf< : <-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
             → (sp1 : MinSUP A (ZChain.chain zc))
@@ -1647,7 +1391,7 @@
            asp : odef A sp
            asp = MinSUP.asm sp1
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< (& A) → (ab : odef A b )
-              →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f mf as0 (ZChain.supf zc) b) ab
+              →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f (ZChain.supf zc) b) ab
               → * a < * b  → odef chain b
            z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl )
            z22 : sp o< & A
@@ -1660,9 +1404,9 @@
                z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne eq )
                ... | case2 lt = lt
-               z19 : IsSUP A (UnionCF A f mf as0 (ZChain.supf zc) sp) asp
+               z19 : IsSUP A (UnionCF A f (ZChain.supf zc) sp) asp
                z19 = record {   x≤sup = z20 }  where
-                   z20 : {y : Ordinal} → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
+                   z20 : {y : Ordinal} → odef (UnionCF A f (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
                    z20 {y} zy with MinSUP.x≤sup sp1
                        (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22)  zy ))
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p )