fix: missing `share` when entering telescopes in `Sym.simp`

src/Lean/Meta/Sym/Simp/Forall.lean

diff --git a/src/Lean/Meta/Sym/Simp/Forall.lean b/src/Lean/Meta/Sym/Simp/Forall.lean
index 9d98a35..4032430 100644
--- a/src/Lean/Meta/Sym/Simp/Forall.lean
+++ b/src/Lean/Meta/Sym/Simp/Forall.lean
@@ -81,7 +81,7 @@
   else if (← isProp e) then
     let n := getForallTelescopeSize e.bindingBody! 1
     forallBoundedTelescope e n fun xs b => withoutModifyingCacheIfNotWellBehaved do
-      main xs b
+      main xs (← share b)
   else
     return .rfl
 where
@@ -90,7 +90,7 @@
     | .rfl _ => return .rfl
     | .step b' h _ =>
       let h ← mkLambdaFVars xs h
-      let e' ← shareCommonInc (← mkForallFVars xs b')
+      let e' ← share (← mkForallFVars xs b')
       -- **Note**: consider caching the forall-congr theorems
       let hcongr ← mkForallCongrFor xs
       return .step e' (mkApp3 hcongr (← mkLambdaFVars xs b) (← mkLambdaFVars xs b') h)

src/Lean/Meta/Sym/Simp/Lambda.lean

diff --git a/src/Lean/Meta/Sym/Simp/Lambda.lean b/src/Lean/Meta/Sym/Simp/Lambda.lean
index 7ee3694..98a4d0f 100644
--- a/src/Lean/Meta/Sym/Simp/Lambda.lean
+++ b/src/Lean/Meta/Sym/Simp/Lambda.lean
@@ -48,14 +48,14 @@
 
 public def simpLambda (e : Expr) : SimpM Result := do
   lambdaTelescope e fun xs b => withoutModifyingCacheIfNotWellBehaved do
-    main xs b
+    main xs (← share b)
 where
   main (xs : Array Expr) (b : Expr) : SimpM Result := do
     match (← simp b) with
     | .rfl _ => return .rfl
     | .step b' h _ =>
       let h ← mkLambdaFVars xs h
-      let e' ← shareCommonInc (← mkLambdaFVars xs b')
+      let e' ← share (← mkLambdaFVars xs b')
       let funext ← getFunext xs b
       return .step e' (mkApp3 funext e e' h)