∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε : Type u} [Monad m] [inst : Std.Do.WP m ps]
  (f : {β : Type u} → m β → m β) {α : Type u} (x : ExceptT ε m α)
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)),
  ⦃(Std.Do.wp (f x.run)).apply (fun e => Except.casesOn e Q.2.1 Q.1, Q.2.2)⦄ MonadFunctor.monadMap (fun {β} => f) x ⦃Q⦄