--- a/HOD.agda	Sun Jul 07 00:31:15 2019 +0900
+++ b/HOD.agda	Sun Jul 07 00:51:12 2019 +0900
@@ -234,7 +234,11 @@
 csuc x = Ord ( osuc ( od→ord x ))
 
 in-codomain : {n : Level} → (X : HOD {suc n} ) → ( ψ : HOD {suc n} → HOD {suc n} ) → HOD {suc n}
-in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (Ord y )))))  }
+in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (Ord y )))))
+    ; otrans = lemma } where
+  lemma : {x : Ordinal} → ¬ ((y : Ordinal) → ¬ def X y ∧ (x ≡ od→ord (ψ (Ord y)))) →
+    {y : Ordinal} → y o< x → ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (y ≡ od→ord (ψ (Ord y₁))))
+  lemma {x} notx {y} y<x noty = {!!}
 
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
 
@@ -299,7 +303,12 @@
     ; isZF = isZF 
  } where
     Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
-    Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
+    Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x ;
+         otrans = lemma } where
+       lemma :  {x : Ordinal} → (x o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) x →
+            {y : Ordinal} → y o< x → (y o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) y
+       lemma {x} repl {y} y<x = record { proj1 = ordtrans y<x (proj1 repl)
+         ; proj2 = otrans (in-codomain X ψ) (proj2 repl) y<x }
     Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n}
     Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → X ∋ ord→od y  → ψ (ord→od y)) ∧ (X ∋ ord→od x )  ; otrans = lemma } where
        lemma :  {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
@@ -345,8 +354,8 @@
        ;   infinity∅ = infinity∅
        ;   infinity = λ _ → infinity
        ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
-       ;   replacement← = {!!}
-       ;   replacement→ = {!!}
+       ;   replacement← = replacement←
+       ;   replacement→ = replacement→
      } where
 
          pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
@@ -418,14 +427,10 @@
          power→ :  ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
          power→ = {!!}
          power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A = def-subst {suc n} {Replace (Def (Ord a)) ψ} {_} {Power A} {od→ord t} {!!} {!!} lemma1 where
+         power← A t t→A = {!!} where 
               a = od→ord A
               ψ : HOD → HOD
               ψ y = Def (Ord a) ∩ y
-              lemma1 : od→ord (Def (Ord a) ∩ t) ≡ od→ord t
-              lemma1 = {!!} 
-              lemma2 : Ord ( sup-o ( λ x → od→ord (ψ (ord→od x )))) ≡ Power A
-              lemma2 = {!!}
 
          union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}
          union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )