DEFINITION and5_ind() TYPE = ∀P0:Prop .∀P1:Prop .∀P2:Prop .∀P3:Prop.∀P4:Prop.∀P:Prop.(P0→P1→P2→P3→P4→P)→(and5 P0 P1 P2 P3 P4)→P BODY =Show proof