Anomaly when trying to use `proc` on a goal with `Pr`

[oskgo]

This is purely a diagnostics bug. The following code throws an anomaly when it should print an error:

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

lemma L &m: Pr[M.p() @&m: true] = Pr[M.p() @&m: true].
proof. proc.