diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean
index f43faa43f0..031f9be542 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean
@@ -181,6 +181,10 @@ partial def reduceProjBeta? (e : Expr) : MetaM (Option Expr) :=
           let e' := mkAppRev f' rargs
           go (some e') e'.getAppFn e'.getAppRevArgs
         | none    => pure lastReduction
+      | .letE x ty val body nondep =>
+        match ← go none body rargs with
+        | none => pure lastReduction
+        | some body' => pure (some (.letE x ty val body' nondep))
       | _ => pure lastReduction
 
 def mkSpecContext (optConfig : Syntax) (lemmas : Syntax) (ignoreStarArg := false) : TacticM Context := do
diff --git a/tests/lean/run/mvcgenTutorial.lean b/tests/lean/run/mvcgenTutorial.lean
index e2991f2de5..4588f7665b 100644
--- a/tests/lean/run/mvcgenTutorial.lean
+++ b/tests/lean/run/mvcgenTutorial.lean
@@ -115,6 +115,11 @@ def mkFreshN (n : Nat) : AppM (List Nat) := do
     acc := acc.push n
   return acc.toList
 
+theorem mkFreshN_spec_noncompositional (n : Nat) : ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by
+  mvcgen [mkFreshN, mkFresh, liftCounterM]
+  case inv1 => exact ⇓⟨xs, acc⟩ _ state => ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝
+  all_goals mleave; grind
+
 @[spec]
 theorem mkFresh_spec [Monad m] [WPMonad m ps] (c : Nat) :
     ⦃fun state => ⌜state.counter = c⌝⦄ mkFresh (m := m) ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by