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