# HG changeset patch # User Shinji KONO # Date 1593762704 -32400 # Node ID c030a9655e79df04f0153c58985187b147bb286a # Parent 35e1214fa0933fa5c88fab6711c52ece562310d7 ... diff -r 35e1214fa093 -r c030a9655e79 OD.agda --- a/OD.agda Fri Jul 03 16:50:19 2020 +0900 +++ b/OD.agda Fri Jul 03 16:51:44 2020 +0900 @@ -445,7 +445,7 @@ 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 → {!!} ) ) + lemmad = {!!} 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)) @@ -453,7 +453,7 @@ lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t) 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 with osuc-≡< (⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → {!!} )) 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)))