# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593762619 -32400
# Node ID 35e1214fa0933fa5c88fab6711c52ece562310d7
# Parent  6b09b5af9fcd62b40d507141f30f6a5d2a256609
...

diff -r 6b09b5af9fcd -r 35e1214fa093 OD.agda
--- a/OD.agda	Fri Jul 03 13:36:17 2020 +0900
+++ b/OD.agda	Fri Jul 03 16:50:19 2020 +0900
@@ -442,10 +442,20 @@
               sup1 =  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 
+              lemmab : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) )))) o< sup1
+              lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 
+              lemmad : Ord (osuc (od→ord A)) ∋ t
+              lemmad = subst (λ k → k o< osuc (od→ord A)) {!!} {!!} -- ( ⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → {!!} ) )
+              lemmac : ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) ))) =h= Ord (od→ord A)
+              lemmac = record { eq→ = {!!} ; eq← = {!!} }
+              lemmae : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A))
+              lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac)
               lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
-              lemma7 with osuc-≡< ( ⊆→o≤ t→A )
-              lemma7 | case1 eq = subst (λ k → k o< sup1 ) {!!} (sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 )
-              lemma7 | case2 lt = ordtrans (subst₂ (λ j k → j o< k ) {!!} {!!} lt) (sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 )
+              lemma7 with osuc-≡< lemmad
+              lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab )
+              lemma7 | case1 eq with osuc-≡< lemmad 
+              lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae {!!}) lemmab -- od→ord (Ord (od→ord A)) ≡ od→ord t
+              lemma7 | case1 eq | case2 lt = ordtrans {!!} (subst (λ k → k o< sup1) lemmae lemmab ) 
               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 )