--- a/OD.agda	Mon Jul 27 16:20:14 2020 +0900
+++ b/OD.agda	Mon Jul 27 18:52:48 2020 +0900
@@ -459,10 +459,13 @@
 ord∋eq :  {A i : HOD } → { f : (x : HOD ) → A ∋ x → Set (suc n)}
     → ( ( 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 with of (od→ord i) lt
-... | t = HE.subst₂ (λ j k → f j (k j)) (HE.≡-to-≅  oiso) (f-extensionality (λ _ → refl ) lemma ) t where
-   lemma : (i : HOD) → ? ≅ ?
-   lemma = {!!}
+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 = {!!}
+   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