fix: bv_omega to use -implicitDefEqProofs (#7387)

This PR uses `-implicitDefEqProofs` in `bv_omega` to ensure it is not
affected by the change in #7386.

---------

Co-authored-by: Leonardo de Moura <leomoura@amazon.com>

src/Init/Tactics.lean

@@ -1347,7 +1347,7 @@ syntax (name := omega) "omega" optConfig : tactic
 Currently the preprocessor is implemented as `try simp only [bitvec_to_nat] at *`.
 `bitvec_to_nat` is a `@[simp]` attribute that you can (cautiously) add to more theorems.
 -/
-macro "bv_omega" : tactic => `(tactic| (try simp only [bitvec_to_nat] at *) <;> omega)
+macro "bv_omega" : tactic => `(tactic| (try simp -implicitDefEqProofs only [bitvec_to_nat] at *) <;> omega)
 
 /-- Implementation of `ac_nf` (the full `ac_nf` calls `trivial` afterwards). -/
 syntax (name := acNf0) "ac_nf0" (location)? : tactic

src/kernel/type_checker.cpp

@@ -618,7 +618,6 @@ template<typename F> optional<expr> type_checker::reduce_bin_nat_pred(F const &
 }
 
 optional<expr> type_checker::reduce_nat(expr const & e) {
-    if (has_fvar(e)) return none_expr();
     unsigned nargs = get_app_num_args(e);
     if (nargs == 1) {
         expr const & f = app_fn(e);