# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688159943 -32400
# Node ID 2da55d442e4f62898002f83998a669f3cf4671bc
# Parent  51956de5145592b3d01d212cd7587a067e4aee39
...

diff -r 51956de51455 -r 2da55d442e4f src/cardinal.agda
--- a/src/cardinal.agda	Fri Jun 30 21:57:16 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 01 06:19:03 2023 +0900
@@ -388,9 +388,14 @@
       ... | case2 lt1 = ?
 
       be72 :  (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x) →  h (be71 x bx cc1 ) (cc10 bx cc1) ≡ x
-      be72 x bx (case1 x₁)  with cc10 bx (case1 x₁)
-      ... | case1 c1 = ? -- trans ? (UC-iso1 x (subst (λ k → odef k x) (sym *iso) x₁))
-      ... | case2 c2 = ⊥-elim ( c2 ? )
+      be72 x bx (case1 (x₁ @ record { y = y ; ay = ay ; x=fy = x=fy })) = subst (λ k → fU (Uf x (subst (λ k → odef k x) (sym *iso) x₁)) k ≡ x) 
+        ? be76 where
+          be77 : odef (* (& UC)) (Uf x (subst (λ k → odef k x) (sym *iso) x₁)) ≅ be08 (subst (λ k → odef k x) (sym *iso) x₁)
+          be77 = ?
+          be76 : fU (Uf x (subst (λ k → odef k x) (sym *iso) x₁)) (be08 (subst (λ k → odef k x) (sym *iso) x₁)) ≡ x
+          be76 = UC-iso1 x (subst (λ k → odef k x) (sym *iso) x₁)
+      -- ... | case1 c1 = ? -- trans ? (UC-iso1 x (subst (λ k → odef k x) (sym *iso) x₁))
+      -- ... | case2 c2 = ⊥-elim ( c2 ? )
       be72 x bx (case2 x₁)  with cc10 bx (case2 x₁)
       ... | case1 c1 = ⊥-elim ( x₁ ? )
       ... | case2 c2 = trans ? (a-UC-iso1 x ? )