coqcoq-tacticcoqide

How to prove the same subgoals

I have two equal subgoals like this:

prove_me (x::xs) = true

prove_me (x::xs) = true

Proofs will be equals. How I can solve the second goal using the first one?

Solution

  • You cannot literally reuse the proof of one goal on another goal, but you can prove an auxiliary lemma:

    assert (H : prove_me (x::xs) = true).
{ (* proof of result *) }

    Then, you can use H to discharge the two subgoals once they show up.