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

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?

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.