# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665882594 -32400
# Node ID 213f12f27003b35fe01901794298e33a1c03e831
# Parent  4c33f8383d7dda0e4c645beae3e2a06ad5ff2f2a
supf u o< supf x

diff -r 4c33f8383d7d -r 213f12f27003 src/zorn.agda
--- a/src/zorn.agda	Sat Oct 15 20:05:34 2022 +0900
+++ b/src/zorn.agda	Sun Oct 16 10:09:54 2022 +0900
@@ -262,7 +262,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 : supf u o< supf 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
 
 --
@@ -386,12 +386,12 @@
 
 
 chain-mono : {A : HOD}  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) 
-   {a b c : Ordinal} → a o≤ b
+   (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 {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ = 
+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 {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  ⟫ 
+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 (supf-mono a≤b ) ) is-sup fc  ⟫ 
 
 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
@@ -460,7 +460,7 @@
         {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) 
+      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → supf b o< supf z  → (ab : odef A b) 
           → HasPrev A (UnionCF A f mf ay supf z) b f ∨  IsSup A (UnionCF A f mf ay supf z) ab  
           → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
 
@@ -589,9 +589,9 @@
      SZ1 f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x 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
-        chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) a≤b
+        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 →
-            b o< x → (ab : odef A b) →
+            ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f → 
             * 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
@@ -612,7 +612,7 @@
                 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
                 zc05 with zc04
                 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
-                ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u (ZChain.supf-inject zc zc08) is-sup fc ⟫ where
+                ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u zc08 is-sup fc ⟫ where
                     zc07 : FClosure A f (supf u) (supf s)   -- supf u ≤ supf s  → supf u o≤ supf s
                     zc07 = fc
                     zc06 : supf u ≡ u
@@ -638,18 +638,20 @@
         zc1 x prev with Oprev-p x  -- prev is not used now....
         ... | yes op = record { is-max = is-max } where
            px = Oprev.oprev op
-           zc-b<x : {b : Ordinal } → b o< x → b o< osuc px
-           zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
+           zc-b<x : {b : Ordinal } → ZChain.supf zc b o< ZChain.supf zc x → b o< osuc px
+           zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt  )
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
-              b o< x → (ab : odef A b) →
+              ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
               * a < * b → odef (UnionCF A f mf ay 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 b<x ab has-prev a<b 
-           is-max {a} {b} ua b<x ab P a<b | case2 is-sup 
-             = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+           is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup 
+             = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
               b<A : b o< & A
               b<A = z09 ab
+              b<x : b o< x
+              b<x  = ZChain.supf-inject zc sb<sx
               m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
               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 } )
@@ -665,16 +667,18 @@
               m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
-              b o< x → (ab : odef A b) →
+              ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
               * a < * b → odef (UnionCF A f mf ay 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 b<x 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 )
+           is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P
+           is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua sb<sx ab has-prev a<b 
+           is-max {a} {b} ua sb<sx 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 ))  ⟫
-           ... | case2 y<b = ⟪ ab , ch-is-sup b b<x m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+           ... | case2 y<b = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
               m09 : b o< & A
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
+              b<x : b o< x 
+              b<x  = ZChain.supf-inject zc sb<sx
               m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
               m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
               m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
@@ -700,12 +704,12 @@
            supf = ZChain.supf zc
            sp1 : SUP A chain
            sp1 = sp0 f mf as0 zc 
-           z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) 
+           z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) 
               →  HasPrev A chain b f ∨  IsSup A chain {b} ab 
               → * a < * b  → odef chain b
            z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
-           z21 : & (SUP.sup sp1) o< & A
-           z21 = c<→o< (SUP.as sp1 )
+           z21 : supf (& (SUP.sup sp1)) o< supf (& A)
+           z21 = ?
            -- z21 : supf (& (SUP.sup sp1)) o< & A
            -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) ))
            z12 : odef chain (& (SUP.sup sp1))
@@ -907,7 +911,7 @@
                        zc21 : MinSUP A (UnionCF A f mf ay 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₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o<→≤ a<px) ux ) )
+                       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
@@ -916,7 +920,7 @@
                        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₁} ux = MinSUP.x<sup sup1 (case1 (chain-mono f mf ay supf0 (o≤-refl0 b) ux ) )
+                       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 )
                  ... | tri> ¬a ¬b c = o≤-refl
@@ -928,14 +932,16 @@
                  fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc
                  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
+                 zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where
+                    u<x :  u o< x
+                    u<x = ?
                     zc21 : {z1 : Ordinal } → FClosure A f (supf1 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< u px | inspect supf1 u
-                    ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17
+                    ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u ? record {fcy<sup = zc13 ; order = zc17
                          ; supu=u = trans (sym (sf1=sf0 (o<→≤ a))) (ChainP.supu=u is-sup) } (init asp refl) ⟫ where
                         zc17 :  {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u →
                             FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
@@ -951,26 +957,28 @@
                     ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫ )
                  zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
                  zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
-                 zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = zc21 fc where
+                 zc12 {z} (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where
+                        u<x :  u o< x
+                        u<x = ?
                         zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef (UnionCF A f mf ay supf1 x) z1
                         zc21 {z1} (fsuc z2 fc ) with zc21 fc
                         ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                         ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ 
                         zc21 (init asp refl ) with trio< u px | inspect supf1 u
                         ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u 
-                             (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc)) 
-                                record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 (o<→≤ u<x)) (ChainP.supu=u is-sup) } zc14 ⟫  where
+                             ?  
+                                record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup) } zc14 ⟫  where
                             zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u →
                                   FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
-                            zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ u<x))) ( ChainP.order is-sup 
-                               (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u<x)) ss<spx) (fcup fc s≤px) ) where
+                            zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ ?))) ( ChainP.order is-sup 
+                               (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ ?)) ss<spx) (fcup fc s≤px) ) where
                                   s≤px : s o≤ px
-                                  s≤px = ordtrans ( supf-inject0 supf1-mono ss<spx ) (o<→≤ u<x)
+                                  s≤px = ? -- ordtrans ( supf-inject0 supf1-mono ss<spx ) (o<→≤ u<x)
                             zc14 : FClosure A f (supf1 u) (supf0 u)
-                            zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 (o<→≤ u<x))) asp) (sf1=sf0 (o<→≤ u<x))
+                            zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 ?)) asp) (sf1=sf0 ?)
                             zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
-                            zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u<x))) ( ChainP.fcy<sup is-sup fc )
-                        ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px (pxo<x op) record { fcy<sup = zc13 
+                            zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) ( ChainP.fcy<sup is-sup fc )
+                        ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px ? record { fcy<sup = zc13 
                               ; order = zc17 ; supu=u = zc18   } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b)))  ) ⟫ where
                             zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px )
                             zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc )
@@ -989,14 +997,14 @@
                                 zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b))
                                 s≤px : s o≤ px
                                 s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx)
-                        ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , o<→≤ u<x  ⟫ )
+                        ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , ?  ⟫ )
                  zc12 {z} (case2 fc) = zc21 fc where
                         zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1
                         zc21 {z1} (fsuc z2 fc ) with zc21 fc
                         ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                         ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ 
                         zc21 (init asp refl ) with  osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x )
-                        ... | case1 sfpx=px =  ⟪ asp , ch-is-sup px (pxo<x op)
+                        ... | case1 sfpx=px =  ⟪ asp , ch-is-sup px ? -- (pxo<x op)
                                      record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
                               zc15 : supf1 px ≡ px
                               zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px)
@@ -1022,22 +1030,22 @@
 
                         ... | case2 sfp<px  with ZChain.csupf zc sfp<px --  odef (UnionCF A f mf ay supf0 px) (supf0 px)
                         ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ 
-                        ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u (ordtrans u≤x px<x) 
-                              record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ (o<→≤ u≤x) ) ⟫  where
+                        ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u ?  
+                              record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ ? ) ⟫  where
                                  z10 :  {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) 
-                                 z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u≤x))) (ChainP.fcy<sup is-sup fc)
+                                 z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) (ChainP.fcy<sup is-sup fc)
                                  z11  : {s z1 : Ordinal} → (lt : supf1 s o< supf1 u ) → FClosure A f (supf1 s ) z1 
                                       → (z1 ≡ supf1 u ) ∨ ( z1 << supf1 u )
-                                 z11 {s} {z} lt fc  = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u≤x))) 
+                                 z11 {s} {z} lt fc  = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) 
                                      (ChainP.order is-sup lt0 (fcup fc s≤px )) where
                                        s<u : s o< u
                                        s<u = supf-inject0 supf1-mono lt
                                        s≤px : s o≤ px
-                                       s≤px = ordtrans s<u (o<→≤ u≤x)
+                                       s≤px = ordtrans s<u ? -- (o<→≤ u≤x)
                                        lt0 : supf0 s o< supf0 u
-                                       lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u≤x)) lt
+                                       lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ? ) lt
                                  z12 : supf1 u ≡ u
-                                 z12 = trans (sf1=sf0 (o<→≤ u≤x)) (ChainP.supu=u is-sup)
+                                 z12 = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup)
 
 
 
@@ -1103,7 +1111,8 @@
                            cs06 : supf0 px o< osuc px
                            cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) sfpx<x 
                      csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } =  zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b))))
-                     csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ )
+                     csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? 
+                     -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ )
 
 
           zc4 : ZChain A f mf ay x     --- x o≤ supf px