--- a/OD.agda	Wed Jul 31 12:40:02 2019 +0900
+++ b/OD.agda	Wed Jul 31 15:29:51 2019 +0900
@@ -104,15 +104,15 @@
 otrans : {n : Level} {a x y : Ordinal {n} } → def (Ord a) x → def (Ord x) y → def (Ord a) y
 otrans x<a y<x = ordtrans y<x x<a
 
-∅3 : {n : Level} →  { x : Ordinal {n}}  → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
+∅3 : {n : Level} →  { x : Ordinal {suc n}}  → ( ∀(y : Ordinal {suc n}) → ¬ (y o< x ) ) → x ≡ o∅ {suc n}
 ∅3 {n} {x} = TransFinite {n} c2 c3 x where
-   c0 : Nat →  Ordinal {n}  → Set n
-   c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x))  → x ≡ o∅ {n}
-   c2 : (lx : Nat) → c0 lx (record { lv = lx ; ord = Φ lx } )
-   c2 Zero not = refl
-   c2 (Suc lx) not with not ( record { lv = lx ; ord = Φ lx } )
+   c0 : Nat →  Ordinal {suc n}  → Set (suc n)
+   c0 lx x = (∀(y : Ordinal {suc n}) → ¬ (y o< x))  → x ≡ o∅ {suc n}
+   c2 : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → c0 (lv x₁) (record { lv = lv x₁ ; ord = ord x₁ }))→ c0 lx (record { lv = lx ; ord = Φ lx } )
+   c2 Zero _ not = refl
+   c2 (Suc lx) _ not with not ( record { lv = lx ; ord = Φ lx } )
    ... | t with t (case1 ≤-refl )
-   c2 (Suc lx) not | t | ()
+   c2 (Suc lx) _ not | t | ()
    c3 : (lx : Nat) (x₁ : OrdinalD lx) → c0 lx  (record { lv = lx ; ord = x₁ })  → c0 lx (record { lv = lx ; ord = OSuc lx x₁ })
    c3 lx (Φ .lx) d not with not ( record { lv = lx ; ord = Φ lx } )
    ... | t with t (case2 Φ< )