performance improvements to prove_refinement...

- totally remove `MaybeDestructArg`
  - instead, induction is triggered for each datatype in specific cases
    which are added to the hint database totally normally
  - infinite induction loops are avoided using dummy datatype `DidInduction`
- add `NoRewrite` option to `prove_refinement`, clean up the definitions of
  `prove_refinement` and its variants
- tweak when equalities are actually rewritten
- only inject and disciminate equalities on known constructor pairings
- replace `apply IntroArg_unfold; intro e` with just `intro e`
- replace all instances of `rewrite`s on known lemmas in `Hint Externs` with
  `apply` on a new lemma whose proof is just rewriting by the original lemma
  (this is faster since `rewrite` is slow)
- replace some instances of `Hint Resolve` with `Hint Extern`
- replace `autorewrite with SAWCoreBitvectors` with explicit rules on
  `IntroArg`s and a much smaller `autorewrite with SAWCoreBitvectors_eqs`
- re-define `bvNat` in a way that makes it work with `compute_bv_funs`

coq/handwritten/CryptolToCoq/CompM.v

@@ -923,3 +923,10 @@ Lemma refinesM_assumingM_l {A} (P:Prop) (m1 m2 : CompM A) :
 Proof.
   apply refinesM_forallM_l.
 Qed.
+
+(* NOTE: the other direction does not hold *)
+Lemma assumingM_bindM {A B} (P:Prop) (m: CompM A) (Q: A -> CompM B) :
+  refinesM ((assumingM P m) >>= Q) (assumingM P (m >>= Q)).
+Proof.
+  apply forallM_bindM.
+Qed.