--- a/OD.agda	Thu Aug 01 15:38:08 2019 +0900
+++ b/OD.agda	Fri Aug 02 12:17:10 2019 +0900
@@ -11,6 +11,9 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 
+open import logic
+open import nat
+
 -- Ordinal Definable Set
 
 record OD {n : Level}  : Set (suc n) where
@@ -21,6 +24,8 @@
 
 open Ordinal
 open _∧_
+open _∨_
+open Bool
 
 record _==_ {n : Level} ( a b :  OD {n} ) : Set n where
   field
@@ -155,9 +160,6 @@
 o≡→== : {n : Level} →  { x y : Ordinal {n} } → x ≡  y →  ord→od x == ord→od y
 o≡→== {n} {x} {.x} refl = eq-refl
 
->→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
->→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
-
 c≤-refl : {n : Level} →  ( x : OD {n} ) → x c≤ x
 c≤-refl x = case1 refl