--- a/ordinal-definable.agda	Mon Jun 10 00:29:20 2019 +0900
+++ b/ordinal-definable.agda	Mon Jun 10 09:35:14 2019 +0900
@@ -134,9 +134,6 @@
 =-iso : {n : Level } {x y : OD {suc n} } → (x == y) ≡ (ord→od (od→ord x) == y)
 =-iso {_} {_} {y} = cong ( λ k → k == y ) (sym oiso)
 
-=>-iso : {n : Level } {x y z : OD {suc n} } → (x == y) → def z (od→ord x ) → def z (od→ord y )
-=>-iso {n} {x} {y} {z} eq z>x = {!!}
-
 ord→== : {n : Level} →  { x y : OD {n} } → od→ord x ≡  od→ord y →  x == y
 ord→== {n} {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
    lemma : ( ox oy : Ordinal {n} ) → ox ≡ oy →  (ord→od ox) == (ord→od oy)
@@ -178,6 +175,15 @@
 od≡-def : {n : Level} →  { x : Ordinal {suc n} } → ord→od x ≡ record { def = λ z → z o< x } 
 od≡-def {n} {x} = subst (λ k  → ord→od x ≡ k ) oiso (cong ( λ k → ord→od k ) (≡-def {n} {x} ))
 
+==→o≡1 : {n : Level} →  { x y : OD {suc n} } → x == y →  od→ord x ≡ od→ord y 
+==→o≡1 eq = ==→o≡ (subst₂ (λ k j → k == j ) (sym oiso) (sym oiso) eq )
+
+==-def-l : {n : Level } {x y : Ordinal {suc n} } { z : OD {suc n} }→ (ord→od x == ord→od y) → def z x → def z y
+==-def-l {n} {x} {y} {z} eq z>x = subst ( λ k → def z k ) (==→o≡ eq) z>x
+
+==-def-r : {n : Level } {x y : OD {suc n} } { z : Ordinal {suc n} }→ (x == y) → def x z → def y z
+==-def-r {n} {x} {y} {z} eq z>x = subst (λ k → def k z ) (subst₂ (λ j k → j ≡ k ) oiso oiso (cong (λ k → ord→od k) (==→o≡1 eq))) z>x  
+
 ∋→o< : {n : Level} →  { a x : OD {suc n} } → a ∋ x → od→ord x o< od→ord a
 ∋→o< {n} {a} {x} lt = t where
          t : (od→ord x) o< (od→ord a)
@@ -339,20 +345,24 @@
          power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
          power→ A t P∋t {x} t∋x = proj1 lemma-s where
               minsup :  OD
-              minsup =  csuc (ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) )
-              lemma-t : minsup ∋ t
-              lemma-t = o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) {!!} {!!} )) {!!} {!!} ) 
+              minsup =  ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 
+              lemma-t : csuc minsup ∋ t
+              lemma-t = o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) refl diso )) refl refl ) 
               lemma-s : ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))  ∋ x
-              lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) {!!} {!!} )
-              lemma-s | case1 eq = {!!}
-              lemma-s | case2 lt = {!!}
+              lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl diso  )
+              lemma-s | case1 eq = def-subst ( ==-def-r (o≡→== eq) (subst (λ k → def k (od→ord x)) (sym oiso) t∋x ) ) oiso refl
+              lemma-s | case2 lt = transitive {n} {minsup} {t} {x} (def-subst (o<→c< lt) oiso refl ) t∋x
               -- = {!!} -- transitive {!!} t∋x
          power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A  = def-subst ( o<→c< lemma ) {!!} {!!} where
+         power← A t t→A  = def-subst {suc n} {_} {_} {Power A} {od→ord t}
+                  ( o<→c< {suc n} {od→ord (ZFSubset A (ord→od (od→ord t)) )} {sup-o (λ x → od→ord (ZFSubset A (ord→od x)))}
+                      lemma ) refl lemma1 where
               lemma-eq :  ZFSubset A t == t
               eq→ lemma-eq {z} w = proj2 w 
               eq← lemma-eq {z} w = record { proj2 = w  ;
                  proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
+              lemma1 : od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t
+              lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) (==→o≡1 (lemma-eq))
               lemma :  od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
               lemma = sup-o<   
          union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → csuc z ∋ z