--- a/ordinal.agda	Tue Jul 30 17:52:15 2019 +0900
+++ b/ordinal.agda	Wed Jul 31 12:40:02 2019 +0900
@@ -112,10 +112,22 @@
 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
 ¬a≤a  (s≤s lt) = ¬a≤a  lt
 
+a<sa : {la : Nat} → la < Suc la 
+a<sa {Zero} = s≤s z≤n
+a<sa {Suc la} = s≤s a<sa 
+
 =→¬< : {x : Nat  } → ¬ ( x < x )
 =→¬< {Zero} ()
 =→¬< {Suc x} (s≤s lt) = =→¬< lt
 
+<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
+<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
+<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
+<-∨ {Suc x} {Zero} (s≤s ())
+<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
+<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
+<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
+
 case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥
 case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2
 ... | refl = nat-≡< refl lt1
@@ -124,7 +136,7 @@
 case21-⊥ {x} {y} lt1 lt2 with d<→lv lt2
 ... | refl = nat-≡< refl lt1
 
-o<¬≡ : {n : Level } { ox oy : Ordinal {n}} → ox ≡ oy  → ox o< oy  → ⊥
+o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy  → ox o< oy  → ⊥
 o<¬≡ {_} {ox} {ox} refl (case1 lt) =  =→¬< lt
 o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt
 
@@ -315,13 +327,27 @@
      }
  }
 
-TransFinite : {n m : Level} → { ψ : Ordinal {n} → Set m }
-  → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
+TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
+  → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx)  → ψ x ) → ψ ( 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Φ caseOSuc record { lv = lv ; ord = (Φ (lv)) } = caseΦ lv
-TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = 
-      caseOSuc lx ox (TransFinite caseΦ caseOSuc  record { lv = lx ; ord = ox })
+TransFinite {n} {m} {ψ} caseΦ caseOSuc x = TransFinite1 (lv x) (ord x) where
+  TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox)
+  TransFinite1 Zero (Φ 0) = caseΦ Zero lemma where
+      lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
+      lemma x (case1 ())
+      lemma x (case2 ())
+  TransFinite1 (Suc lx) (Φ (Suc lx)) = caseΦ (Suc lx) lemma where
+      lemma : (x : Ordinal) → x o< ordinal (Suc lx) (Φ (Suc lx)) → ψ x
+      lemma (ordinal lx1 ox1) (case1 lt) with <-∨ lt
+      lemma (ordinal lx (Φ lx)) (case1 lt) | case1 refl = TransFinite1 lx (Φ lx)
+      lemma (ordinal lx (OSuc lx ox1)) (case1 lt) | case1 refl = caseOSuc lx ox1 ( lemma (ordinal lx ox1) (case1 a<sa)) 
+      lemma (ordinal Zero (Φ 0)) (case1 lt) | case2 (s≤s lt1) = caseΦ Zero ( λ x lt → ⊥-elim (¬x<0 lt) )
+      lemma (ordinal (Suc lx1) (Φ (Suc lx1))) (case1 lt) | case2 (s≤s lt1) = caseΦ (Suc lx1) lemma2 where
+          lemma2 : (y : Ordinal) → (Suc (lv y) ≤ Suc lx1) ∨ (ord y d< Φ (Suc lx1)) → ψ y
+          lemma2 y (case1 lt2 ) = {!!}
+      lemma (ordinal lx1 (OSuc lx1 ox1)) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 ( lemma (ordinal lx1 ox1) (case1 (<-trans lt1 a<sa ))) 
+  TransFinite1 lx (OSuc lx ox)  = caseOSuc lx ox (TransFinite1 lx ox )
 
 -- we cannot prove this in intutionistic logic 
 --  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p