tactics: change guard check

Allow for the SMT to help discharging it, since some examples Nick ran
into require it. However, I'd like to revisit this throughout the
engine: when do we consider it acceptable to call the SMT during tactics
execution? I'd like to say never, but not sure how feasible that is.

Example file was:

```
module Test
open FStar.BV
open FStar.Tactics
open FStar.Tactics.BV
module U = FStar.UInt

val lemma_test: x:U.uint_t 64 ->
  Lemma (U.logand #64 x 0 == 0)
let lemma_test x =
 assert_by_tactic (bv_tac ()) (U.logand #64 x 0 == (0 <: uint_t' 64))
```

over commit a50b225

It seems the SMT is needed for deciding equality of two types,
`uint_t 64` and `uint_t' 64`, which have the same definition but the
typechecker can discharge this by itself. They are refinements,
but have the same definition. So maybe the typechecker discharges the
bi-implication instead of noticing the equality.

For now, bite the bullet and call z3.

src/tactics/FStar.Tactics.Basic.fs

@@ -524,7 +524,7 @@ let apply_lemma (tm:term) : tac<unit> =
                                  (Print.term_to_string (U.mk_squash post))
                                  (Print.term_to_string goal.goal_ty)
     | Some g ->
-        let _ = Rel.discharge_guard_no_smt goal.context g in
+        let _ = Rel.discharge_guard goal.context g in
         let solution = S.mk_Tm_app tm uvs None goal.context.range in
         let implicits = implicits.implicits |> List.filter (fun (_, _, _, tm, _, _) ->
              let hd, _ = U.head_and_args tm in