In Coq, what tactic can I use to remove a True precondition from a hypothesis

Question

One of my hypothesis is an implication with an always-true condition (x=x->P). What tactic can I use to rewrite this hypothesis into its conclusion P? The only way I could think of is an awkward combination of assert, apply, and rename. There ought to be a better way.

Theorem myexample: forall T (x: T) (P: Prop), (x = x -> P) -> P.
Proof.
  intros T x P H.
  (* At this point, the hypothesis is "H: x=x->P" *)
  assert (H': x=x). { reflexivity. }
  apply H in H'. clear H. rename H' into H.
  (* Now the hypothesis is "H: P" *)
  apply H.
Qed.

ps.: In this particular example, we could also prove with apply H; reflexivity. But my question is about how to clean up the hypothesis without touching the goal.

Answer 1

You can use specialize tactic

specialize (H eq_refl).

eq_refl is a constructor of type eq, which is hiding behind the = notation

Another way, if your hypothesis have something non-trivial in premise, is to construct it using tactics (tactics in terms)

As you mentioned yourself, premise of H can be constructed using reflexivity, so here it is:

specialize (H ltac:(reflexivity)).

Answer 2

If you use ssreflect, you can, after the intros, use:

move: (H erefl) => {}H.