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 =
Show proof