--- a/src/zorn.agda	Fri Dec 09 11:10:41 2022 +0900
+++ b/src/zorn.agda	Fri Dec 09 11:38:13 2022 +0900
@@ -475,6 +475,12 @@
    ... | case2 lt = lt
    ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) 
 
+   supfeq : {a b : Ordinal } → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b 
+   supfeq = ?
+
+   unioneq : {a b : Ordinal } → z o≤ supf a → supf a o≤ supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b 
+   unioneq = ?
+
    -- 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
 
@@ -1189,47 +1195,20 @@
                      ... | tri≈ ¬a b ¬c = o≤-refl0 b
                      ... | 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
-                     spx<x : supf0 px o< x
-                     spx<x = ?
-                     spx<=sb : supf0 px ≤ sp1
-                     spx<=sb = MinSUP.x≤sup sup1 (case2 ⟪ init (ZChain.asupf zc) refl , ? ⟫ )
-                     sa<<sb : supf1 a << supf1 b
-                     sa<<sb with osuc-≡< b≤x
-                     ... | case2 b<x = subst₂ (λ j k → j << k ) (sym (sf1=sf0 ?)) (sym (sf1=sf0 ?)) ( ZChain.supf-mono< zc (zc-b<x _ b<x) 
-                         (subst₂ (λ j k → j o< k) (sf1=sf0 ?) (sf1=sf0 ?)  sa<sb ))
-                     ... | case1 b=x with osuc-≡< ( supf1-mono a≤px )   --   supf1 a ≤ supf1 px << sp1
-                     ... | case2 sa<spx = subst₂ (λ j k → j << k ) (sym (sf1=sf0 ?)) (sym (sf1=sp1 ?))
-                        ( ftrans<-≤ ( ZChain.supf-mono< zc o≤-refl (subst₂ (λ j k → j o< k) (sf1=sf0 ?) (sf1=sf0 ?) sa<spx)) spx<=sb )
-                     ... | case1 sa=spx with spx<=sb
-                     ... | case2 lt = subst₂ (λ j k → j << k ) ? ? lt
-                     ... | case1 eq = ?
-                     -- supf1 a o≤ x
-                     --    x o< supf1 a o< supf1 b -> UnionCF px ⊆ UnionCF a → supf0 px ≡ supf0 a → ⊥
-                     --    a o≤ supf1 a
-                     sa<x : supf1 a o< x    -- supf1 a o< supf1 x ≡ sp1 ( supf of fc (supf0 px) ∧ (supf0 px o< x)
-                     sa<x with x<y∨y≤x (supf1 a) x
-                     ... | case1 lt = lt
-                     ... | case2 x≤sa = ⊥-elim ( <<-irr z27 sa<<sb ) where
-                          z27 : supf1 b ≤ supf1 a
-                          z27 = subst (λ k → supf1 b ≤ k ) ? (IsMinSUP.x≤sup (is-minsup ? ) ? )
-                     ssa=sa : supf1 a ≡ supf1 (supf1 a)   -- supf0 a o≤ px
-                     ssa=sa = sym ( sup=u ? ? ? )
-                     sa<b : supf1 a o< b  -- supf1 (supf1 a) ≡ supf1 a o< supf1 b  → inject supf1 a o< b
-                     sa<b = supf-inject0 supf1-mono (subst (λ k → k o< supf1 b ) ? sa<sb )
                      z20 : w ≤ supf1 b
                      z20 with trio< b px
                      ... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb) 
                           (fcup fc (o<→≤ (ordtrans a<b b<px))) 
                      ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26  where 
-                          -- sa<b : supf1 a o< b  -- px
-                          -- sa<b = ?
                           z26 : odef ( UnionCF A f ay supf0 b ) w 
-                          z26 with cfcs a<b b≤x sa<b fc  
+                          z26 with x<y∨y≤x (supf1 a) b
+                          ... | case2 b≤sa = ?
+                          ... | case1 sa<b with cfcs a<b b≤x sa<b fc  
                           ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ 
                           ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u ? ? ? ⟫ 
-                     ... | tri> ¬a ¬b px<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc))) 
-                          -- sa<b : supf1 a o< b   --  b ≡ x
-                          -- sa<b = ?
+                     ... | tri> ¬a ¬b px<b with x<y∨y≤x (supf1 a) b
+                     ... | case1 sa<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc))) 
+                     ... | case2 b≤sa = ? -- x=b  x o≤ sa   UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥
 
      ... | no lim with trio< x o∅
      ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )