perf: avoid "dependent implications" as local E-matching theorems in grind

This PR implements a simple optimization: dependent implications are
no longer treated as E-matching theorems in `grind`. In
`grind_bitvec2.lean`, this change saves around 3 seconds, as many
dependent implications are generated. Example:
```lean
 ∀ (h : i + 1 ≤ w), x.abs.getLsbD i = x.abs[i]
 ```

src/Lean/Meta/Tactic/Grind/ForallProp.lean

@@ -107,7 +107,16 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
       addNewRawFact h' e' (← getGeneration e) (.forallProp e)
     else
       if b.hasLooseBVars then
-        addLocalEMatchTheorems e
+        unless (← isProp a) do
+          /-
+          We used to waste a lot of time trying to process terms such as
+          ```
+          ∀ (h : i + 1 ≤ w), x.abs.getLsbD i = x.abs[i]
+          ```
+          as E-matching theorems. They are "dependent" implications, and should be handled
+          by `propagateForallPropUp`.
+          -/
+          addLocalEMatchTheorems e
       else
         unless (← alreadyInternalized b) do return ()
         if (← isEqFalse b <&&> isProp a) then