# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665831260 -32400
# Node ID 4d99a1306f408c660ba02e6fc9464124162c87e9
# Parent  f0b98f57ec650186dd9c10bb37a45be5ff39c2f5
roll back

diff -r f0b98f57ec65 -r 4d99a1306f40 src/zorn.agda
--- a/src/zorn.agda	Thu Oct 13 17:47:19 2022 +0900
+++ b/src/zorn.agda	Sat Oct 15 19:54:20 2022 +0900
@@ -407,7 +407,7 @@
 
       minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x) 
       supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
-      csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
+      csupf : {b : Ordinal } → b o< z → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
 
    chain : HOD
    chain = UnionCF A f mf ay supf z
@@ -601,14 +601,14 @@
 
         supf = ZChain.supf zc
 
-        csupf-fc : {b s z1 : Ordinal} → b o≤ & A → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
-        csupf-fc {b} {s} {z1} b≤z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
+        csupf-fc : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
+        csupf-fc {b} {s} {z1} b<z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
                 s<b : s o< b
                 s<b = ZChain.supf-inject zc ss<sb
-                s≤<z : s o≤ & A
-                s≤<z = ordtrans s<b b≤z
+                s<z : s o< & A
+                s<z = ordtrans s<b b<z
                 zc04 : odef (UnionCF A f mf ay supf (& A))  (supf s)
-                zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc))
+                zc04 = ZChain.csupf zc s<z (z09 (ZChain.asupf zc))
                 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
                 zc05 with zc04
                 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
@@ -624,10 +624,11 @@
                 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb 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) ⟫ 
+
         order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
         order {b} {s} {z1} b<z ss<sb fc = zc04 where
           zc00 : ( z1  ≡  MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1  << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) )
-          zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤  b<z) ) (subst (λ k →  odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc (o<→≤ b<z) ss<sb fc ))
+          zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤  b<z) ) (subst (λ k →  odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc b<z ss<sb fc ))
           -- supf (supf b) ≡ supf b
           zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
           zc04 with zc00
@@ -796,8 +797,10 @@
           zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
+          opx=x : osuc px ≡ x
+          opx=x = Oprev.oprev=x 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 lt = subst (λ k → b o< k ) (sym opx=x) lt 
 
           supf0 = ZChain.supf zc
           pchain  : HOD
@@ -812,7 +815,7 @@
           ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b)
           ... | tri> ¬a ¬b px<b with osuc-≡< b≤x
           ... | case1 eq = case2 eq
-          ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ ) 
+          ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym opx=x) b<x  ⟫ ) 
 
           zc41 : supf0 px o< x →  ZChain A f mf ay x 
           zc41 sfpx<x =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
@@ -945,7 +948,7 @@
                         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<→≤ a)) ( ChainP.fcy<sup is-sup fc )
                     ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) (cong supf0 b) asp ) (cong supf0 (sym b)) )
-                    ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫ )
+                    ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym opx=x) 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
@@ -955,7 +958,7 @@
                         ... | ⟪ 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)) 
+                             (subst (λ k → u o< k) opx=x (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
                             zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u →
                                   FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
@@ -992,7 +995,7 @@
                         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 )
+                        zc21 (init asp refl ) with  osuc-≡< ( subst (λ k → supf0 px o< k ) (sym opx=x) sfpx<x )
                         ... | 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
@@ -1004,7 +1007,7 @@
                               zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
                                     FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
                               zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx 
-                                     (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where
+                                     (MinSUP.x<sup mins (zc18 (fcup fc (o<→≤ s<px) )) ) where
                                   mins : MinSUP A (UnionCF A f mf ay supf0 px)
                                   mins = ZChain.minsup zc o≤-refl
                                   mins-is-spx : MinSUP.sup mins ≡ supf1 px 
@@ -1013,28 +1016,35 @@
                                   s<px = supf-inject0 supf1-mono ss<spx
                                   sf<px : supf0 s o< px
                                   sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx
-                                  csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
-                                  csupf17 (init as refl ) = ZChain.csupf zc sf<px 
-                                  csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
-
-                        ... | 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
-                                 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)
-                                 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))) 
-                                     (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)
-                                       lt0 : supf0 s o< supf0 u
-                                       lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u≤x)) lt
-                                 z12 : supf1 u ≡ u
-                                 z12 = trans (sf1=sf0 (o<→≤ u≤x)) (ChainP.supu=u is-sup)
+                                  zc18 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
+                                  zc18 (init as refl ) = ZChain.csupf zc s<px sf<px 
+                                  zc18 (fsuc x fc) = ZChain.f-next zc (zc18 fc)
+                        ... | case2 sfpx<px = ⟪ ZChain.asupf zc , ch-is-sup (supf1 px) (subst (λ k → k o< x) (sym (sf1=sf0 o≤-refl)) sfpx<x )
+                              record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans  supu=u (sf1=sf0 o≤-refl)) ) ⟫  where
+                                  minsfpx : MinSUP A (UnionCF A f mf ay supf0 (supf1 px))
+                                  minsfpx = ZChain.minsup zc (o<→≤ (subst (λ k → k o< px) (sym (sf1=sf0 o≤-refl)) sfpx<px))
+                                  mins : MinSUP A (UnionCF A f mf ay supf0 px)
+                                  mins = ZChain.minsup zc o≤-refl
+                                  mins-is-spx : MinSUP.sup mins ≡ supf1 px 
+                                  mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl ))
+                                  supu=u : supf1 (supf1 px) ≡ supf1 px
+                                  supu=u with osuc-≡< (supf1-mono (o<→≤ sfpx<px))
+                                  ... | case1 eq = trans (cong supf1 (sf1=sf0 o≤-refl) ) eq
+                                  ... | case2 ss<sfpx = ? where
+                                      zc30 : supf1 px o< px
+                                      zc30 = subst (λ k → k o< px) (sym (sf1=sf0 o≤-refl )) sfpx<px 
+                                      zc32 : supf1 (supf0 px) ≡ supf0 (supf1 px)
+                                      zc32 = trans (sf1=sf0 (subst (λ k → supf0 px o< k) (sym opx=x)  sfpx<x) ) 
+                                          ( cong supf0 (sym (sf1=sf0 o≤-refl ) ) )
+                                      zc31 : supf0 (supf1 px) o< px
+                                      zc31 = subst (λ k → k o< px ) zc32 ( ordtrans ss<sfpx (subst (λ k → k o< px ) 
+                                         (sym (sf1=sf0 o≤-refl ))  sfpx<px ))
+                                      cs05 : odef (UnionCF A f mf ay supf0 px) (supf0 (supf1 px)) 
+                                      cs05 = ZChain.csupf zc zc30 zc31
+                                      cs06 : supf1 (supf1 px) ≡ supf1 px
+                                      cs06 with cs05
+                                      ... | ⟪ ua1 , ch-init fc ⟫ = ?
+                                      ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fcp ⟫ = ?
 
 
 
@@ -1070,21 +1080,19 @@
                         odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m ? ?
 
-                 csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
-                 csupf1 {z1} sz1<x = csupf2 where
+                 csupf1 : {z1 : Ordinal } → z1 o< x → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
+                 csupf1 {z1} z1<x sz1<x = csupf2 where
                      --  z1 o< px → supf1 z1 ≡ supf0 z1
                      --  z1 ≡ px , supf0 px o< px   .. px o< z1, x o≤ z1 ...  supf1 z1 ≡ sp1
                      --  z1 ≡ px , supf0 px ≡  px
                      psz1≤px :  supf1 z1 o≤ px
-                     psz1≤px =  subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x 
-                     cs01 : supf0 px o< px → odef (UnionCF A f mf ay supf0 px) (supf0 px)
-                     cs01 spx<px = ZChain.csupf zc spx<px
+                     psz1≤px =  subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x 
                      csupf2 :  odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
                      csupf2 with  trio< z1 px | inspect supf1 z1
                      csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px
                      ... | case2 lt  = zc12 (case1 cs03)  where
                            cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1)
-                           cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
+                           cs03 = ZChain.csupf zc a (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt )
                      ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) )
                      ... | case1 sfz=sfpx =  zc12 (case2 (init (ZChain.asupf zc) cs04 )) where
                            supu=u : supf1 (supf1 z1) ≡ supf1 z1
@@ -1100,33 +1108,9 @@
                            cs05 : px o< supf0 px
                            cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx
                            cs06 : supf0 px o< osuc px
-                           cs06 = subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x 
+                           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 } 
-                       = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x)
-                              record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where 
-                           supu=u : supf1 (supf1 z1) ≡ supf1 z1
-                           supu=u = ?
-                           sp1≤px : sp1 o≤ px
-                           sp1≤px with trio< sp1 px
-                           ... | tri< a ¬b ¬c = o<→≤ a
-                           ... | tri≈ ¬a b ¬c = o≤-refl0 b
-                           ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x  ⟫ )
-
-                     -- with trio< sp1 px
-                     -- ... | tri< sp1<px ¬b ¬c = ? --  supf1 z1 = sp1 o< px o< z1 
-                     -- ... | tri≈ ¬a sp1=px ¬c = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x)
-                     --         record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where 
-                     --      --  supf1 z1 ≡ sp1, px o< z1, sp1 o< x  -- sp1 o< z1
-                     --      --  supf1 sp1 o≤ supf1 z1 ≡ sp1 o< z1
-                     --      asm : odef A (supf1 z1)
-                     --      asm =  subst (λ k → odef A k ) (sym (sf1=sp1 px<z1)) ( MinSUP.asm sup1) 
-                     --      cs05 : odef (UnionCF A f mf ay supf1 x) (supf1 sp1) 
-                     --      cs05 = zc12 (case2 (init (ZChain.asupf zc) ( begin
-                     --         supf0 px ≡⟨ sym (sf1=sf0 o≤-refl )  ⟩
-                     --        supf1 px ≡⟨ cong supf1 (sym sp1=px)  ⟩
-                     --       supf1 sp1 ∎  ))) where open ≡-Reasoning
-                     --... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<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 
           zc4 with trio< x (supf0 px)
@@ -1189,13 +1173,13 @@
                  zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = ⊥-elim (¬sp=x zcsup) where
                         eq : u1 ≡ x 
                         eq with trio< u1 x
-                        ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ )
+                        ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym opx=x) a ⟫ )
                         ... | tri≈ ¬a b ¬c = b
                         ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x ? )
                         s1u=x : supf0 u1 ≡ x
                         s1u=x = trans ? eq
                         zc13 : osuc px o< osuc u1
-                        zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) ) 
+                        zc13 = o≤-refl0 ( trans opx=x (sym eq ) ) 
                         x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
                         x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
                         x<sup {w} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u≤x) ? ))
@@ -1205,7 +1189,7 @@
                                     u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩ 
                                     supf0 u ≡⟨ ? ⟩ 
                                     supf0 u1 ≡⟨ s1u=x ⟩ 
-                                    x ≡⟨ sym (Oprev.oprev=x op) ⟩ 
+                                    x ≡⟨ sym opx=x ⟩ 
                                     osuc px ∎ where open ≡-Reasoning
                         ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
                         zc12 : supf0 x ≡ u1
@@ -1216,7 +1200,7 @@
                  zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 ? where
                         eq : u1 ≡ x 
                         eq with trio< u1 x
-                        ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ )
+                        ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym opx=x) a ⟫ )
                         ... | tri≈ ¬a b ¬c = b
                         ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x ? )
                         zc20 : {z : Ordinal} → FClosure A f (supf0 u1) z → OD.def (od pchain) z
@@ -1244,7 +1228,7 @@
                      zc30 : z ≡ x
                      zc30 with osuc-≡< z≤x
                      ... | case1 eq = eq
-                     ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
+                     ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym opx=x) 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 ne {w} lt with zc11 ? ⟪ proj1 lt , ? ⟫
@@ -1270,7 +1254,7 @@
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
                      ... | case1 eq = sym (eq)
-                     ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
+                     ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym opx=x) b<x ⟫ )
                      zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
                      zcsup with zc30
                      ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt →