DEFINITION and5_rec()
TYPE =
       ΠP0:Prop
         .ΠP1:Prop
           .ΠP2:Prop
             .ΠP3:Prop
               .ΠP4:Prop
                 .ΠP:Set.(P0→P1→P2→P3→P4→P)→(and5 P0 P1 P2 P3 P4)→P
BODY =
λP0:Prop
         .λP1:Prop
           .λP2:Prop
             .λP3:Prop
               .λP4:Prop
                 .λP:Set
                   .λf:P0→P1→P2→P3→P4→P
                     .λH:and5 P0 P1 P2 P3 P4.<λH1:and5 P0 P1 P2 P3 P4.P> CASE H OF and5_intro H1 H2 H3 H4 H5⇒f H1 H2 H3 H4 H5