Rewriting under `cvg_to` Fails

[Yosuke-Ito-345]

In probability.v, I would like to rewrite the function under cvg_to by

eq_cvg : forall (T T' : Type) (F : set_system T) (f g : T -> T') (x : set_system T'),
  f =1 g -> (f x @[x --> F] --> x) = (g x @[x --> F] --> x)

The minimal working example is

Lemma eq_cvg_fail (R : realType) : (n - n)%:R@[n --> \oo] --> (0:R).
Proof.
under eq_cvg=> n.
  rewrite subnn.
  over.

I expect the result to be something like

0%R@[n --> \oo] --> (0:R).

but the actual proof state is

forall t : set R,
nbhs [set P | (exists2 i : R, [set e | 0 < e] i & ball_ [eta normr] 0 i `<=` P)] t ->
nbhs (0 @[_ --> \oo]) t

This goal is correct but cvg_to is unfolded unintentionally according to @CohenCyril. I hope this would be fixed. You can find the full code in the attached file eq_cvg_fail.txt. The original file was eq_cvg_fail.v. I changed the extension from .v to .txt because GitHub rejected .v.