--- a/OD.agda	Mon Jul 27 18:52:48 2020 +0900
+++ b/OD.agda	Mon Jul 27 19:58:46 2020 +0900
@@ -460,17 +460,32 @@
     → ( ( x : Ordinal ) → ( lx : odef A x ) → f (ord→od x) (d→∋ A lx) )
     → ( lt : A ∋ i ) → f i lt 
 ord∋eq {A} {i} {f} of lt = lemma oiso lt where
-   eq2 : {i j : Ordinal } → i ≡ j →  (lti : odef A i ) → (ltj : odef A j ) → lti ≅ ltj → ?
-   eq2 refl _ _ HE.refl = {!!}
-   eq1 : {j : Ordinal } → (lt : odef A (od→ord (ord→od j)) ) → d→∋ A (subst (λ k → def (od A) k) diso lt) ≡ lt
-   eq1 {j} lt = {!!}
+   lemma2 : (j : Ordinal) → (ltj :  odef A j )
+          → (i : HOD) → (lti :  odef A (od→ord i) )
+          →  (ord→od j ≡ i ) →  d→∋ A ltj ≅ lti
+   lemma2 j _ i _ refl = HE.refl 
+   lemma1 : (j : Ordinal) → (ltj :  odef A j )
+          → (i : HOD) → (lti :  odef A (od→ord i) )
+          →  (ord→od j ≡ i ) →  d→∋ A ltj ≅ lti
+          → f (ord→od j) (d→∋ A ltj) ≡ f i lti
+   lemma1 j _ i _ refl HE.refl = refl
+   lemma0 : (j : Ordinal) → (lt :  odef A j ) → f (ord→od j) (d→∋ A lt) 
+   lemma0 j  lt = of j lt
    lemma : {i : HOD } → {j : Ordinal} → ord→od j ≡ i  → (lti : odef A (od→ord i)) → f i lti
    lemma {i} {j} refl lt = subst (λ k → f (ord→od j) k ) {!!} ( of j (subst (λ k → odef A k ) diso lt ))
 
 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
 nat→ω-iso  {i} lt = ord∋eq {infinite} {i} (λ x lx → lemma lx ) lt where
    lemma : {x : Ordinal} → (lx : infinite-d x ) → nat→ω ( ω→nat (ord→od x) (d→∋ infinite lx) ) ≡ ord→od x
-   lemma = {!!}
+   lemma {o∅} iφ = begin
+         nat→ω (ω→nat (ord→od o∅) (d→∋ infinite iφ))
+      ≡⟨ {!!} ⟩
+         nat→ω Zero
+      ≡⟨ sym o∅≡od∅ ⟩
+          ord→od o∅ 
+      ∎ where open ≡-Reasoning
+   lemma {x1} (isuc lx) = {!!}
+   
 
 infixr  200 _∈_
 -- infixr  230 _∩_ _∪_