--- a/ordinal.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/ordinal.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -10,6 +10,10 @@
 open import Relation.Nullary
 open import Relation.Binary.Core
 
+----
+--
+-- Countable Ordinals
+--
 
 data OrdinalD {n : Level} :  (lv : Nat) → Set n where
    Φ : (lv : Nat) → OrdinalD  lv
@@ -210,8 +214,7 @@
      ; ¬x<0 = ¬x<0 
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
-     ; TransFinite = TransFinite1
-     ; TransFinite1 = TransFinite2
+     ; TransFinite = TransFinite2
      ; Oprev-p  = Oprev-p 
    } ;
    isNext = record {
@@ -244,16 +247,6 @@
      Oprev-p  (ordinal lv (OSuc lv ox)) = yes record { oprev = ordinal lv ox ; oprev=x = refl }
      ord1 : Set (suc n)
      ord1 = Ordinal {suc n}
-     TransFinite1 : { ψ : ord1  → Set (suc n) }
-          → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
-          →  ∀ (x : ord1)  → ψ x
-     TransFinite1 {ψ} lt x = TransFinite {n} {suc n} {ψ} caseΦ caseOSuc x where
-        caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
-            ψ (record { lv = lx ; ord = Φ lx })
-        caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
-        caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
-            ψ (record { lv = lx ; ord = OSuc lx x₁ })
-        caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
      TransFinite2 : { ψ : ord1  → Set (suc (suc n)) }
           → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord1)  → ψ x