cannot step back across `phoare` lemmas

[oskgo]

MRE:

require import Real.

module M = {proc p()={}}.

phoare p: [M.p: true ==> true] = 1%r.
proof. proc; auto. qed.

Stepping back after stepping over qed does not work, requiring a full restart.

Curiously, the following variation works:

require import Real.

module M = {proc p()={}}.

phoare p: [M.p: true ==> true] = 1%r by proc; auto.

The workaround is to use lemma p: phoare[M.p: true ==> true] = 1%r instead.