--- a/ordinal.agda	Mon May 20 18:18:43 2019 +0900
+++ b/ordinal.agda	Tue May 21 00:30:01 2019 +0900
@@ -30,11 +30,22 @@
 
 open import Data.Nat.Properties 
 open import Data.Empty
+open import Data.Unit using ( ⊤ )
 open import Relation.Nullary
 
 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 }
 
@@ -167,13 +178,13 @@
      }
  }
 
-TransFinite : {n : Level} → ( ψ : Ordinal {n} → Set n ) 
+TransFinite : {n : Level} → { ψ : Ordinal {n} → Set n }
   → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 
   → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
   → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
   →  ∀ (x : Ordinal)  → ψ x
-TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
-TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
-    ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
-TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
+TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
+TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
+    ( TransFinite caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
+TransFinite caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁