(* internal existential quantification *)
inductive dex (D:Domain) (P:D → Prop): Prop ≝
| dex_intro: ∀d. cin D d → P d → dex D P
.
(* internal existential quantification *)
inductive dex (D:Domain) (P:D → Prop): Prop ≝
| dex_intro: ∀d. cin D d → P d → dex D P
.