Anomaly when using `conseq` with exceptions on a `hoare` goal without

[oskgo]

The following emits anomaly: Failure("no default exception").

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

lemma L: hoare[M.p: true ==> true].
proof.
conseq (: _ ==> _ | _ => true).