diff --git a/src/Lean/Meta/Sym/Simp/Have.lean b/src/Lean/Meta/Sym/Simp/Have.lean
index d0d648023c..95a3a61de9 100644
--- a/src/Lean/Meta/Sym/Simp/Have.lean
+++ b/src/Lean/Meta/Sym/Simp/Have.lean
@@ -318,12 +318,13 @@ For each application `f a`:
 -/
 def simpBetaApp (e : Expr) (fType : Expr) (fnUnivs argUnivs : Array Level)
     (simpBody : Simproc) : SimpM Result := do
-  return (← go e 0).1
+  let numArgs := argUnivs.size
+  return (← go e (numArgs - 1)).1
 where
   go (e : Expr) (i : Nat) : SimpM (Result × Expr) := do
     match e with
     | .app f a =>
-      let (rf, fType) ← go f (i+1)
+      let (rf, fType) ← go f (i-1)
       let r ← match rf, (← simp a) with
         | .rfl _, .rfl _ =>
           pure .rfl
diff --git a/tests/lean/run/sym_cbv_12336.lean b/tests/lean/run/sym_cbv_12336.lean
new file mode 100644
index 0000000000..3e1e8a82ab
--- /dev/null
+++ b/tests/lean/run/sym_cbv_12336.lean
@@ -0,0 +1,5 @@
+import Std
+set_option cbv.warning false
+
+def test : ((Std.TreeSet.empty : Std.TreeSet Nat).insertMany [1]).toList = [1] := by
+  conv => lhs; cbv