# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657897427 -32400
# Node ID d76047a8a89b65e96dcc5bf9c338a2b8c37d06c7
# Parent  b0cad3ec7da08ea684ebab3fb02ff37a98eaed62
...

diff -r b0cad3ec7da0 -r d76047a8a89b src/zorn.agda
--- a/src/zorn.agda	Fri Jul 15 21:39:32 2022 +0900
+++ b/src/zorn.agda	Sat Jul 16 00:03:47 2022 +0900
@@ -741,16 +741,18 @@
               zc12 = ⟪ ab , record { u = UChain.u (proj2 za) ;  u<x = ? ; uchain = ? } ⟫
               -- ZChain.is-max (uzc za) ? ? ab (subst (λ k → HasPrev A k ab f ∨  IsSup A k ab ) cheq P)  a<b 
 
-          chain-mono : pchain ⊆'  UnionCF A f mf ay psupf x  
-          chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  ; u<x = UChain.u<x (proj2 za) ; uchain = zc11 }  ⟫ where
+          chain-mono : {x1 : Ordinal } → x1 o≤ x  → UnionCF A f mf ay psupf x1   ⊆'  UnionCF A f mf ay psupf x  
+          chain-mono {x} x1≤x {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  
+                 ; u<x = ? ; uchain = zc11 }  ⟫ where
               zc11 : Chain A f mf ay psupf (UChain.u (proj2 za)) a
               zc11 with UChain.uchain (proj2 za)
               ... | ch-init .a x = ch-init a x
-              ... | ch-is-sup is-sup fc = ch-is-sup ? (subst (λ k → FClosure A f k a ) ? fc )
+              ... | ch-is-sup is-sup fc = ch-is-sup ? fc
+              -- OrdTrans (UChain.u<x (proj2 za)) ?  
 
-          chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain 
-             → UnionCF A f mf ay psupf x ≡ pchain 
-          chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
+          chain-≡ : {x1 : Ordinal } → x1 o≤ x  → UnionCF A f mf ay psupf x ⊆'  UnionCF A f mf ay psupf x1
+             → UnionCF A f mf ay psupf x ≡ UnionCF A f mf ay psupf x1 
+          chain-≡ {x1} x1≤x lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono x1≤x }
 
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)