Coq：证明如果（A，B）=（C，D），则A = C / \ B = D

Question

标题中，我找不到足够的工具来解决这个琐碎的事情：

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

我怎么证明呢？

Answer 1

就知道了。是pair_equal_spec：

Proof.
  intros.
  apply pair_equal_spec.
  assumption.
Qed.