--- a/BAlgbra.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/BAlgbra.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -4,7 +4,9 @@
 
 open import zf
 open import logic
+import OrdUtil
 import OD 
+import ODUtil
 import ODC
 
 open import Relation.Nullary
@@ -16,6 +18,12 @@
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ )  
 
 open inOrdinal O
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
+
 open OD O
 open OD.OD
 open ODAxiom odAxiom
@@ -47,7 +55,7 @@
         lemma4 {y} z with proj1 z
         lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) *iso (proj2 z)) )
         lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) *iso (proj2 z)) )
-        lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (* u) x) → ⊥) → odef (A ∪ B) x
+        lemma3 : (((u : Ordinal ) → ¬ odef (A , B) u ∧ odef (* u) x) → ⊥) → odef (A ∪ B) x
         lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not)   -- choice
     lemma2 :  {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
     lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A