∀ {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 : ReaderT ρ m α) (Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)),
  (Std.Do.wp (MonadFunctor.monadMap (fun {β} => f) x)).apply Q = fun s =>
    (Std.Do.wp (f (x.run s))).apply (fun a => Q.1 a s, Q.2)