How to prove the same subgoals

Question

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?

Answer 1

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.