∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {o : Type u → Type u_1} {n : Type u → Type u_2} {α : Type u}
  {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP o ps] [inst_1 : MonadControl n o] [inst_2 : MonadControlT m n]
  (x : stM m o α), ⦃(Std.Do.wp (MonadControl.restoreM (restoreM x))).apply Q⦄ restoreM x ⦃Q⦄