# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688528136 -32400
# Node ID b7f6eb9eaf0d01976908a8f9e55ee23d5d26921f
# Parent  a295c52af3b725d29fdbd2fd3e226cf23a0bca76
...

diff -r a295c52af3b7 -r b7f6eb9eaf0d src/cardinal.agda
--- a/src/cardinal.agda	Wed Jul 05 10:57:43 2023 +0900
+++ b/src/cardinal.agda	Wed Jul 05 12:35:36 2023 +0900
@@ -373,13 +373,14 @@
 
      p0 : odef (Power S) o∅
      p0 z xz = ⊥-elim (¬x<0 (subst (λ k → odef k z) o∅≡od∅ xz)  )
-
+ 
      s : Ordinal 
      s = fun→ b o∅ p0
 
      ss : odef S s
      ss = funB b o∅ p0
 
+
      diag4 : ⊥ 
      diag4 with ODC.p∨¬p O ( odef (* (fun← b s ss)) s)
      ... | case1 y  = ?