# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558430244 -32400
# Node ID 2b853472cb248ba219eb64bf8602234816bcd7b9
# Parent  3b0fdb95618e759e170023736d70e5e4877d63d7
fix

diff -r 3b0fdb95618e -r 2b853472cb24 ordinal-definable.agda
--- a/ordinal-definable.agda	Tue May 21 00:30:01 2019 +0900
+++ b/ordinal-definable.agda	Tue May 21 18:17:24 2019 +0900
@@ -96,6 +96,7 @@
    c3 lx (Φ .lx) d not | t | ()
    c3 lx (OSuc .lx x₁) d not with not (  record { lv = lx ; ord = OSuc lx x₁ } )
    ... | t with t (case2 (s< {!!} ) )
+--   x d< OSuc lx x is bad on ℵ case
    c3 lx (OSuc .lx x₁) d not | t | ()
    c3 .(Suc lv) (ℵ lv) not = {!!}
 
diff -r 3b0fdb95618e -r 2b853472cb24 ordinal.agda
--- a/ordinal.agda	Tue May 21 00:30:01 2019 +0900
+++ b/ordinal.agda	Tue May 21 18:17:24 2019 +0900
@@ -36,16 +36,6 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 
-¬ℵ : {n : Level} {lx : Nat } ( x : OrdinalD {n} lx ) → Set 
-¬ℵ (Φ lv₁) = ⊤
-¬ℵ (OSuc lv₁ x) = ¬ℵ x
-¬ℵ (ℵ lv₁) = ⊥
-
-s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → ¬ℵ x  → x d< OSuc lx x
-s<refl {n} {.lv₁} {Φ lv₁} t = Φ<
-s<refl {n} {.lv₁} {OSuc lv₁ x} t = s< (s<refl t)
-s<refl {n} {.(Suc lv₁)} {ℵ lv₁} ()
-
 o∅ : {n : Level} → Ordinal {n}
 o∅  = record { lv = Zero ; ord = Φ Zero }