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

diff -r 04bb6152f691 -r 51956de51455 src/cardinal.agda
--- a/src/cardinal.agda	Fri Jun 30 21:37:32 2023 +0900
+++ b/src/cardinal.agda	Fri Jun 30 21:57:16 2023 +0900
@@ -389,7 +389,7 @@
 
       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₁))
+      ... | 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₁ ? )