Proof irrelevance

Note: You can do `Local Notation pip P := (forall p1 p2 : P, p1 = p2).`, and then you don't need `at level 80`, and don't make `pip` into a symbol.  (Also, I'm curious, why `pip`, rather than `uip`?)