INDUCTIVE DEFINITION ex_2 () [ A0:Set, A1:Set, :A0→A1→Prop ]
OF ARITY Prop
BUILT FROM:
     ex_2_intro: ∀x0:A0.∀x1:A1.(P0 x0 x1)→(ex_2 A0 A1 P0)