From 4c44f4ef7c17ee62aa61bc7be3491b554d262c2d Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Wed, 24 Sep 2025 16:32:08 +0200
Subject: [PATCH] chore: add fixed test case for #9363 (#10547)

---
 tests/lean/run/9363.lean | 44 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 tests/lean/run/9363.lean

diff --git a/tests/lean/run/9363.lean b/tests/lean/run/9363.lean
new file mode 100644
index 0000000000..30e3daa1fc
--- /dev/null
+++ b/tests/lean/run/9363.lean
@@ -0,0 +1,44 @@
+import Std.Tactic.Do
+
+open Std.Do
+
+set_option mvcgen.warning false
+
+axiom P : Nat → Prop
+axiom P' : Nat → Prop
+axiom Q : Nat → Prop
+axiom R : Assertion ps
+
+axiom hPQ : ∀ n, P n → P' n → Q n
+
+axiom G : StateM Nat Unit
+axiom H : StateM Nat Unit
+
+noncomputable def F : StateM Nat Unit := do
+  G
+  H
+
+@[spec]
+axiom G_spec : ⦃⌜True⌝⦄ G ⦃⇓ _ n => ⌜P n ∧ P' n⌝⦄
+
+@[spec]
+axiom H_spec : ⦃fun n => ⌜Q n⌝⦄ H ⦃⇓ _ => R⦄
+
+theorem F_spec :
+   ⦃⌜True⌝⦄
+   F
+   ⦃⇓ _ => R⦄ := by
+  mvcgen [F]
+
+  -- Goal:
+  -- s✝¹ : Nat
+  -- r✝ : Unit
+  -- s✝ : Nat
+  -- h : P s✝ ∧ P' s✝
+  -- ⊢ Q s✝
+
+  rename_i h
+  cases h
+  apply hPQ
+  assumption
+  assumption