∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α β : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  (f : m (α → β)) (x : m α) (Q : Std.Do.PostCond β ps),
  (Std.Do.wp (f <*> x)).apply Q = (Std.Do.wp f).apply (fun f => (Std.Do.wp x).apply (fun a => Q.1 (f a), Q.2), Q.2)