--- a/HOD.agda	Sun Jun 30 23:09:17 2019 +0900
+++ b/HOD.agda	Mon Jul 01 00:20:56 2019 +0900
@@ -265,20 +265,6 @@
 -- L0 :  {n : Level} → (α : Ordinal {suc n}) → α o< β → L (osuc α) ∋ L α
 -- L1 :  {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : HOD {suc n})  → L α ∋ x → L β ∋ x 
 
-record Constructible {n : Level} ( α : Ordinal {suc n}) : Set (suc (suc n)) where
-    field
-      LSet : HOD {suc n}
-      L0 :  Def LSet  ∋ LSet 
-      L1 :  {β : Ordinal {suc n}} →  {x : HOD {suc n} } → β o< α   → L β ∋ x → LSet  ∋ x 
-
-open Constructible
-
-Lα : {n : Level} → (α : Ordinal {suc n}) → Constructible {n} α
-Lα {n}  record { lv = Zero ; ord = (Φ .0) } = record { LSet = {!!} ; L0 = {!!} ; L1 = {!!} }
-Lα {n}  record { lv = lx ; ord = (OSuc lv ox) } = record { LSet = {!!} ; L0 = {!!} ; L1 = {!!} }
-Lα {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
-    record { LSet = {!!}  ; L0 = {!!} ; L1 = {!!} }
-
 omega : { n : Level } → Ordinal {n}
 omega = record { lv = Suc Zero ; ord = Φ 1 }
 
@@ -363,25 +349,23 @@
          power→ A t P∋t {x} t∋x = proj1 lemma-s where
               minsup :  HOD
               minsup =  ZFSubset A ( Ord ( 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 ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))  ∋ x
-              lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl (sym ord-Ord) )
-              lemma-s | case1 eq = {!!}
-              lemma-s | case2 lt = transitive {n} {minsup} {t} {x} {!!} t∋x
+              lemma-s with osuc-≡<  (sup-lb  P∋t)  
+              lemma-s | case1 eq = proj1 ( def-subst t∋x ()  ? )
+              lemma-s | case2 lt = {!!} 
          -- 
          -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
          -- Power A is a sup of ZFSubset A t, so Power A ∋ t
          -- 
          power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
          power← A t t→A  = def-subst {suc n} {_} {_} {Power A} {od→ord t}
-                  {!!} refl lemma1 where
+                 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) {!!}
+              lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ 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-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}