Coq rewrite tactic can't find subterm

Question

I writing a proof in coq and I'm trying to use the rewrite tactic. I wanted to include a minimal working example but there are quite a lot of things I would have to include (this proof is building on previous work of my own). Let me know if it is necessary and I can get a working example uploaded. Otherwise: My current goal is:

1 subgoal
A : Type
a : A
h : eq_refl a = eq_refl a
______________________________________(1/1)
eq_refl (eq_refl a) * h * eq_refl (eq_refl a) = h

I have defined the notation * to be path concatenation (or just using transativity on proofs of equality). Now is where I look to apply rewrite on the lhs of the goal equality. I have a path from the term on the lhs to h * eq_refl given by ap(fun (p : eq_refl a = eq_refl a) => p * eq_refl(eq_refl a)) (pinv (refllid h))) (sorry for the notation, I'm doing HoTT. ap takes p : a = b to (ap f p) : f a = f b) for any f). I can confirm this with Check:

ap (fun (p : eq_refl = eq_refl) => p * eq_refl) (pinv (refllid h))
     : eq_refl * h * eq_refl = h * eq_refl

I also made sure to check that the eq_refl s are really eq_refl (eq_refl a) by checking things with all implicit arguments printed. But, if I try

rewrite (ap(fun (p : eq_refl a = eq_refl a) => p * eq_refl(eq_refl a)) (pinv (refllid h))).

I get the error

Found no subterm matching "eq_refl * h * eq_refl" in the current goal.

But there is quite clearly a subterm of this form. I don't understand why Coq is getting snagged here.

** Edit ** I was able to (laboriously) get the proof to work by using eq_rect. But if I'm not mistaken, rewrite is based on eq_rect. Also I really don't want to have to use eq_rect each time. So I'd still love any input on what went wrong with rewrite.