如何破坏Coq中的对等价？

Question

使用Coq时，我试图破坏对等价假设。但是我没有找到适合我的策略。

情况是：

a, b, a', b' : nat
H0 : (a, b) = (a', b')

我想破坏H0中的对以生成

H1 : a = a'
H2 : b = b'

我该如何实现？我应该使用哪种战术？还是应该定义销毁这种对的引理？

谢谢！

Answer 1

首先使用，injection H0然后intros近似。