# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595901068 -32400
# Node ID ce2ce3f62023c01452897a626d5c541f27d94699
# Parent  d87492ae40401b53c4c783f833ce9c903ea3ace7
...

diff -r d87492ae4040 -r ce2ce3f62023 OD.agda
--- a/OD.agda	Tue Jul 28 10:32:33 2020 +0900
+++ b/OD.agda	Tue Jul 28 10:51:08 2020 +0900
@@ -519,9 +519,11 @@
                   (od→ord (ord→od x₁ , ord→od x₁))  record {proj1 = pair2 ; proj2 = subst (λ k → odef k (od→ord (ord→od x₁))) (sym oiso) pair1 } )
                lemma1 : infinite ∋ ord→od x₁
                lemma1 = subst (λ k → odef infinite k) (sym diso) ltd
+               lemma2 : {x₁ : Ordinal} → {ltd : infinite-d x₁ } → ω→nato ltd ≡ ω→nat (ord→od x₁) (subst (λ k → odef infinite k) (sym diso) ltd)
+               lemma2 {o∅} {iφ} = {!!}
+               lemma2 {x₁}  {isuc ltd} = cong (λ k → Suc k ) ( lemma2 {_} {ltd} )
                lemma :  nat→ω (ω→nato ltd) ≡ ord→od x₁
-               lemma with prev {ord→od x₁} lemma0 lemma1
-               ... | t = {!!}
+               lemma = trans  (cong (λ k →  nat→ω  k) lemma2) ( prev {ord→od x₁} lemma0 lemma1 )
 
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t