# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688092204 -32400
# Node ID cc76e2b1f3b5ded6650848cb3a731202c0d5ec99
# Parent  1e2c77c1227d1b6cd4f71872afd22abbbe1d41eb
...

diff -r 1e2c77c1227d -r cc76e2b1f3b5 src/cardinal.agda
--- a/src/cardinal.agda	Fri Jun 30 10:58:06 2023 +0900
+++ b/src/cardinal.agda	Fri Jun 30 11:30:04 2023 +0900
@@ -338,13 +338,21 @@
            be60 = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫
 
       be72 :  (x : Ordinal) (bx : odef (* b) x) → h (be71 x bx) ≡ x
-      be72  x bx with ODC.∋-p O UC (* (h⁻¹ bx))
-      be72 x bx | yes cn with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) 
-      be72 x bx | yes cn | case1 record { y = y ; ay = ay ; x=fy = x=fy } with CN.i (subst (λ k → CN k) &iso cn) | CN.gfix (subst (λ k → CN k) &iso cn)
-      ... | 0 | a-g ax ¬ib = ?
-      ... | suc i | next-gf ix t = ?
-      be72 x bx | yes cn | case2 nimg = ?
-      be72 x bx | no ncn  = ?
+      be72 x bx = ? where
+           be73 : (cn : odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) → odef (* a) (Uf x (subst (λ k → odef k x) (sym *iso) cn))
+           be73 cn with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)   
+           ... | case1 img = be03 (subst (λ k → odef k x) (sym *iso) cn) where
+               be03 : (cn : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x) → odef (* a) (Uf x cn )
+               be03 cn with subst (λ k → odef k x ) *iso cn
+               ... | record { y = y ; ay = ay ; x=fy = x=fy } = UC⊆a ay
+           ... | case2 nimg = ⊥-elim ( nimg cn)
+           be60 : (ncn : ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) → odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
+           be60 ncn = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫
+           be74 : (ncn : ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) → odef (* a) (i→ be11 x (subst (λ k → odef k x ) (sym *iso) (be60 ncn) )) 
+           be74 ncn with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)   
+           ... | case1 img = ⊥-elim ( ncn img )
+           ... | case2 nimg = proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be11 x (subst (λ k → odef k x) (sym *iso) (be60 ncn)) ))   
+
 
 _c<_ : ( A B : HOD ) → Set n
 A c< B = ¬ ( Injection (& A)  (& B) )