--- a/ordinal.agda	Sat Aug 01 11:06:29 2020 +0900
+++ b/ordinal.agda	Sat Aug 01 18:05:23 2020 +0900
@@ -1,13 +1,15 @@
 open import Level
 module ordinal where
 
-open import zf
-
+open import logic
+open import nat
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 open import Data.Empty
-open import  Relation.Binary.PropositionalEquality
-open import  logic
-open import  nat
+open import Relation.Binary.PropositionalEquality
+open import Data.Nat.Properties 
+open import Relation.Nullary
+open import Relation.Binary.Core
+
 
 data OrdinalD {n : Level} :  (lv : Nat) → Set n where
    Φ : (lv : Nat) → OrdinalD  lv
@@ -40,16 +42,6 @@
 d<→lv Φ< = refl
 d<→lv (s< lt) = refl
 
-o<-subst : {n : Level } {Z X z x : Ordinal {n}}  → Z o< X → Z ≡ z  →  X ≡ x  →  z o< x
-o<-subst df refl refl = df
-
-open import Data.Nat.Properties 
-open import Data.Unit using ( ⊤ )
-open import Relation.Nullary
-
-open import Relation.Binary
-open import Relation.Binary.Core
-
 o∅ : {n : Level} → Ordinal {n}
 o∅  = record { lv = Zero ; ord = Φ Zero }
 
@@ -207,14 +199,14 @@
 
 C-Ordinal : {n : Level} →  Ordinals {suc n} 
 C-Ordinal {n} = record {
-     ord = Ordinal {suc n}
+     Ordinal = Ordinal {suc n}
    ; o∅ = o∅
    ; osuc = osuc
    ; _o<_ = _o<_
    ; next = next
    ; isOrdinal = record {
-       Otrans = ordtrans
-     ; OTri = trio<
+       ordtrans = ordtrans
+     ; trio< = trio<
      ; ¬x<0 = ¬x<0 
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<