add pair_equiv

When having H: (a1, b1) ≡ (a2, b2), it's actually rather annoying to rewrite an a1 in the goal:

destruct H as [H _]; simpl in H; rewrite H

This is because destructing H yields (a1, b1).1 ≡ (a2, b2).1.

So a lemma like this could be useful, then we should be able to do apply pair_equiv in H as [-> _].