对Coq中的两个子目标使用相同的证明

Question

在对归纳类型进行归纳之后，我有两个子目标要证明。假设和目标略有不同，但可以用相同的(长)证据来解决，目前的证据如下：

induction x.
{
  admit.
}
{
  <long proof>
}
{
  <copy-paste of long proof>
}

是否有一种方法可以避免复制粘贴并保持交互性，例如，编写类似于以下内容的东西？

induction x.
{
  admit.
}
all:
{
  <long proof>
}

Answer 1

有时，您可以通过中间引理来解决这些目标：

assert (H : statement_of_lemma).
{ 
  proof...
}

稍后，您只需将H应用于每个子案例。