DEFINITION and4_ind() TYPE = ∀P0:Prop .∀P1:Prop.∀P2:Prop.∀P3:Prop.∀P:Prop.(P0→P1→P2→P3→P)→(and4 P0 P1 P2 P3)→P BODY =Show proof