--- a/src/ODUtil.agda	Sun Jan 01 17:02:54 2023 +0900
+++ b/src/ODUtil.agda	Sun Jan 01 20:03:29 2023 +0900
@@ -32,6 +32,15 @@
 _⊂_ : ( A B : HOD) → Set n
 _⊂_ A B = ( & A o< & B) ∧ ( A ⊆ B )
 
+⊆∩-dist : {a b c : HOD} → a ⊆ b → a ⊆ c  →  a ⊆ ( b ∩ c )
+⊆∩-dist {a} {b} {c} a<b a<c {z} az = ⟪ a<b az , a<c az ⟫
+
+⊆∩-incl-1 : {a b c : HOD} → a ⊆ c → ( a ∩ b ) ⊆ c
+⊆∩-incl-1 {a} {b} {c} a<c {z} ab = a<c (proj1 ab)
+
+⊆∩-incl-2 : {a b c : HOD} → a ⊆ c → ( b ∩ a ) ⊆ c
+⊆∩-incl-2 {a} {b} {c} a<c {z} ab = a<c (proj2 ab)
+
 cseq :  HOD  →  HOD
 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
     lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)