∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ : Type u}
  {Q : Std.Do.PostCond PUnit.{u + 1} (Std.Do.PostShape.arg σ ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  (x : σ), (Std.Do.wp (set x)).apply Q = fun x_1 => Q.1 PUnit.unit x