Используя одно и то же доказательство для двух подцелей в 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 к каждому подслучаю.