diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean
index c02705271d..5309c40305 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@@ -409,5 +409,5 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
   -- but optConfig is not a leading_parser, and neither is the syntax for `lemmas`
   let ctx ← mkSpecContext stx[1] stx[2]
   let vcs ← genVCs (← getMainGoal) ctx (fuel := .unlimited)
-  let tac ← `(tactic| try (apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro); trivial))
+  let tac ← `(tactic| try ((try apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro)); trivial))
   for vc in vcs do discard <| runTactic vc tac
diff --git a/tests/lean/run/9362.lean b/tests/lean/run/9362.lean
new file mode 100644
index 0000000000..e938cd2ce7
--- /dev/null
+++ b/tests/lean/run/9362.lean
@@ -0,0 +1,20 @@
+import Std.Tactic.Do
+
+open Std.Do
+
+set_option mvcgen.warning false
+
+axiom G (lt : Nat) : Id Unit
+
+noncomputable def F : Id Unit := do
+  G 1
+
+axiom P : Prop
+
+@[spec]
+axiom G_spec (h : P) :
+   ⦃⌜True⌝⦄ G 1 ⦃⇓ _ => ⌜0 < 1⌝⦄
+
+theorem F_spec (h : P) :
+   ⦃⌜True⌝⦄ F ⦃⇓ _ => ⌜0 < 1⌝⦄ := by
+  mvcgen [F] -- should close (h : P ⊢ P) by trivial