duplicate a hypothesis

Stream: new members

[Michael Beeson]

Suppose I have a hypothesis h. I need to do something to that hypothesis now, using cases.
But later I need to use hypothesis h. Using cases will "clear" h so it's not available later.
Therefore I need to make a copy of h before I use cases on it. How can I do that? (in tactic mode).

[Alex J. Best]

have h' := h should work

[Michael Beeson]

Thank you!

[Alex J. Best]

You could also restructure the proof so that the cases h is within a { } block, by using suffices or have for your intermediate goals, outside the { } the original h will be left intact