INDUCTIVE DEFINITION
ex4_4 ()
[
A0:Set, A1:Set, A2:Set, A3:Set, :A0→A1→A2→A3→Prop, :A0→A1→A2→A3→Prop, :A0→A1→A2→A3→Prop, :A0→A1→A2→A3→Prop
]
OF ARITY
Prop
BUILT FROM:
ex4_4_intro: ∀x0:A0.∀x1:A1.∀x2:A2.∀x3:A3.(P0 x0 x1 x2 x3)→(P1 x0 x1 x2 x3)→(P2 x0 x1 x2 x3)→(P3 x0 x1 x2 x3)→(ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)