--- a/OD.agda	Tue Jul 28 20:48:24 2020 +0900
+++ b/OD.agda	Tue Jul 28 22:34:42 2020 +0900
@@ -519,6 +519,9 @@
 ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
 ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
 
+ω-∈s : (x : HOD) →  Union ( x , (x , x)) ∋ x
+ω-∈s x not = not (od→ord (x , x)) record { proj1 = case2 refl ; proj2 = subst (λ k → odef k (od→ord x) ) (sym oiso) (case1 refl) }
+
 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
 nat→ω-iso {i} = ε-induction1 {λ i →  (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
      ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
@@ -543,8 +546,8 @@
                lemma1 = subst (λ k → odef infinite k) (sym diso) ltd
                lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
                lemma3 iφ iφ refl = HE.refl
-               lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ? )
-               lemma3 (isuc ltd) iφ eq = {!!}
+               lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) diso eq (c<→o< (ω-∈s (ord→od y)) )))
+               lemma3 (isuc {y} ltd)  iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) diso (sym eq) (c<→o< (ω-∈s (ord→od y)) )))
                lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
                ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq eq)) t  
                lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1