# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659510291 -32400
# Node ID f4450bc95699c1ebef55060a4116b43a10f9eca8
# Parent  201b66da4e690ffeaba619f440a4b04e87e05903
...

diff -r 201b66da4e69 -r f4450bc95699 src/zorn.agda
--- a/src/zorn.agda	Wed Aug 03 02:50:13 2022 +0900
+++ b/src/zorn.agda	Wed Aug 03 16:04:51 2022 +0900
@@ -284,7 +284,7 @@
 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 ) 
+    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
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -308,16 +308,16 @@
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
 
-      sup : {x : Ordinal } → x o< z  → SUP A (UnionCF A f mf ay supf x)
-      supf-is-sup : {x : Ordinal } → (x<z : x o< z) → supf x ≡ & (SUP.sup (sup x<z) )
+      sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
+      supf-is-sup : {x : Ordinal } → (x<z : x o≤ z) → supf x ≡ & (SUP.sup (sup x<z) )
       sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
       csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
       supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
    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 SUP.x<sup (sup u<z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
+   fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ 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 ) ⟫ 
-   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u<z ) ) ))
-   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u<z ))) ) lt )
+   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
+   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
    order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
    order {b} {s} {z1} b<z sf<sb fc = zc04 where
         zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
@@ -334,18 +334,18 @@
             zc03 : odef (UnionCF A f mf ay supf b)  (supf s)
             zc03 with csupf (o<→≤ s<z) 
             ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
-            ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u<x (osucc s<b)) is-sup fc ⟫ 
+            ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ordtrans u≤x (osucc s<b)) is-sup fc ⟫ 
         zc01  (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
             zc04 : odef (UnionCF A f mf ay supf b) (f x)
             zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 fc  )
             ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ 
-            ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u<x is-sup (fsuc _ fc) ⟫ 
-        zc00 : ( * z1  ≡  SUP.sup (sup b<z )) ∨ ( * z1  < SUP.sup ( sup b<z ) )
-        zc00 = SUP.x<sup (sup b<z) (zc01 fc )
+            ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ 
+        zc00 : ( * z1  ≡  SUP.sup (sup (o<→≤ b<z) )) ∨ ( * z1  < SUP.sup ( sup (o<→≤ b<z) ) )
+        zc00 = SUP.x<sup (sup (o<→≤ b<z)) (zc01 fc )
         zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
         zc04 with zc00
-        ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup  b<z ) ) (cong (&) eq) )
-        ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (supf-is-sup b<z ) )))  lt )
+        ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup  (o<→≤ b<z) ) ) (cong (&) eq) )
+        ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (supf-is-sup (o<→≤ b<z) ) )))  lt )
 
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
@@ -368,7 +368,7 @@
 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
+     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
@@ -376,14 +376,14 @@
      ... | 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
+     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
+     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
           ct00 : * a ≡ * b
@@ -391,7 +391,7 @@
      ... | 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
+     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 
@@ -513,9 +513,9 @@
             * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
         is-max-hp x {a} {b} ua b<x 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 , 
+        ... | ⟪ 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))  ⟫ 
+                      (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫ 
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
         ... | yes op = record { is-max = is-max } where
@@ -642,7 +642,7 @@
      ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay) 
 
      inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
-     inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy  ; sup = sup ; supf-is-sup =  λ b<0 → ⊥-elim (¬x<0 b<0)
+     inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy  ; sup = ? ; supf-is-sup = ? 
       ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; supf-mono = mono ; csupf = csupf } where
           spi =  & (SUP.sup (ysup f mf ay))
           isupf : Ordinal → Ordinal
@@ -658,11 +658,11 @@
           isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
           isy {z} ⟪ az , uz ⟫ with uz 
           ... | ch-init fc = s≤fc y f mf fc 
-          ... | ch-is-sup u u<x is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup)  (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc )
+          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup)  (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc )
           inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
           inext {a} ua with (proj2 ua)
           ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua))  , ch-init (fsuc _ fc )  ⟫
-          ... | ch-is-sup u u<x is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) ,  ch-is-sup u u<x is-sup (fsuc _ fc) ⟫
+          ... | ch-is-sup u u≤x is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) ,  ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
           itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 
           itotal {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) )
@@ -713,11 +713,11 @@
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-          pnext {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u ? is-sup (fsuc _ fc ) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u ? is-sup (fsuc _ fc ) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {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
+          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
                zc7 : y <= (ZChain.supf zc) u 
                zc7 = ChainP.fcy<sup is-sup (init ay refl)
           pcy : odef pchain y
@@ -727,25 +727,50 @@
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
-          --  (¬ odef (UnionCF A f mf ay supf0 z) (supf0 px)) ∨ (supf0 px is sup of UnionCF px )
+          --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 
           no-extension : ZChain A f mf ay x
-          no-extension = record { supf = supf0 ; supf-mono = ZChain.supf-mono zc ; sup = sup
-               ; initial = pinit ; chain∋init = pcy  ; sup=u = {!!} ; supf-is-sup = ? ; csupf = ? 
-              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }  where
-                 sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf0 z)
-                 sup {z} z<x with trio< z px
-                 ... | tri< a ¬b ¬c = ZChain.sup zc a
-                 ... | tri> ¬a ¬b c = ⊥-elim (¬p<x<op ⟪ c , subst (λ k → z o< k) (sym (Oprev.oprev=x op)) z<x ⟫ )  --   px < z < x
-                 ... | tri≈ ¬a b ¬c = record { sup = * (supf0 px) ; A∋maximal = subst (λ k → odef A k ) (sym &iso) (proj1 zc8) ; x<sup = x<sup } where
-                     zc9 : SUP A (UnionCF A f mf ay supf0 x)
-                     zc9 = supP pchain  pchain⊆A ptotal
-                     zc8 : odef (UnionCF A f mf ay supf0 z) (supf0 px)
-                     zc8 = subst (λ k → odef (UnionCF A f mf ay supf0 z) k ) (cong supf0 b)  (ZChain.csupf zc (subst (λ k → z o≤ k) b o≤-refl ))
-                     x<sup' :  {w : HOD} → UnionCF A f mf ay supf0 x ∋ w → (w ≡  (SUP.sup zc9) ) ∨ (w < (SUP.sup zc9) )
-                     x<sup' {q} uw = SUP.x<sup zc9 uw
-                     x<sup :  {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ * (supf0 px) ) ∨ (w < * (supf0 px) )
-                     x<sup {w} ⟪ aw , ch-init fc ⟫ = ?
-                     x<sup {w} ⟪ aw , ch-is-sup u u≤z is-sup fc ⟫ = ?
+          no-extension = record { supf = supf1 ; supf-mono = ? ; sup = sup
+               ; initial = ? ; chain∋init = ?  ; sup=u = {!!} ; supf-is-sup = ? ; csupf = ? 
+              ;  chain⊆A = ? ;  f-next = ? ;  f-total = ? }  where
+                 sup1 : SUP A (UnionCF A f mf ay supf0 x)
+                 sup1 = supP pchain pchain⊆A ptotal
+                 sp1 = & (SUP.sup sup1 )
+                 supf1 : Ordinal → Ordinal
+                 supf1 z with trio< z px
+                 ... | tri< a ¬b ¬c = ZChain.supf zc z
+                 ... | tri≈ ¬a b ¬c = ZChain.supf zc z
+                 ... | tri> ¬a ¬b c = sp1
+                 UnionCF⊆ : UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay supf0 x 
+                 UnionCF⊆ ⟪ as , ch-init fc ⟫ = UnionCF⊆ ⟪ as , ch-init fc ⟫ 
+                 UnionCF⊆ ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = o1  }  fc ⟫ with trio< u px
+                 ... | tri< a ¬b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 } fc ⟫  where
+                     order1 :  {s z1 : Ordinal} → supf1 s o< supf0 u → FClosure A f (supf1 s) z1 
+                        → (z1 ≡ supf0 u) ∨ (z1 << (supf0 u))
+                     order1 {s} {z1} = o1 {s} {z1}
+                     order0 : {s z1 : Ordinal}  → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 
+                        → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
+                     order0 {s} {z1} with trio< s px
+                     ... | tri< a ¬b ¬c = o1 {s} {z1}
+                     ... | tri≈ ¬a b ¬c = o1 {s} {z1}
+                     ... | tri> ¬a ¬b c = ?
+                 ... | tri≈ ¬a b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = ? } fc ⟫ 
+                 ... | tri> ¬a ¬b c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = fcy<sup ; order = order } fc0 ⟫  where
+                     --    px o< u , u o< osuc x → u ≡ x
+                     --    supf0 x ≡ sp1 ≡ x
+                     --         u≤x → supf0 u < x
+                     fc1 :  FClosure A f sp1 z
+                     fc1 = fc
+                     fc0 :  FClosure A f (supf0 u) z
+                     fc0 = ?
+                     fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u) ∨ (z << supf0 u)
+                     fcy<sup {z} fc = ?
+                     order : {s z1 : Ordinal}  → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
+                     order = ?
+                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
+                 sup {z} z≤x with trio< z px
+                 ... | tri< a ¬b ¬c = ? -- ZChain.sup zc (o<→≤ a)
+                 ... | tri≈ ¬a b ¬c = ? -- ZChain.sup zc (o≤-refl0 b)
+                 ... | tri> ¬a ¬b c = ? --  sp1
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* px)
@@ -844,11 +869,11 @@
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-init (fsuc _ fc) ⟫
-          pnext {a} ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u ? is-sup (fsuc _ fc) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u ? is-sup (fsuc _ fc) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {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
+          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
                zc7 : y <= psupf _
                zc7 = ChainP.fcy<sup is-sup (init ay refl)
           pcy : odef pchain y
@@ -864,7 +889,7 @@
                 * a < * b → odef (UnionCF A f mf ay supf x) b
           is-max-hp supf x {a} {b} ua b<x 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 , 
+          ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , 
                      subst (λ k → UChain A f mf ay supf x k )
                           (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u ? is-sup (fsuc _ fc))  ⟫