--- a/src/zorn.agda	Sun Nov 20 17:33:10 2022 +0900
+++ b/src/zorn.agda	Sun Nov 20 17:44:21 2022 +0900
@@ -651,6 +651,12 @@
     { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y
 init-uchain A f mf ay = ⟪ ay , ch-init (init ay refl)   ⟫
 
+record IChain  (A : HOD)  ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
+  field
+     i : Ordinal  
+     i<x : i o< x
+     fc : FClosure A f (supfz i<x) z 
+
 Zorn-lemma : { A : HOD }
     → o∅ o< & A
     → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
@@ -1307,15 +1313,9 @@
           supfz : {z : Ordinal } → z o< x → Ordinal
           supfz {z} z<x = ZChain.supf (pzc  (ob<x lim z<x)) z
 
-          record IChain (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
-              field
-                 i : Ordinal  
-                 i<x : i o< x
-                 fc : FClosure A f (supfz i<x) z 
-
           pchainx : HOD
-          pchainx = record { od = record { def = λ z → IChain supfz z } ; odmax = & A ; <odmax = zc00 } where
-               zc00 : {z : Ordinal } → IChain supfz z → z o< & A
+          pchainx = record { od = record { def = λ z → IChain A f supfz z } ; odmax = & A ; <odmax = zc00 } where
+               zc00 : {z : Ordinal } → IChain A f supfz z → z o< & A
                zc00 {z} ic = z09 ( A∋fc (supfz (IChain.i<x ic)) f mf (IChain.fc ic) )
 
           zeq : {xa xb z : Ordinal }