title: Rewrite tactic fails to find term occurrence within pattern matching
body: <p>In Coq, I'm having problems with applying the <code>rewrite</code> tactic in the following situation:</p>
  
  <pre><code>Section Test.
  
  Hypothesis s t        : nat -&gt; nat.
  Hypothesis s_ext_eq_t : forall (x : nat), s x = t x.
  
  Definition dummy_s : nat -&gt; nat :=
    fun n =&gt; match n with
           | O =&gt; 42
           | S np =&gt; s np
         end.
  
  Definition dummy_t : nat -&gt; nat :=
    fun n =&gt; match n with
           | O =&gt; 42
           | S np =&gt; t np
         end.
  
  Goal forall (n : nat), dummy_s n = dummy_t n.
  Proof.
    intro n. unfold dummy_s. unfold dummy_t.
  </code></pre>
  
  <p>At that stage, the local context and current goal look as follows:</p>
  
  <pre><code>1 subgoals, subgoal 1 (ID 6)
  
  s : nat -&gt; nat
  t : nat -&gt; nat
  s_ext_eq_t : forall x : nat, s x = t x
  n : nat
  ============================
  match n with
  | 0 =&gt; 42
  | S np =&gt; s np
  end = match n with
        | 0 =&gt; 42
        | S np =&gt; t np
        end
  </code></pre>
  
  <p>Now it should be possible to apply the <code>rewrite</code> tactic to replace the occurence of <code>s np</code> in the goal by <code>t np</code>, thereby making it possible to solve the goal using <code>reflexivity</code>. However,</p>
  
  <pre><code>rewrite s_ext_eq_t.
  </code></pre>
  
  <p>gives</p>
  
  <pre><code>Toplevel input, characters 0-18:
  Error: Found no subterm matching "s ?190" in the current goal.
  </code></pre>
  
  <p>What am I doing wrong? One <em>can</em> get into a situation where <code>rewrite</code> is applicable via</p>
  
  <pre><code> destruct n. 
     (* n = 0 *)
     reflexivity.
     (* n &gt; 0 *)
     rewrite s_ext_eq_t.
     reflexivity.
   Qed.
  </code></pre>
  
  <p>but in the actual situation I am facing, several such destructs would be necessary, and I wonder whether <code>rewrite</code> or a variant of it is able to do this automatically.</p>
  
  <hr>
  
  <p><em>Addendum</em> The above situation naturally occurs when proving that a function defined via well-founded recursion has the desired fixed point property: </p>
  
  <p>Suppose <code>A: Type</code> and that <code>R: A -&gt; A -&gt; Prop</code> is a well-founded relation, i.e. we have <code>Rwf: well_founded R</code>. Then, given a type family <code>P: A -&gt; Type</code> we may construct a section</p>
  
  <pre><code>Fix : forall (x : A), P a
  </code></pre>
  
  <p>through recursion over <code>R</code>, with the recursion step given as a function </p>
  
  <pre><code> F : forall x:A, (forall y:A, R y x -&gt; P y) -&gt; P x
  </code></pre>
  
  <p>See <a href="https://coq.inria.fr/library/Coq.Init.Wf.html" rel="noreferrer">https://coq.inria.fr/library/Coq.Init.Wf.html</a> However, to show that <code>Fix</code> indeed has the fixed point property</p>
  
  <pre><code>  forall (x : A), Fix x = F (fun (y:A) _ =&gt; Fix y)`
  </code></pre>
  
  <p>we need to provide a witness </p>
  
  <pre><code>  F_ext : forall (x:A) (f g:forall y:A, R y x -&gt; P y),
               (forall (y:A) (p:R y x), f y p = g y p) -&gt; F f = F g.
  </code></pre>
  
  <p>i.e. we have to show that <code>F</code> does not use anything else from the given <code>f: forall y:A, R y x -&gt; P y</code> but its values. Of course, in any concrete situation, this should be trivial to verify, but when one tries to prove it, one runs into a situation a minimal example of which I have presented above: One is facing a huge equality of two copies of the code for the recursion step, one time with <code>f</code> and another time with <code>g</code>. Your assumption tells  that <code>f</code> and <code>g</code> are extensionally equal, so one should be able to rewrite them. However, in the code for the recursion step, there might be a large number of pattern matchings and new variables that doesn't make sense in the local context, hence it would be (unnecessarily?) quite tedious to <code>destruct</code> dozens of times before being allowed to apply <code>rewrite</code>.</p>