# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593747607 -32400
# Node ID 8b5c8b6858835265c8f7d3f7a84f13113538b788
# Parent  c1581ed5f38b5973811244c67946a931ea67d87d
...

diff -r c1581ed5f38b -r 8b5c8b685883 OD.agda
--- a/OD.agda	Thu Jul 02 19:05:55 2020 +0900
+++ b/OD.agda	Fri Jul 03 12:40:07 2020 +0900
@@ -439,8 +439,12 @@
                     t
                  ∎
               --- (od→ord t) o< (sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x))))
+              lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A)))
+              lemma9 = <-osuc 
+              lemma8 :  od→ord t o< od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A)))))
+              lemma8 = {!!}
               lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
-              lemma7 = ordtrans {!!} (sup-o< {!!} {!!}) 
+              lemma7 = ordtrans lemma8 (sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 )
               lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
               lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  (λ x lt → od→ord (A ∩ (ord→od x))))
                   lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )