INDUCTIVE DEFINITION ex () [ A:Set, :A→Prop ]
OF ARITY Prop
BUILT FROM:
     ex_intro: ∀x:A.(P x)→(ex A P)