--- a/src/ODUtil.agda	Mon Jul 01 07:00:04 2024 +0900
+++ b/src/ODUtil.agda	Mon Jul 01 15:43:35 2024 +0900
@@ -54,6 +54,10 @@
 eq→ (*iso∩ {p} {q}) {x} ⟪ px , qx ⟫ = ⟪ eq← *iso px , eq← *iso qx ⟫
 eq← (*iso∩ {p} {q}) {x} ⟪ px , qx ⟫ = ⟪ eq→ *iso px , eq→ *iso qx ⟫
 
+∩-cong : {A B C D : HOD} → A =h= B → C =h= D → (A ∩ C) =h= (B ∩ D)
+eq→ (∩-cong eq1 eq2) {x} lt = ⟪ eq→ eq1 (proj1 lt) , eq→ eq2 (proj2 lt) ⟫
+eq← (∩-cong eq1 eq2) {x} lt = ⟪ eq← eq1 (proj1 lt) , eq← eq2 (proj2 lt) ⟫
+
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
 power→⊆ A t  PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x))  where
    t1 : {x : HOD }  → t ∋ x → A ∋ x
@@ -82,6 +86,12 @@
       lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
       lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)
 
+∪-cong : {A B C D : HOD} → A =h= B → C =h= D → (A ∪ C) =h= (B ∪ D)
+eq→ (∪-cong {A} {B} {C} {D} eq1 eq2) {x} (case1 lt) = case1 (eq→ eq1 lt)
+eq→ (∪-cong {A} {B} {C} {D} eq1 eq2) {x} (case2 lt) = case2 (eq→ eq2 lt)
+eq← (∪-cong {A} {B} {C} {D} eq1 eq2) {x} (case1 lt) = case1 (eq← eq1 lt)
+eq← (∪-cong {A} {B} {C} {D} eq1 eq2) {x} (case2 lt) = case2 (eq← eq2 lt)
+
 x∪x≡x : { A  : HOD  } → (A ∪ A) =h= A 
 x∪x≡x {A} = record { eq← = λ {x} lt → case1 lt ; eq→ =  lem00 } where
     lem00 : {x : Ordinal} → odef A x ∨ odef A x → odef A x