DEFINITION and3_rec()
TYPE =
ΠP0:Prop
.ΠP1:Prop.ΠP2:Prop.ΠP:Set.(P0→P1→P2→P)→(and3 P0 P1 P2)→P
BODY =
λP0:Prop
.λP1:Prop
.λP2:Prop
.λP:Set.λf:P0→P1→P2→P.λH:and3 P0 P1 P2.<λH1:and3 P0 P1 P2.P> CASE H OF and3_intro H1 H2 H3⇒f H1 H2 H3