--- a/src/ODC.agda	Thu Sep 08 09:16:51 2022 +0900
+++ b/src/ODC.agda	Thu Sep 08 12:44:22 2022 +0900
@@ -88,6 +88,13 @@
 ... | yes p = p
 ... | no ¬p = ⊥-elim ( notnot ¬p )
 
+or-exclude : {A B : Set n} → A ∨ B → A ∨ ( (¬ A)  ∧  B )
+or-exclude {A} {B} ab with p∨¬p A
+or-exclude {A} {B} (case1 a) | case1 a0 = case1 a
+or-exclude {A} {B} (case1 a) | case2 ¬a = ⊥-elim ( ¬a a )
+or-exclude {A} {B} (case2 b) | case1 a = case1 a
+or-exclude {A} {B} (case2 b) | case2 ¬a = case2 ⟪ ¬a , b ⟫
+
 open _⊆_
 
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A