--- a/src/zorn.agda	Mon Oct 03 01:43:00 2022 +0900
+++ b/src/zorn.agda	Mon Oct 03 12:52:25 2022 +0900
@@ -395,7 +395,7 @@
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
-      x≤supfx : z o≤ supf z
+      x≤supfx : {z : Ordinal } → z o≤ supf z
 
       minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x) 
       supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (M→S supf (minsup x≤z) ))
@@ -1078,6 +1078,15 @@
                                   csupf17 (init as refl ) = ZChain.csupf zc sf<px 
                                   csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
 
+                 x≤supfx1 : {z : Ordinal} → z o≤ supf1 z
+                 x≤supfx1 {z} with trio< z ( supf1 z) --  supf1 x o< x → supf1 x o≤ supf1 px → x o< px ∨ supf1 x ≡ supf1 px
+                 ... | tri< a ¬b ¬c = o<→≤ a
+                 ... | tri≈ ¬a b ¬c = o≤-refl0 b
+                 ... | tri> ¬a ¬b c with osuc-≡< (subst (λ k → supf1 x o< k ) (sym (Oprev.oprev=x op)) ? ) -- c : supf1 x < x     
+                 ... | case2 lt = ?
+                    -- ⊥-elim ( o<> (pxo<x op) (supf-inject0 supf-mono1 ( subst (λ k → supf1 x o< k ) 
+                    --  (trans sfpx=px (sym (sf1=sf0 o≤-refl))) lt )))  -- lt : supf1 x o< px ≡ supf0 px ≡ supf1 px
+                 ... | case1 eq = ? --   supf1 x ≡ px ≡ supf1 px
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
@@ -1095,25 +1104,26 @@
                  ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1  
                          ; x<sup = ? ; minsup = ? } ; tsup=sup = ? } 
 
-
                  csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) 
                  csupf1 {z1} sz1<x with trio< (supf0 z1) px
                  ... | tri< a ¬b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) (sym (sf1=sf0 z1≤px)) (case1 (ZChain.csupf zc a )) where
                         z1≤px : z1 o≤ px
                         z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) sfpx=px a ))
                  ... | tri≈ ¬a b ¬c = subst₂ (λ j k → odef j k ) (sym ch1x=pchainpx) zc20 (case2 (init apx sfpx=px )) where
-                      z1≤px : z1 o≤ px
-                      z1≤px with trio< z1 px
-                      ... | tri< a ¬b ¬c = o<→≤ a
-                      ... | tri≈ ¬a b ¬c = o≤-refl0 b
-                      ... | tri> ¬a ¬b c = ⊥-elim ( o<> c ( supf-inject0 supf-mono1 (subst (λ k → supf1 z1 o< k ) refl ?) ) )
+                      z1≤px : z1 o≤ px -- z1 o≤ supf1 z ≡ px 
+                      z1≤px = subst (λ k → z1 o< k) (cong osuc b ) ( ZChain.x≤supfx zc  )
                       zc20 : supf0 px ≡ supf1 z1 
                       zc20 = begin
-                        supf0 px  ≡⟨ ? ⟩
-                        px  ≡⟨ ? ⟩
-                        supf0 z1  ≡⟨ ? ⟩
+                        supf0 px  ≡⟨ sym sfpx=px ⟩
+                        px  ≡⟨ sym b ⟩
+                        supf0 z1  ≡⟨ sym (sf1=sf0 z1≤px)  ⟩
                         supf1 z1 ∎ where open ≡-Reasoning
-                 ... | tri> ¬a ¬b c = ⊥-elim ( ? )
+                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ zc20 , subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) where
+                      zc21 : px o< z1
+                      zc21 =  ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) sfpx=px c  )
+                      zc20 : px o< supf1 z1
+                      zc20 = ordtrans<-≤ zc21 x≤supfx1
+                     -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x
 
           ... | case2 px<spfx = ? where