Coq: prove that if (A, B) = (C, D) then A = C /\ B = D

Question

As in title, I cannot find sufficient tools to solve this trivial thing:

p : (A, B) = (C, D)
------------
A = C /\ B = D

How can I prove it?

Answer 1

Just got it. It was pair_equal_spec:

Proof.
  intros.
  apply pair_equal_spec.
  assumption.
Qed.