--- a/HOD.agda	Wed Jun 26 20:32:30 2019 +0900
+++ b/HOD.agda	Wed Jun 26 22:53:30 2019 +0900
@@ -207,6 +207,9 @@
 
 open _∧_
 
+ord⇔ : {n : Level} →  ( x y : HOD {suc n} ) → ( {z : Ordinal {suc n} } → def x z ⇔ def y z ) → od→ord x ≡ od→ord y
+ord⇔ = {!!}
+
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
 
@@ -371,29 +374,25 @@
          extensionality : {A B : HOD {suc n}} → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
-         xx-union : {x  : HOD {suc n}} → (x , x) ≡ record { def = λ z → z o< osuc (od→ord x) }
-         xx-union {x} = cong ( λ k → Ord k ) (omxx (od→ord x))
-         xxx-union : {x  : HOD {suc n}} → (x , (x , x)) ≡ record { def = λ z → z o< osuc (osuc (od→ord x))}
-         xxx-union {x} = cong ( λ k → Ord k ) lemma where
-             lemma1 : {x  : HOD {suc n}} → od→ord x o< od→ord (x , x)
-             lemma1 {x} = c<→o< ( proj1 (pair x x ) )
-             lemma2 : {x  : HOD {suc n}} → od→ord (x , x) ≡ osuc (od→ord x)
-             lemma2 = trans ( cong ( λ k →  od→ord k ) xx-union ) {!!}
-             lemma : {x  : HOD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x))
-             lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) lemma1 ) ) ( cong ( λ k → osuc k ) lemma2 )
-         uxxx-union : {x  : HOD {suc n}} → Union (x , (x , x)) ≡ record { def = λ z → osuc z o< osuc (osuc (od→ord x)) }
-         uxxx-union {x} = cong ( λ k → record { def = λ z → osuc z o< k ; otrans = {!!} } ) {!!} where
-             lemma : od→ord (x , (x , x)) ≡ osuc (osuc (od→ord x))
-             lemma = trans ( cong ( λ k → od→ord k ) xxx-union ) {!!}
-         uxxx-2 : {x  : HOD {suc n}} → record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } == record { def = λ z → z o< osuc (od→ord x) }
-         eq→ ( uxxx-2 {x} ) {m} lt = proj1 (osuc2 m (od→ord x)) lt
-         eq← ( uxxx-2 {x} ) {m} lt = proj2 (osuc2 m (od→ord x)) lt
-         uxxx-ord : {x  : HOD {suc n}} → od→ord (Union (x , (x , x))) ≡ osuc (od→ord x)
-         uxxx-ord {x} = trans (cong (λ k →  od→ord k ) uxxx-union) {!!} 
+         open  import  Relation.Binary.PropositionalEquality
+         uxxx-ord : {x  : HOD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) )
+         uxxx-ord {x} {y} = subst (λ k → k ⇔ ( y o< osuc (od→ord x) )) (sym lemma) ( osuc2 y (od→ord x))  where
+              lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x)) 
+              lemma {y} = let open ≡-Reasoning in begin
+                   def (Union (x , (x , x))) y  
+                ≡⟨⟩
+                   def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x)  (od→ord x)  )) ))) ( osuc y )
+                ≡⟨⟩
+                   osuc y o<  omax (od→ord x) (od→ord (Ord (omax (od→ord x)  (od→ord x)  )) )
+                ≡⟨ cong (λ k → osuc y o<  omax (od→ord x) k ) (sym ord-Ord)  ⟩
+                   osuc y o<  omax (od→ord x) (omax (od→ord x)  (od→ord x)  ) 
+                ≡⟨ cong (λ k → osuc y o<  k ) (omxxx  (od→ord x) )  ⟩
+                   osuc y o< osuc (osuc (od→ord x))
+                ∎ 
          infinite : HOD {suc n}
          infinite = Ord omega 
          infinity∅ : Ord omega  ∋ od∅ {suc n}
-         infinity∅ = {!!}
+         infinity∅ = o<-subst (case1 (s≤s z≤n) ) ord-Ord refl
          infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
          infinity x lt = {!!} where
               lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega