title: rewrite works for = but not for <-> (iff) in Coq
body: <p>I have the following during a proof, in which I need to replace <code>normal_form step t</code> with <code>value t</code> as there is a proven theorem that there are equivalent.</p>
  
  <pre><code>H1 : t1 ==&gt;* t1' /\ normal_form step t1'
  t2' : tm
  H2 : t2 ==&gt;* t2' /\ normal_form step t2'
  ______________________________________(1/1)
  exists t' : tm, P t1 t2 ==&gt;* t' /\ normal_form step t'
  </code></pre>
  
  <p>The equivalence theorem is:</p>
  
  <pre><code>Theorem nf_same_as_value
   : forall t : tm, normal_form step t &lt;-&gt; value t
  </code></pre>
  
  <p>Now, I can use this theorem to rewrite <code>normal_form</code> occurrences in the hypotheses, <strong><em>but not</em></strong> in the goal. That is</p>
  
  <pre><code>rewrite nf_same_as_value in H1; rewrite nf_same_as_value in H2.
  </code></pre>
  
  <p>works on the hypothesis, but <code>rewrite nf_same_as_value.</code> on the goal gives:</p>
  
  <pre><code>Error:
  Found no subterm matching "normal_form step ?4345" in the current goal.
  </code></pre>
  
  <p>Is the <code>rewrite</code> on the goal here impossible theoretically, or is it an implementation issue?</p>
  
  <p>-- Edit --</p>
  
  <p>My confusion here is that if we define <code>normal_form step = value</code>, the rewrite would have worked. If we define <code>forall t, normal_form step t &lt;-&gt; value t</code>, then the <code>rewrite</code> works if <code>normal_form step</code> is not quoted in an existential, but does not work if it is in an existential. </p>
  
  <p>Adapting @Matt 's example,</p>
  
  <pre><code>Require Export Coq.Setoids.Setoid.
  Inductive R1 : Prop -&gt; Prop -&gt; Prop :=
  |T1_refl : forall P, R1 P P.
  
  Inductive R2 : Prop -&gt; Prop -&gt; Prop :=
  |T2_refl : forall P, R2 P P.
  
  Theorem Requal : R1 = R2. 
  Admitted. 
  
  Theorem Requiv : forall x y, R1 x y &lt;-&gt; R2 x y. 
  Admitted. 
  
  Theorem test0 : forall y, R2 y y -&gt; exists x, R1 x x. 
  Proof.
    intros. rewrite &lt;- Requal in H. (*works*) rewrite Requal. (*works as well*) 
  
  Theorem test2 : forall y, R2 y y -&gt; exists x, R1 x x. 
  Proof.
    intros. rewrite &lt;- Requiv in H. (*works*) rewrite Requiv. (*fails*) 
  </code></pre>
  
  <p>What confuses me is why the last step has to fail. </p>
  
  <pre><code>1 subgoal
  y : Prop
  H : R1 y y
  ______________________________________(1/1)
  exists x : Prop, R1 x x
  </code></pre>
  
  <p>Is this failure related to functional extensionality?</p>
  
  <p>The error message is particularly confusing:</p>
  
  <pre><code>Error:
  Found no subterm matching "R1 ?P ?P0" in the current goal.
  </code></pre>
  
  <p>There is exactly one subterm matching <code>R1 _ _</code>, namely R1 x x. </p>
  
  <p>Also, per @larsr, the rewrite works if <code>eexists</code> is used</p>
  
  <pre><code>Theorem test1 : forall y, R2 y y -&gt; exists x, R1 x x. 
  Proof.
    intros. eexists. rewrite Requiv. (*works as well*) apply H. Qed.
  </code></pre>
  
  <p>What did <code>eexists</code> add here?</p>