--- a/HOD.agda	Mon Jul 15 09:31:32 2019 +0900
+++ b/HOD.agda	Mon Jul 15 15:54:59 2019 +0900
@@ -247,6 +247,9 @@
 omega : { n : Level } → Ordinal {n}
 omega = record { lv = Suc Zero ; ord = Φ 1 }
 
+od-infinite : {n : Level} → OD {suc n}
+od-infinite = record { def = λ x → x o< sup-o ( λ y → od→ord (Ord y)) }
+
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
     ZFSet = OD {suc n}
@@ -258,7 +261,7 @@
     ; Power = Power
     ; Select = Select
     ; Replace = Replace
-    ; infinite = Ord omega
+    ; infinite = od-infinite
     ; isZF = isZF 
  } where
     ZFSet = OD {suc n}
@@ -284,7 +287,7 @@
     infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
     infixr  220 _⊆_
-    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (Ord omega)
+    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace od-infinite
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
@@ -297,7 +300,7 @@
        ;   minimul = minimul
        ;   regularity = regularity
        ;   infinity∅ = infinity∅
-       ;   infinity = λ _ → infinity
+       ;   infinity = infinity
        ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
        ;   replacement← = replacement←
        ;   replacement→ = replacement→
@@ -473,29 +476,29 @@
               xod  : {lx : Nat } → { ox : OrdinalD {suc n} lx } → OD {suc n}
               xod  {lx} {ox} = ord→od (xord {lx} {ox})
               lemmaφ :  (lx : Nat) → def (Union (odΦ {lx} , (odΦ {lx} , odΦ {lx} ))) y ⇔ (y o< osuc (record { lv = lx ; ord = Φ lx }))
-              proj1 (lemmaφ lx) = {!!}
+              proj1 (lemmaφ lx) df = TransFiniteExists _ df lemma where
+                  lemma : {y1 : Ordinal} → def (odΦ {lx} , (odΦ {lx} , odΦ {lx} )) y1 ∧ def (ord→od y1) y → y o< xord {lx} {OSuc lx (Φ lx)}
+                  lemma {y1} xx with proj1 xx | c<→o< {suc n} {ord→od y} {ord→od y1} (def-subst {suc n} {ord→od y1} {y} (proj2 xx) refl (sym diso))
+                  --  x : lv y1 < lx ,  x₁ : lv (od→ord (ord→od y) < lv y1  -> lv y < lx
+                  lemma {y1} xx | case1 x | case1 x₁ =
+                      case1 ( <-trans  (subst (λ k → lv k < lv (od→ord (ord→od y1))) diso x₁) (subst (λ k → lv k < lx ) (sym diso) {!!}) )
+                  lemma {y1} xx | case1 x | case2 x₁ with d<→lv x₁
+                  ... | eq = case1 {!!}
+                  lemma {y1} xx | case2 x | lt = {!!}
               proj2 (lemmaφ lx) lt not = not (ordΦ {lx}){!!}
               lemma-suc : (lx : Nat) (ox : OrdinalD lx) →
                     def (Union (xod {lx} {ox} , (xod {lx} {ox} , xod {lx} {ox} ))) y ⇔ (y o< osuc (xord {lx} {ox})) →
                     def (Union (xod {lx} {OSuc lx ox} , (xod {lx} {OSuc lx ox} , xod {lx} {OSuc lx ox} ))) y
                         ⇔ (y o< osuc (xord  {lx} {OSuc lx ox}))
-              proj1 (lemma-suc lx ox prev) = {!!}
+              proj1 (lemma-suc lx ox prev) df =  TransFiniteExists _ df {!!}
               proj2 (lemma-suc lx ox prev) lt not = not (xord {lx} {ox}) {!!}
               lemma = TransFinite {suc n} {λ ox → def (Union (ord→od ox , (ord→od ox , ord→od ox))) y ⇔ ( y o< osuc ox ) }
                   lemmaφ lemma-suc (od→ord x) where
 
-         infinite : OD {suc n}
-         infinite = Ord omega 
-         infinity∅ : Ord omega  ∋ od∅ {suc n}
-         infinity∅ = o<-subst (case1 (s≤s z≤n) ) (sym ord-od∅) refl
-         infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-         infinity x lt = o<-subst ( lemma (od→ord x) lt ) eq refl where
-              eq :  osuc (od→ord x) ≡ od→ord (Union (x , (x , x)))
-              eq = let open ≡-Reasoning in begin
-                    osuc (od→ord x)
-                 ≡⟨ {!!}  ⟩
-                    od→ord (Union (x , (x , x)))
-                 ∎
+         infinity∅ : od-infinite  ∋ od∅ {suc n}
+         infinity∅ = {!!} -- o<-subst (case1 (s≤s z≤n) ) (sym ord-od∅) refl
+         infinity : (x : OD) → od-infinite ∋ x → od-infinite ∋ Union (x , (x , x ))
+         infinity x lt = {!!} where
               lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega 
               lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n)
               lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n)