coq - 如何在 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作为第一个近似值。