title: Coq rewrite tactic can't find subterm
body: <p>I writing a proof in coq and I'm trying to use the <code>rewrite</code> 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:</p>
  <pre><code>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
  </code></pre>
  <p>I have defined the notation <code>*</code> to be path concatenation (or just using transativity on proofs of equality). Now is where I look to apply <code>rewrite</code> on the lhs of the goal equality. I have a path from the term on the lhs to <code>h * eq_refl</code> given by <code>ap(fun (p : eq_refl a = eq_refl a) =&gt; p * eq_refl(eq_refl a)) (pinv (refllid h)))</code> (sorry for the notation, I'm doing HoTT. <code>ap</code> takes p : a = b to (ap f p) : f a = f b) for any f). I  can confirm this with <code>Check</code>:</p>
  <pre><code>ap (fun (p : eq_refl = eq_refl) =&gt; p * eq_refl) (pinv (refllid h))
       : eq_refl * h * eq_refl = h * eq_refl
  </code></pre>
  <p>I also made sure to check that the <code>eq_refl</code> s are really <code>eq_refl (eq_refl a)</code> by checking things with all implicit arguments printed. But, if I try</p>
  <pre><code>rewrite (ap(fun (p : eq_refl a = eq_refl a) =&gt; p * eq_refl(eq_refl a)) (pinv (refllid h))).
  </code></pre>
  <p>I get the error</p>
  <pre><code>Found no subterm matching &quot;eq_refl * h * eq_refl&quot; in the current goal.
  </code></pre>
  <p>But there is quite clearly a subterm of this form. I don't understand why Coq is getting snagged here.</p>
  <p>** Edit ** I was able to (laboriously) get the proof to work by using <code>eq_rect</code>. But if I'm not mistaken, <code>rewrite</code> is based on <code>eq_rect</code>. Also I really don't want to have to use <code>eq_rect</code> each time. So I'd still love any input on what went wrong with <code>rewrite</code>.</p>