Discarding tautological premises in Coq

I have a hypothesis in the local context, let's call it H which is of the form true=true -> conclusion. Which tactic can I use to discard the p开发者_如何学Goremise and retain only the conclusion?

---

This asserts the premise as a subgoal and then tries to prove both it, and the original goal with the conclusion of H prepended, using the trivial tactic.

lapply H; trivial.

---

Use the specialize tactic: http://coq.inria.fr/doc/Reference-Manual011.html#@tactic35

specialize (H (eq_refl true)).

---

I came up with the following. Either of these works:

assert (H2 : conclusion). apply H. reflexivity.

assert (H2 : true->true). reflexivity. apply H in H2.

assert (H2 := H (eq_refl true)). also works. I would still like to know about cleaner solutions.