--- a/OD.agda	Sun Jul 26 21:39:27 2020 +0900
+++ b/OD.agda	Mon Jul 27 09:29:41 2020 +0900
@@ -495,6 +495,9 @@
   ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
   }
 
+selection-in-domain : {ψ : HOD → Set n} {X y : HOD} → Select X ψ ∋ y → X ∋ y 
+selection-in-domain {ψ} {X} {y} lt = proj1 ((proj2 (selection {ψ} {X} )) lt)
+
 sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y))))
 sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt )
 replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x