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

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.

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)).

• When I tried using eq_refl, I got an error saying: The term "eq_refl" has type "RelationClasses.Reflexive Logic.eq" while it is expected to have type "x = x". Turns out that I had Imported another module that shadowed the definition of eq_refl. My workaround was specialize (H Coq.Init.Logic.eq_refl). Commented Mar 18 at 16:45

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

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