JasonGross: You can do Local Notation pip P := (forall p1 p2 : P, p1 = p2).