INDUCTIVE DEFINITION
ex3_2 ()
[
A0:Set, A1:Set, :A0→A1→Prop, :A0→A1→Prop, :A0→A1→Prop
]
OF ARITY
Prop
BUILT FROM:
ex3_2_intro: ∀x0:A0.∀x1:A1.(P0 x0 x1)→(P1 x0 x1)→(P2 x0 x1)→(ex3_2 A0 A1 P0 P1 P2)