# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562556848 -32400
# Node ID 21b9e78e93598600931067f76175852d53172b01
# Parent  c30bc9f5bd0d58754aff101c08e6b71f21c8dc56
union remains

diff -r c30bc9f5bd0d -r 21b9e78e9359 HOD.agda
--- a/HOD.agda	Mon Jul 08 12:13:19 2019 +0900
+++ b/HOD.agda	Mon Jul 08 12:34:08 2019 +0900
@@ -465,13 +465,15 @@
               lemma0 {x} t∋x = c<→o< (t→A t∋x)
               lemma3 : Def (Ord a) ∋ t
               lemma3 = ord-power← a t lemma0
+              lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
+              lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) (sym Ord-ord-≡) (∩-≡ t→A ) ))
               lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x))
-              lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {{!!}}
-              ... | lt = {!!}
+              lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
+              ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where
+                  lemma5 : od→ord (A ∩ Ord (od→ord t)) ≡ od→ord (A ∩ ord→od (od→ord t))
+                  lemma5 = cong (λ k → od→ord (A ∩ k )) Ord-ord
               lemma2 :  def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
               lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma4 }) ) where
-                  lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
-                  lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) (sym Ord-ord-≡) (∩-≡ t→A ) ))
 
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq