rewrite works for = but not for <-> (iff) in Co

Question

I have the following during a proof, in which I need to replace normal_form step t with value t as there is a proven theorem that there are equivalent.

H1 : t1 ==>* t1' /\ normal_form step t1'
t2' : tm
H2 : t2 ==>* t2' /\ normal_form step t2'
______________________________________(1/1)
exists t' : tm, P t1 t2 ==>* t' /\ normal_form step t'

The equivalence theorem is:

Theorem nf_same_as_value
 : forall t : tm, normal_form step t <-> value t

Now, I can use this theorem to rewrite normal_form occurrences in the hypotheses, but not in the goal. That is

rewrite nf_same_as_value in H1; rewrite nf_same_as_value in H2.

works on the hypothesis, but rewrite nf_same_as_value. on the goal gives:

Error:
Found no subterm matching "normal_form step ?4345" in the current goal.

Is the rewrite on the goal here impossible theoretically, or is it an implementation issue?

-- Edit --

My confusion here is that if we define normal_form step = value, the rewrite would have worked. If we define forall t, normal_form step t <-> value t, then the rewrite works if normal_form step is not quoted in an existential, but does not work if it is in an existential.

Adapting @Matt 's example,

Require Export Coq.Setoids.Setoid.
Inductive R1 : Prop -> Prop -> Prop :=
|T1_refl : forall P, R1 P P.

Inductive R2 : Prop -> Prop -> Prop :=
|T2_refl : forall P, R2 P P.

Theorem Requal : R1 = R2. 
Admitted. 

Theorem Requiv : forall x y, R1 x y <-> R2 x y. 
Admitted. 

Theorem test0 : forall y, R2 y y -> exists x, R1 x x. 
Proof.
  intros. rewrite <- Requal in H. (*works*) rewrite Requal. (*works as well*) 

Theorem test2 : forall y, R2 y y -> exists x, R1 x x. 
Proof.
  intros. rewrite <- Requiv in H. (*works*) rewrite Requiv. (*fails*) 

What confuses me is why the last step has to fail.

1 subgoal
y : Prop
H : R1 y y
______________________________________(1/1)
exists x : Prop, R1 x x

Is this failure related to functional extensionality?

The error message is particularly confusing:

Error:
Found no subterm matching "R1 ?P ?P0" in the current goal.

There is exactly one subterm matching R1 _ _, namely R1 x x.

Also, per @larsr, the rewrite works if eexists is used

Theorem test1 : forall y, R2 y y -> exists x, R1 x x. 
Proof.
  intros. eexists. rewrite Requiv. (*works as well*) apply H. Qed.

What did eexists add here?

Answer 1

The rewrite cannot go under the existential quantifier. You'll need to instantiate t' first before you can do the rewrite. Note that econstructor may be a useful tactic in this case, which can replace the existential quantifier with a unification variable.

EDIT in response to OP's comment

This will still not work for equality. As an example, try:

Inductive R1 : Prop -> Prop -> Prop :=
|T1_refl : forall P, R1 P P.

Inductive R2 : Prop -> Prop -> Prop :=
|T2_refl : forall P, R2 P P.

Theorem Req : forall x y, R1 x y = R2 x y. 
Admitted. 

Theorem test : forall y, R2 y y -> exists x, R1 x x. 
Proof.
  intros. rewrite Req. (*rewrite still fails*)

The issue is not actually about equality vs. iff, the issue relates to rewriting under a binding (in this case a lambda). The implementation of exists x : A, P is really just syntax for ex A (fun x => P x), so the rewrite is failing not because of the iff, but because the rewrite tactic does not want to go under the binding for x in (fun x => P x). It seems as though there might be a way to do this with setoid_rewrite, however, I don't have any experience with this.