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

The following emits `anomaly: Failure("no default exception")`.
```
module M = {proc p() = {}}.

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