fix: simp have in Sym (#12370)

This PR fixes a proof construction bug in `Sym.simp`.

Closes #12336

Author: leodemoura

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

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