Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1418:51956de51455

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 30 Jun 2023 21:57:16 +0900
parents 04bb6152f691
children 2da55d442e4f
files src/cardinal.agda
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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₁ ? )