rewrite fails with abbrev

[cassiersg]

The following behavior is not expected (tested on release 2025.02):

require import AllCore.

op a (i:int) : int.
abbrev b (i:int) : int = a i.
lemma bE i: b i = 0. admitted.
abbrev c = b.
abbrev d i = b i.

(* These work as expected. *)
lemma b_apply (i:int): b i = 0. proof. apply bE. qed.
lemma b_rewrite (i:int): b i = 0. proof. by rewrite bE. qed.

lemma c_apply (i:int): c i = 0. proof. apply bE. qed.

lemma d_apply (i:int): d i = 0. proof. apply bE. qed.
lemma d_rewrite (i:int): d i = 0. proof. by rewrite bE. qed.

(* Fails "nothing to rewrite". *)
lemma c_rewrite (i:int): c i = 0. proof. by rewrite bE. qed.

[strub]

Here is the problem reduces:

require import AllCore.

op a : int -> int.

axiom A : forall x, a x = 0.

lemma L : (fun x => a x) 0 = 0.
proof. by rewrite A. qed.