How to duplicate a hypothesis in Coq?

Question

During a proof, I encountered an hypothesis H. I have lemmas: H -> A and H -> B.

How can I duplicate H in order to deduce two hypotheses A and B ?

edited: More precisely, I have:

lemma l1: X -> A.
lemma l2: X -> B.

1 subgoals, subgoal 1 (ID: 42)
H: X
=========
Y

But, I want to get:

1 subgoals, subgoal 1 (ID: 42)
H1: A
H2: B
=========
Y

Answer 1

If you absolutely need to use an assumption multiple times as you suggested, you can use forward-reasoning tactics such as assert to do so without clearing it from the context, e.g.

assert (HA := l1 H).
assert (HB := l2 H).

You can also do something like assert (H' := H). to explicitly copy H into H', although you can usually resort to a more direct way for getting what you want.

Answer 2

Why do you think that you need to duplicate the hypothesis? If you are using it in a proof, it won't become unavailable. See this example:

Parameter A B H : Type.
Parameter lemma1 : H -> A.
Parameter lemma2 : H -> B.

Goal H -> A * B.
intro; split; [apply lemma1 | apply lemma2]; assumption.
Qed.