DEFINITION and4_rec()
TYPE =
ΠP0:Prop
.ΠP1:Prop
.ΠP2:Prop
.ΠP3:Prop.ΠP:Set.(P0→P1→P2→P3→P)→(and4 P0 P1 P2 P3)→P
BODY =
λP0:Prop
.λP1:Prop
.λP2:Prop
.λP3:Prop
.λP:Set
.λf:P0→P1→P2→P3→P.λH:and4 P0 P1 P2 P3.<λH1:and4 P0 P1 P2 P3.P> CASE H OF and4_intro H1 H2 H3 H4⇒f H1 H2 H3 H4