INDUCTIVE DEFINITION
ex_3 ()
[
A0:Set, A1:Set, A2:Set, :A0→A1→A2→Prop
]
OF ARITY
Prop
BUILT FROM:
ex_3_intro: ∀x0:A0.∀x1:A1.∀x2:A2.(P0 x0 x1 x2)→(ex_3 A0 A1 A2 P0)