∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε : Type u_1} {α : Type u} {x : m α} {h : ε → m α}
  {Q : Std.Do.PostCond α ps} [inst : MonadExceptOf ε m] [inst_1 : Std.Do.WP m ps],
  (Std.Do.wp (tryCatch x h)).apply Q = (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q