DEFINITION and3_rec() TYPE = ΠP0:Prop .ΠP1:Prop.ΠP2:Prop.ΠP:Set.(P0→P1→P2→P)→(and3 P0 P1 P2)→P BODY =Show proof