diff --git a/coq/handwritten/CryptolToCoq/CompMExtra.v b/coq/handwritten/CryptolToCoq/CompMExtra.v
index fcc6a993..e96792e1 100644
--- a/coq/handwritten/CryptolToCoq/CompMExtra.v
+++ b/coq/handwritten/CryptolToCoq/CompMExtra.v
@@ -7,7 +7,6 @@ From Coq          Require Import Strings.String.
 From CryptolToCoq Require Import SAWCorePrelude.
 From CryptolToCoq Require Import SAWCoreScaffolding.
 From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
-From CryptolToCoq Require Import SAWCoreBitvectors.
 From CryptolToCoq Require Export CompM.
 
 (***
@@ -141,7 +140,6 @@ Ltac argName n :=
   | Either   => fresh "e_either"
   | Maybe    => fresh "e_maybe"
   | SigT     => fresh "e_either"
-  | If0      => fresh "e_if"
   | If       => fresh "e_if"
   | Assert   => fresh "e_assert"
   | Assuming => fresh "e_assuming"
@@ -149,20 +147,27 @@ Ltac argName n :=
   | Forall   => fresh "e_forall"
   end.
 
+Definition FreshIntroArg (_ : ArgName) A (goal : A -> Prop) := forall a, goal a.
+
 Definition IntroArg (_ : ArgName) A (goal : A -> Prop) := forall a, goal a.
 
+Lemma unFreshIntroArg n A goal : IntroArg n A goal -> FreshIntroArg n A goal.
+Proof. unfold FreshIntroArg, IntroArg; auto. Qed.
+
+Hint Extern 999 (FreshIntroArg ?n ?T ?goal) => simple apply (unFreshIntroArg n T goal) : refinesFun.
+
 Lemma IntroArg_fold n A goal : forall a, IntroArg n A goal -> goal a.
 Proof. unfold IntroArg; intros a H; exact (H a). Qed.
 
 (* Lemma IntroArg_unfold n A (goal : A -> Prop) : (forall a, goal a) -> IntroArg n A goal. *)
 (* Proof. unfold IntroArg; intro H; exact H. Qed. *)
 
-Ltac IntroArg_intro e := (* apply IntroArg_unfold; *) intro e; unfold_projs in e.
+Ltac IntroArg_intro e := intro e; unfold_projs in e.
 
 Ltac IntroArg_forget := let e := fresh in intro e; clear e.
 
 Lemma IntroArg_and n P Q (goal : P /\ Q -> Prop)
-  : IntroArg n P (fun p => IntroArg n Q (fun q => goal (conj p q))) -> IntroArg n _ goal.
+  : IntroArg n P (fun p => FreshIntroArg n Q (fun q => goal (conj p q))) -> IntroArg n _ goal.
 Proof. unfold IntroArg; intros H [ p q ]; apply H. Qed.
 
 Lemma IntroArg_or n P Q (goal : P \/ Q -> Prop)
@@ -171,11 +176,11 @@ Lemma IntroArg_or n P Q (goal : P \/ Q -> Prop)
 Proof. unfold IntroArg; intros Hl Hr [ p | q ]; [ apply Hl | apply Hr ]. Qed.
 
 Lemma IntroArg_sigT n A P (goal : {a : A & P a} -> Prop)
-  : IntroArg n A (fun a => IntroArg n (P a) (fun p => goal (existT _ a p))) -> IntroArg n _ goal.
+  : IntroArg n A (fun a => FreshIntroArg n (P a) (fun p => goal (existT _ a p))) -> IntroArg n _ goal.
 Proof. unfold IntroArg; intros H [ a p ]; apply H. Qed.
 
 Lemma IntroArg_prod n P Q (goal : P * Q -> Prop)
-  : IntroArg n P (fun p => IntroArg n Q (fun q => goal (pair p q))) -> IntroArg n _ goal.
+  : IntroArg n P (fun p => FreshIntroArg n Q (fun q => goal (pair p q))) -> IntroArg n _ goal.
 Proof. unfold IntroArg; intros H [ p q ]; apply H. Qed.
 
 Lemma IntroArg_sum n P Q (goal : P + Q -> Prop)
@@ -187,7 +192,7 @@ Lemma IntroArg_unit n (goal : unit -> Prop) : goal tt -> IntroArg n _ goal.
 Proof. unfold IntroArg; intros H []. apply H. Qed.
 
 Lemma IntroArg_eq_sigT_const n A B (a a' : A) (b b' : B) (goal : Prop)
-  : IntroArg n (a = a') (fun _ => IntroArg n (b = b') (fun _ => goal)) ->
+  : IntroArg n (a = a') (fun _ => FreshIntroArg n (b = b') (fun _ => goal)) ->
     IntroArg n (existT _ a b = existT _ a' b') (fun _ => goal).
 Proof.
   unfold IntroArg; intros H eq.
@@ -198,147 +203,6 @@ Qed.
 Hint Resolve IntroArg_and IntroArg_or IntroArg_sigT IntroArg_prod IntroArg_sum
              IntroArg_unit IntroArg_eq_sigT_const | 1 : refinesFun.
 
-Lemma IntroArg_bvEq_eq n w a b goal :
-  IntroArg n (a = b) (fun _ => goal) ->
-  IntroArg n (SAWCorePrelude.bvEq w a b = true) (fun _ => goal).
-Proof. unfold IntroArg; rewrite bvEq_eq; eauto. Qed.
-
-Lemma IntroArg_bvEq_neq n w a b goal :
-  IntroArg n (a <> b) (fun _ => goal) ->
-  IntroArg n (SAWCorePrelude.bvEq w a b = false) (fun _ => goal).
-Proof. unfold IntroArg; rewrite bvEq_neq; eauto. Qed.
-
-Lemma IntroArg_bv_eq_if_true n (b : bool) goal :
-  IntroArg n (b = true) (fun _ => goal) ->
-  IntroArg n ((if b then intToBv 1 1 else intToBv 1 0) = intToBv 1 1) (fun _ => goal).
-Proof. unfold IntroArg; rewrite bv_eq_if_true; eauto. Qed.
-
-Lemma IntroArg_bv_eq_if_false n (b : bool) goal :
-  IntroArg n (b = false) (fun _ => goal) ->
-  IntroArg n ((if b then intToBv 1 1 else intToBv 1 0) = intToBv 1 0) (fun _ => goal).
-Proof. unfold IntroArg; rewrite bv_eq_if_false; eauto. Qed.
-
-Lemma IntroArg_bv_neq_if_true n (b : bool) goal :
-  IntroArg n (b = false) (fun _ => goal) ->
-  IntroArg n ((if b then intToBv 1 1 else intToBv 1 0) <> intToBv 1 1) (fun _ => goal).
-Proof. unfold IntroArg; rewrite bv_neq_if_true; eauto. Qed.
-
-Lemma IntroArg_bv_neq_if_false n (b : bool) goal :
-  IntroArg n (b = true) (fun _ => goal) ->
-  IntroArg n ((if b then intToBv 1 1 else intToBv 1 0) <> intToBv 1 0) (fun _ => goal).
-Proof. unfold IntroArg; rewrite bv_neq_if_false; eauto. Qed.
-
-Lemma IntroArg_and_bool_eq_true_lemma n (b c : bool) goal :
-  IntroArg n ((b = true) /\ (c = true)) (fun _ => goal) ->
-  IntroArg n (and b c = true) (fun _ => goal).
-Proof. unfold IntroArg; rewrite and_bool_eq_true_lemma; eauto. Qed.
-
-Lemma IntroArg_and_bool_eq_false_lemma n (b c : bool) goal :
-  IntroArg n ((b = false) \/ (c = false)) (fun _ => goal) ->
-  IntroArg n (and b c = false) (fun _ => goal).
-Proof. unfold IntroArg; rewrite and_bool_eq_false_lemma; eauto. Qed.
-
-Lemma IntroArg_or_bool_eq_true_lemma n (b c : bool) goal :
-  IntroArg n ((b = true) \/ (c = true)) (fun _ => goal) ->
-  IntroArg n (or b c = true) (fun _ => goal).
-Proof. unfold IntroArg; rewrite or_bool_eq_true_lemma; eauto. Qed.
-
-Lemma IntroArg_or_bool_eq_false_lemma n (b c : bool) goal :
-  IntroArg n ((b = false) /\ (c = false)) (fun _ => goal) ->
-  IntroArg n (or b c = false) (fun _ => goal).
-Proof. unfold IntroArg; rewrite or_bool_eq_false_lemma; eauto. Qed.
-
-Lemma IntroArg_not_bool_eq_true_lemma n (b : bool) goal :
-  IntroArg n (b = false) (fun _ => goal) ->
-  IntroArg n (not b = true) (fun _ => goal).
-Proof. unfold IntroArg; rewrite not_bool_eq_true_lemma; eauto. Qed.
-
-Lemma IntroArg_not_bool_eq_false_lemma n (b : bool) goal :
-  IntroArg n (b = true) (fun _ => goal) ->
-  IntroArg n (not b = false) (fun _ => goal).
-Proof. unfold IntroArg; rewrite not_bool_eq_false_lemma; eauto. Qed.
-
-Lemma IntroArg_boolEq_eq n a b goal :
-  IntroArg n (a = b) (fun _ => goal) ->
-  IntroArg n (boolEq a b = true) (fun _ => goal).
-Proof. unfold IntroArg; rewrite boolEq_eq; eauto. Qed.
-
-Lemma IntroArg_boolEq_neq n a b goal :
-  IntroArg n (a <> b) (fun _ => goal) ->
-  IntroArg n (boolEq a b = false) (fun _ => goal).
-Proof. unfold IntroArg; rewrite boolEq_neq; eauto. Qed.
-
-Lemma IntroArg_bool_eq_if_true n (b : bool) goal :
-  IntroArg n (b = true) (fun _ => goal) ->
-  IntroArg n ((if b then true else false) = true) (fun _ => goal).
-Proof. unfold IntroArg; rewrite bool_eq_if_true; eauto. Qed.
-
-Lemma IntroArg_bool_eq_if_false n (b : bool) goal :
-  IntroArg n (b = false) (fun _ => goal) ->
-  IntroArg n ((if b then true else false) = false) (fun _ => goal).
-Proof. unfold IntroArg; rewrite bool_eq_if_false; eauto. Qed.
-
-Lemma IntroArg_bool_eq_if_inv_true n (b : bool) goal :
-  IntroArg n (b = false) (fun _ => goal) ->
-  IntroArg n ((if b then false else true) = true) (fun _ => goal).
-Proof. unfold IntroArg; rewrite bool_eq_if_inv_true; eauto. Qed.
-
-Lemma IntroArg_bool_eq_if_inv_false n (b : bool) goal :
-  IntroArg n (b = true) (fun _ => goal) ->
-  IntroArg n ((if b then false else true) = false) (fun _ => goal).
-Proof. unfold IntroArg; rewrite bool_eq_if_inv_false; eauto. Qed.
-
-Hint Extern 1 (IntroArg _ (SAWCorePrelude.bvEq _ _ _ = true) _) =>
-   simple apply IntroArg_bvEq_eq : refinesFun.
-Hint Extern 1 (IntroArg _ (SAWCorePrelude.bvEq _ _ _ = false) _) =>
-   simple apply IntroArg_bvEq_neq : refinesFun.
-Hint Extern 1 (IntroArg _ ((if _ then intToBv 1 (-1) else intToBv 1 0) = intToBv 1 1) _) =>
-   simple apply IntroArg_bv_eq_if_true : refinesFun.
-Hint Extern 1 (IntroArg _ ((if _ then intToBv 1 (-1) else intToBv 1 0) = intToBv 1 0) _) =>
-   simple apply IntroArg_bv_eq_if_false : refinesFun.
-Hint Extern 1 (IntroArg _ ((if _ then intToBv 1 (-1) else intToBv 1 0) <> intToBv 1 1) _) =>
-   simple apply IntroArg_bv_neq_if_true : refinesFun.
-Hint Extern 1 (IntroArg _ ((if _ then intToBv 1 (-1) else intToBv 1 0) <> intToBv 1 0) _) =>
-   simple apply IntroArg_bv_neq_if_false : refinesFun.
-Hint Extern 1 (IntroArg _ (and _ _ = true) _) =>
-   simple apply IntroArg_and_bool_eq_true_lemma : refinesFun.
-Hint Extern 1 (IntroArg _ (and _ _ = false) _) =>
-   simple apply IntroArg_and_bool_eq_false_lemma : refinesFun.
-Hint Extern 1 (IntroArg _ (or _ _ = true) _) =>
-   simple apply IntroArg_or_bool_eq_true_lemma : refinesFun.
-Hint Extern 1 (IntroArg _ (or _ _ = false) _) =>
-   simple apply IntroArg_or_bool_eq_false_lemma : refinesFun.
-Hint Extern 1 (IntroArg _ (not _ = true) _) =>
-   simple apply IntroArg_not_bool_eq_true_lemma : refinesFun.
-Hint Extern 1 (IntroArg _ (not _ = false) _) =>
-   simple apply IntroArg_not_bool_eq_false_lemma : refinesFun.
-Hint Extern 1 (IntroArg _ (boolEq _ _ = true) _) =>
-   simple apply IntroArg_boolEq_eq : refinesFun.
-Hint Extern 1 (IntroArg _ (boolEq _ _ = false) _) =>
-   simple apply IntroArg_boolEq_neq : refinesFun.
-Hint Extern 1 (IntroArg _ ((if _ then Datatypes.true else Datatypes.false) = SAWCoreScaffolding.true) _) =>
-   simple apply IntroArg_bool_eq_if_true : refinesFun.
-Hint Extern 1 (IntroArg _ ((if _ then Datatypes.true else Datatypes.false) = SAWCoreScaffolding.false) _) =>
-   simple apply IntroArg_bool_eq_if_false : refinesFun.
-Hint Extern 1 (IntroArg _ ((if _ then Datatypes.false else Datatypes.true) = SAWCoreScaffolding.true) _) =>
-   simple apply IntroArg_bool_eq_if_inv_true : refinesFun.
-Hint Extern 1 (IntroArg _ ((if _ then Datatypes.false else Datatypes.true) = SAWCoreScaffolding.false) _) =>
-   simple apply IntroArg_bool_eq_if_inv_false : refinesFun.
-
-Ltac IntroArg_If0_eq T :=
-  let e := fresh in
-    IntroArg_intro e;
-    compute_bv_funs in e;
-    match T with
-    | bool => (* try rewrite e; *)
-              autorewrite with SAWCoreBitvectors_eqs in e;
-              simpl in e; try fold true in e; try fold false in e
-    end;
-    apply (IntroArg_fold If _ _ e); clear e.
-
-Hint Extern 0 (IntroArg If0 (@eq ?T _ _) _) =>
-  progress (IntroArg_If0_eq T) : refinesFun.
-
 Ltac IntroArg_try_rewrite_bool_eq n T :=
   let e := fresh in
     IntroArg_intro e;
@@ -350,75 +214,6 @@ Ltac IntroArg_try_rewrite_bool_eq n T :=
 Hint Extern 2 (IntroArg ?n (@eq ?T _ _) _) =>
   progress (IntroArg_try_rewrite_bool_eq n T) : refinesFun.
 
-(* Ltac IntroArg_rewrite_bool_eq T n g := *)
-(*   let e := argName n in *)
-(*     IntroArg_intro e; *)
-(*     match T with *)
-(*     | bool => try rewrite e; let t := type of e in idtac t; idtac g *)
-(*               (* autorewrite with SAWCoreBitvectors_eqs in e *) *)
-(*     end; compute_bv_funs in e; simpl in e; *)
-(*     apply (IntroArg_fold n _ _ e); clear e. *)
-
-(* Hint Extern 2 (IntroArg ?n (@eq ?T _ _) ?g) => *)
-(*   progress (IntroArg_rewrite_bool_eq T n g); idtac "made it" : refinesFun. *)
-
-Lemma IntroArg_isBvsle_def n w a b goal
-  : IntroArg n (isBvsle w a b) (fun _ => goal) ->
-    IntroArg n (bvsle w a b = true) (fun _ => goal).
-Proof. unfold IntroArg; rewrite isBvsle_def; eauto. Qed.
-
-Lemma IntroArg_isBvsle_def_opp n w a b goal
-  : IntroArg n (isBvsle w b a) (fun _ => goal) ->
-    IntroArg n (bvslt w a b = false) (fun _ => goal).
-Proof. unfold IntroArg; rewrite isBvsle_def_opp; eauto. Qed.
-
-Lemma IntroArg_isBvslt_def n w a b goal
-  : IntroArg n (isBvslt w a b) (fun _ => goal) ->
-    IntroArg n (bvslt w a b = true) (fun _ => goal).
-Proof. unfold IntroArg; rewrite isBvslt_def; eauto. Qed.
-
-Lemma IntroArg_isBvslt_def_opp n w a b goal
-  : IntroArg n (isBvslt w b a) (fun _ => goal) ->
-    IntroArg n (bvsle w a b = false) (fun _ => goal).
-Proof. unfold IntroArg; rewrite isBvslt_def_opp; eauto. Qed.
-
-Lemma IntroArg_isBvule_def n w a b goal
-  : IntroArg n (isBvule w a b) (fun _ => goal) ->
-    IntroArg n (bvule w a b = true) (fun _ => goal).
-Proof. unfold IntroArg; rewrite isBvule_def; eauto. Qed.
-
-Lemma IntroArg_isBvule_def_opp n w a b goal
-  : IntroArg n (isBvule w b a) (fun _ => goal) ->
-    IntroArg n (bvult w a b = false) (fun _ => goal).
-Proof. unfold IntroArg; rewrite isBvule_def_opp; eauto. Qed.
-
-Lemma IntroArg_isBvult_def n w a b goal
-  : IntroArg n (isBvult w a b) (fun _ => goal) ->
-    IntroArg n (bvult w a b = true) (fun _ => goal).
-Proof. unfold IntroArg; rewrite isBvult_def; eauto. Qed.
-
-Lemma IntroArg_isBvult_def_opp n w a b goal
-  : IntroArg n (isBvult w b a) (fun _ => goal) ->
-    IntroArg n (bvule w a b = false) (fun _ => goal).
-Proof. unfold IntroArg; rewrite isBvult_def_opp; eauto. Qed.
-
-Hint Extern 3 (IntroArg _ (bvsle _ _ _ = true) _) =>
-   simple apply IntroArg_isBvsle_def : refinesFun.
-Hint Extern 3 (IntroArg _ (bvslt _ _ _ = false) _) =>
-   simple apply IntroArg_isBvsle_def_opp : refinesFun.
-Hint Extern 3 (IntroArg _ (bvslt  _ _ = true) _) =>
-   simple apply IntroArg_isBvslt_def : refinesFun.
-Hint Extern 3 (IntroArg _ (bvsle _ _ _ = false) _) =>
-   simple apply IntroArg_isBvslt_def_opp : refinesFun.
-Hint Extern 3 (IntroArg _ (bvule _ _ _ = true) _) =>
-   simple apply IntroArg_isBvule_def : refinesFun.
-Hint Extern 3 (IntroArg _ (bvult _ _ _ = false) _) =>
-   simple apply IntroArg_isBvule_def_opp : refinesFun.
-Hint Extern 3 (IntroArg _ (bvult _ _ _ = true) _) =>
-   simple apply IntroArg_isBvult_def : refinesFun.
-Hint Extern 3 (IntroArg _ (bvule _ _ _ = false) _) =>
-   simple apply IntroArg_isBvult_def_opp : refinesFun.
-
 Ltac IntroArg_intro_injection n :=
   let e := argName n in
     IntroArg_intro e; injection e as; subst.
@@ -455,27 +250,20 @@ Hint Extern 3 (IntroArg ?n (eq true false) _) =>
 Hint Extern 3 (IntroArg ?n (eq false true) _) =>
   IntroArg_intro_discriminate n : refinesFun.
 
-(* Ltac IntroArg_intro_try_rewrite_non_bv n T := *)
-(*   let e := argName n in *)
-(*     IntroArg_intro e; *)
-(*     lazymatch T with *)
-(*     | bitvector _ => fail *)
-(*     | _ => try (time (rewrite e); let t := type of e in idtac t) *)
-(*     end. *)
-
-(* Hint Extern 4 (IntroArg ?n (@eq ?T _ _) _) => *)
-(*   IntroArg_intro_try_rewrite_non_bv n T : refinesFun. *)
-
-Hint Extern 5 (IntroArg ?n _ _) =>
+Hint Extern 4 (IntroArg ?n _ _) =>
   let e := argName n in IntroArg_intro e; subst : refinesFun.
 
 Definition refinesM_either_l_IntroArg {A B C} (f:A -> CompM C) (g:B -> CompM C) eith P :
-  (IntroArg Any _ (fun a => IntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => f a |= P))) ->
-  (IntroArg Any _ (fun b => IntroArg Either (eith = SAWCorePrelude.Right _ _ b) (fun _ => g b |= P))) ->
+  (FreshIntroArg Any _ (fun a =>
+    FreshIntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => f a |= P))) ->
+  (FreshIntroArg Any _ (fun b =>
+    FreshIntroArg Either (eith = SAWCorePrelude.Right _ _ b) (fun _ => g b |= P))) ->
   SAWCorePrelude.either _ _ _ f g eith |= P := refinesM_either_l f g eith P.
 Definition refinesM_either_r_IntroArg {A B C} (f:A -> CompM C) (g:B -> CompM C) eith P :
-  (IntroArg Any _ (fun a => IntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => P |= f a))) ->
-  (IntroArg Any _ (fun b => IntroArg Either (eith = SAWCorePrelude.Right _ _ b) (fun _ => P |= g b))) ->
+  (FreshIntroArg Any _ (fun a =>
+    FreshIntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => P |= f a))) ->
+  (FreshIntroArg Any _ (fun b =>
+    FreshIntroArg Either (eith = SAWCorePrelude.Right _ _ b) (fun _ => P |= g b))) ->
   P |= SAWCorePrelude.either _ _ _ f g eith := refinesM_either_r f g eith P.
 
 Hint Extern 1 (SAWCorePrelude.either _ _ _ _ _ _ |= _) =>
@@ -484,12 +272,14 @@ Hint Extern 1 (_ |= SAWCorePrelude.either _ _ _ _ _ _) =>
   simple apply refinesM_either_r_IntroArg : refinesM.
 
 Definition refinesM_maybe_l_IntroArg {A B} (x : CompM B) (f : A -> CompM B) mb P :
-  (IntroArg Maybe (mb = SAWCorePrelude.Nothing _) (fun _ => x |= P)) ->
-  (IntroArg Any _ (fun a => IntroArg Maybe (mb = SAWCorePrelude.Just _ a) (fun _ => f a |= P))) ->
+  (FreshIntroArg Maybe (mb = SAWCorePrelude.Nothing _) (fun _ => x |= P)) ->
+  (FreshIntroArg Any _ (fun a =>
+    FreshIntroArg Maybe (mb = SAWCorePrelude.Just _ a) (fun _ => f a |= P))) ->
   SAWCorePrelude.maybe _ _ x f mb |= P := refinesM_maybe_l x f mb P.
 Definition refinesM_maybe_r_IntroArg {A B} (x : CompM B) (f : A -> CompM B) mb P :
-  (IntroArg Maybe (mb = SAWCorePrelude.Nothing _) (fun _ => P |= x)) ->
-  (IntroArg Any _ (fun a => IntroArg Maybe (mb = SAWCorePrelude.Just _ a) (fun _ => P |= f a))) ->
+  (FreshIntroArg Maybe (mb = SAWCorePrelude.Nothing _) (fun _ => P |= x)) ->
+  (FreshIntroArg Any _ (fun a =>
+    FreshIntroArg Maybe (mb = SAWCorePrelude.Just _ a) (fun _ => P |= f a))) ->
   P |= SAWCorePrelude.maybe _ _ x f mb := refinesM_maybe_r x f mb P.
 
 Hint Extern 1 (SAWCorePrelude.maybe _ _ _ _ _ |= _) =>
@@ -498,13 +288,13 @@ Hint Extern 1 (_ |= SAWCorePrelude.maybe _ _ _ _ _) =>
   simple apply refinesM_maybe_r_IntroArg : refinesM.
 
 Definition refinesM_sigT_rect_l_IntroArg {A1 A2 B} F P (s: {x:A1 & A2 x}) :
-  (IntroArg Any _ (fun a1 => IntroArg Any _ (fun a2 =>
-    IntroArg SigT (s = existT _ a1 a2) (fun _ => F a1 a2 |= P)))) ->
+  (FreshIntroArg Any _ (fun a1 => FreshIntroArg Any _ (fun a2 =>
+    FreshIntroArg SigT (s = existT _ a1 a2) (fun _ => F a1 a2 |= P)))) ->
   sigT_rect (fun _ => CompM B) F s |= P := refinesM_sigT_rect_l F P s.
 
 Definition refinesM_sigT_rect_r_IntroArg {A1 A2 B} F P (s: {x:A1 & A2 x}) :
-  (IntroArg Any _ (fun a1 => IntroArg Any _ (fun a2 =>
-    IntroArg SigT (s = existT _ a1 a2) (fun _ => P |= F a1 a2)))) ->
+  (FreshIntroArg Any _ (fun a1 => FreshIntroArg Any _ (fun a2 =>
+    FreshIntroArg SigT (s = existT _ a1 a2) (fun _ => P |= F a1 a2)))) ->
   P |= sigT_rect (fun _ => CompM B) F s := refinesM_sigT_rect_r F P s.
 
 Hint Extern 1 (sigT_rect (fun _ => CompM _) _ _ |= _) =>
@@ -513,12 +303,12 @@ Hint Extern 1 (_ |= sigT_rect (fun _ => CompM _) _ _) =>
   simple apply refinesM_sigT_rect_r_IntroArg : refinesM.
 
 Definition refinesM_if_l_IntroArg {A} (m1 m2:CompM A) b P :
-  (IntroArg If0 (b = true) (fun _ => m1 |= P)) ->
-  (IntroArg If0 (b = false) (fun _ => m2 |= P)) ->
+  (FreshIntroArg If (b = true) (fun _ => m1 |= P)) ->
+  (FreshIntroArg If (b = false) (fun _ => m2 |= P)) ->
   (if b then m1 else m2) |= P := refinesM_if_l m1 m2 b P.
 Definition refinesM_if_r_IntroArg {A} (m1 m2:CompM A) b P :
-  (IntroArg If0 (b = true) (fun _ => P |= m1)) ->
-  (IntroArg If0 (b = false) (fun _ => P |= m2)) ->
+  (FreshIntroArg If (b = true) (fun _ => P |= m1)) ->
+  (FreshIntroArg If (b = false) (fun _ => P |= m2)) ->
   P |= (if b then m1 else m2) := refinesM_if_r m1 m2 b P.
 
 Hint Extern 1 ((if _ then _ else _) |= _) =>
@@ -532,10 +322,10 @@ Hint Extern 1 (_ |= returnM (if _ then _ else _)) =>
   simple apply refinesM_returnM_if_r : refinesM.
 
 Definition refinesM_bindM_assertM_l_IntroArg {A} (P:Prop) (m1 m2: CompM A) :
-  (IntroArg Assert P (fun _ => m1 |= m2)) -> assertM P >> m1 |= m2 :=
+  (FreshIntroArg Assert P (fun _ => m1 |= m2)) -> assertM P >> m1 |= m2 :=
   refinesM_bindM_assertM_l P m1 m2.
 Definition refinesM_assumingM_r_IntroArg {A} (P:Prop) (m1 m2: CompM A) :
-  (IntroArg Assuming P (fun _ => m1 |= m2))  -> m1 |= assumingM P m2 :=
+  (FreshIntroArg Assuming P (fun _ => m1 |= m2))  -> m1 |= assumingM P m2 :=
   refinesM_assumingM_r P m1 m2.
 
 Hint Extern 1 (assertM _ >> _ |= _) =>
@@ -549,10 +339,10 @@ Hint Extern 2 (assumingM _ _ |= _) =>
   simple eapply refinesM_assumingM_l; shelve : refinesM.
 
 Definition refinesM_existsM_l_IntroArg A B (P: A -> CompM B) Q :
-  (IntroArg Exists _ (fun a => P a |= Q)) -> existsM P |= Q :=
+  (FreshIntroArg Exists _ (fun a => P a |= Q)) -> existsM P |= Q :=
   refinesM_existsM_l A B P Q.
 Definition refinesM_forallM_r_IntroArg {A B} P (Q: A -> CompM B) :
-  (IntroArg Forall _ (fun a => P |= (Q a))) -> P |= (forallM Q) :=
+  (FreshIntroArg Forall _ (fun a => P |= (Q a))) -> P |= (forallM Q) :=
   refinesM_forallM_r P Q.
 
 Hint Extern 2 (existsM _ |= _) =>
@@ -758,6 +548,13 @@ Admitted.
  *** Automation for proving function refinement
  ***)
 
+Definition StartAutomation (goal : Prop) := goal.
+
+Lemma StartAutomation_fold goal : StartAutomation goal -> goal.
+Proof. easy. Qed.
+
+Hint Extern 999 (StartAutomation ?A) => unfold StartAutomation : refinesFun.
+
 (* Create HintDb refinesFun. *)
 Hint Extern 999 (_ |= _) => shelve : refinesFun.
 Hint Extern 999 (refinesFun _ _) => shelve : refinesFun.
@@ -842,7 +639,8 @@ Ltac prove_refinement_core := prove_refinement_core with Default.
    form` P |= Q`, where P,Q may contain matching calls to `letRecM`. *)
 
 Tactic Notation "prove_refinement" "with" constr(opts) :=
-  unfold_projs; compute_bv_funs;
+  unfold_projs; (* compute_bv_funs; *)
+  apply StartAutomation_fold;
   prove_refinement_core with opts.
 
 Ltac prove_refinement := prove_refinement with Default.
diff --git a/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v b/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
index 41d3c446..ef454442 100644
--- a/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
+++ b/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
@@ -3,15 +3,22 @@
  ***)
 
 From Coq Require Import Program.Basics.
+From Coq Require        Program.Equality.
 From Coq Require Import Vectors.Vector.
+From Coq Require Import Logic.Eqdep.
 
 From CryptolToCoq Require Import SAWCorePrelude.
 From CryptolToCoq Require Import SAWCoreScaffolding.
 From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
+From CryptolToCoq Require Import CompMExtra.
 
 Import SAWCorePrelude.
 
-Create HintDb SAWCoreBitvectors.
+(* A duplicate from `Program.Equality`, because importing that
+   module directly gives us a conflict with the `~=` notation... *)
+Tactic Notation "dependent" "destruction" ident(H) := 
+  Equality.do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => Equality.do_case hyp) H.
+
 Create HintDb SAWCoreBitvectors_eqs.
 
 
@@ -66,22 +73,24 @@ Ltac compute_bv_funs_tac H t compute_bv_binrel compute_bv_binop
     end
   end.
 
-Ltac unfold_bv_funs := unfold bvultWithProof, bvuleWithProof,
+Ltac unfold_bv_funs := unfold bvNat, bvultWithProof, bvuleWithProof,
                               bvsge, bvsgt, bvuge, bvugt, bvSCarry, bvSBorrow,
                               xor, xorb.
 
 Tactic Notation "compute_bv_funs" :=
-  unfold_bv_funs; repeat match goal with
-                         | |- ?t => let H := fresh "H" in
-                                    try (compute_bv_funs_tac H t compute_bv_binrel_in_goal compute_bv_binop_in_goal compute_bv_unrel_in_goal compute_bv_unop_in_goal)
-                         end.
+  unfold_bv_funs;
+  repeat match goal with
+         | |- ?t => let H := fresh "H" in
+                    try (compute_bv_funs_tac H t compute_bv_binrel_in_goal compute_bv_binop_in_goal compute_bv_unrel_in_goal compute_bv_unop_in_goal)
+         end.
 
 Tactic Notation "compute_bv_funs" "in" ident(H) :=
-  unfold_bv_funs; repeat match goal with
-                  | H': ?t |- _ => match H' with
-                                   | H => try (compute_bv_funs_tac H t compute_bv_binrel_in compute_bv_binop_in compute_bv_unrel_in compute_bv_unop_in)
-                                   end
-                  end.
+  unfold_bv_funs;
+  repeat match goal with
+         | H': ?t |- _ => match H' with
+                          | H => try (compute_bv_funs_tac H t compute_bv_binrel_in compute_bv_binop_in compute_bv_unrel_in compute_bv_unop_in)
+                          end
+         end.
 
 
 (** Bitvector maximum and minimum values **)
@@ -106,25 +115,21 @@ Definition bvumin w : bitvector w := gen w _ (fun _ => false).
 Definition isBvsle w a b : Prop := bvsle w a b = true.
 Definition isBvsle_def w a b : bvsle w a b = true <-> isBvsle w a b := reflexivity _.
 Definition isBvsle_def_opp w a b : bvslt w a b = false <-> isBvsle w b a. Admitted.
-Hint Rewrite isBvsle_def isBvsle_def_opp : SAWCoreBitvectors.
 Instance PreOrder_isBvsle w : PreOrder (isBvsle w). Admitted.
 
 Definition isBvslt w a b : Prop := bvslt w a b = true.
 Definition isBvslt_def w a b : bvslt w a b = true <-> isBvslt w a b := reflexivity _.
 Definition isBvslt_def_opp w a b : bvsle w a b = false <-> isBvslt w b a. Admitted.
-Hint Rewrite isBvslt_def isBvslt_def_opp : SAWCoreBitvectors.
 Instance PreOrder_isBvslt w : PreOrder (isBvslt w). Admitted.
 
 Definition isBvule w a b : Prop := bvule w a b = true.
 Definition isBvule_def w a b : bvule w a b = true <-> isBvule w a b := reflexivity _.
 Definition isBvule_def_opp w a b : bvult w a b = false <-> isBvule w b a. Admitted.
-Hint Rewrite isBvule_def isBvule_def_opp : SAWCoreBitvectors.
 Instance PreOrder_isBvule w : PreOrder (isBvule w). Admitted.
 
 Definition isBvult w a b : Prop := bvult w a b = true.
 Definition isBvult_def w a b : bvult w a b = true <-> isBvult w a b := reflexivity _.
 Definition isBvult_def_opp w a b : bvule w a b = false <-> isBvult w b a. Admitted.
-Hint Rewrite isBvult_def isBvult_def_opp : SAWCoreBitvectors.
 Instance PreOrder_isBvult w : PreOrder (isBvult w). Admitted.
 
 
@@ -174,55 +179,34 @@ Definition isBvsle_antisymm w a b : isBvsle w a b -> isBvsle w b a -> a = b.
 Admitted.
 
 
-(** Lemmas about bitvector equality **)
-
-Lemma bvEq_eq  w a b : bvEq w a b = true <-> a = b. Admitted.
-Lemma bvEq_neq w a b : bvEq w a b = false <-> a <> b. Admitted.
-Hint Rewrite bvEq_eq bvEq_neq : SAWCoreBitvectors.
-
-Lemma bv_eq_if_true (b : bool) : (if b then intToBv 1 1 else intToBv 1 0) = intToBv 1 1 <-> b = true.
-Proof. split; intro H; destruct b; reflexivity || inversion H. Qed.
-Lemma bv_eq_if_false (b : bool) : (if b then intToBv 1 1 else intToBv 1 0) = intToBv 1 0 <-> b = false.
-Proof. split; intro H; destruct b; reflexivity || inversion H. Qed.
-
-Hint Rewrite bv_eq_if_true bv_eq_if_false : SAWCoreBitvectors.
-
-Lemma bv_neq_if_true (b : bool) : (if b then intToBv 1 1 else intToBv 1 0) <> intToBv 1 1 <-> b = false.
-Proof.
-  split; intro H; destruct b; try reflexivity || inversion H.
-  - pose (H0 := H (reflexivity _)); inversion H0.
-  - intro H0; inversion H0.
-Qed.
+(** Lemmas about bitvector addition **)
 
-Lemma bv_neq_if_false (b : bool) : (if b then intToBv 1 1 else intToBv 1 0) <> intToBv 1 0 <-> b = true.
-Proof.
-  split; intro H; destruct b; try reflexivity || inversion H.
-  - pose (H0 := H (reflexivity _)); inversion H0.
-  - intro H0; inversion H0.
-Qed.
+Lemma bvAdd_id_l w a : bvAdd w (intToBv w 0) a = a.
+Admitted.
 
-Hint Rewrite bv_neq_if_true bv_neq_if_false : SAWCoreBitvectors.
+Lemma bvAdd_id_r w a : bvAdd w a (intToBv w 0) = a.
+Admitted.
 
+Hint Rewrite bvAdd_id_l bvAdd_id_r : SAWCoreBitvectors_eqs.
 
-(** Lemmas about bitvector addition **)
+Lemma bvAdd_comm w a b : bvAdd w a b = bvAdd w b a.
+Admitted.
 
-Lemma bvAdd_id_l w a : bvAdd w (intToBv w 0) a = a. Admitted.
-Lemma bvAdd_id_r w a : bvAdd w a (intToBv w 0) = a. Admitted.
-Lemma bvAdd_comm w a b : bvAdd w a b = bvAdd w b a. Admitted.
-Lemma bvAdd_assoc w a b c : bvAdd w (bvAdd w a b) c = bvAdd w a (bvAdd w b c). Admitted.
+Lemma bvAdd_assoc w a b c : bvAdd w (bvAdd w a b) c = bvAdd w a (bvAdd w b c).
+Admitted.
 
 
-(** Lemmas about subtraction, negation, and sign bits **)
+(** Lemmas about bitvector subtraction, negation, and sign bits **)
 
 Lemma bvSub_zero_bvNeg w a : bvSub w (intToBv w 0) a = bvNeg w a.
 Admitted.
 
-Hint Rewrite bvSub_zero_bvNeg : SAWCoreBitvectors SAWCoreBitvectors_eqs.
+Hint Rewrite bvSub_zero_bvNeg : SAWCoreBitvectors_eqs.
 
 Lemma bvNeg_msb w a : msb w (bvNeg (Succ w) a) = not (msb w a).
 Admitted.
 
-Hint Rewrite bvNeg_msb : SAWCoreBitvectors SAWCoreBitvectors_eqs.
+Hint Rewrite bvNeg_msb : SAWCoreBitvectors_eqs.
 
 Lemma bvslt_bvSub_r w a b : isBvslt w a b <-> isBvslt w (intToBv w 0) (bvSub w b a).
 Admitted.
@@ -246,78 +230,91 @@ Lemma bvule_msb_r w a b : isBvule (Succ w) a b -> msb w b = false -> msb w a = f
 Admitted.
 
 
-(** Other rewriting hints not directly involving bitvectors **)
+(** Some general lemmas about boolean equality **)
 
-Lemma and_bool_eq_true_lemma (b c : bool) : and b c = true <-> (b = true) /\ (c = true).
+Lemma boolEq_eq a b : boolEq a b = true <-> a = b.
+Proof. split; destruct a, b; easy. Qed.
+
+Lemma boolEq_neq a b : boolEq a b = false <-> a <> b.
+Proof. split; destruct a, b; easy. Qed.
+
+Lemma boolEq_refl a : boolEq a a = true.
+Proof. destruct a; easy. Qed.
+
+Lemma and_bool_eq_true b c : and b c = true <-> (b = true) /\ (c = true).
 Proof.
   split.
   - destruct b, c; auto.
   - intro; destruct H; destruct b, c; auto.
 Qed.
 
-Lemma and_bool_eq_false_lemma (b c : bool) : and b c = false <-> (b = false) \/ (c = false).
+Lemma and_bool_eq_false b c : and b c = false <-> (b = false) \/ (c = false).
 Proof.
   split.
   - destruct b, c; auto.
   - intro; destruct H; destruct b, c; auto.
 Qed.
 
-Hint Rewrite and_bool_eq_true_lemma and_bool_eq_false_lemma : SAWCoreBitvectors.
-
-Lemma or_bool_eq_true_lemma (b c : bool) : or b c = true <-> (b = true) \/ (c = true).
+Lemma or_bool_eq_true b c : or b c = true <-> (b = true) \/ (c = true).
 Proof.
   split.
   - destruct b, c; auto.
   - intro; destruct H; destruct b, c; auto.
 Qed.
 
-Lemma or_bool_eq_false_lemma (b c : bool) : or b c = false <-> (b = false) /\ (c = false).
+Lemma or_bool_eq_false b c : or b c = false <-> (b = false) /\ (c = false).
 Proof.
   split.
   - destruct b, c; auto.
   - intro; destruct H; destruct b, c; auto.
 Qed.
 
-Hint Rewrite or_bool_eq_true_lemma or_bool_eq_false_lemma : SAWCoreBitvectors.
-
-Lemma not_bool_eq_true_lemma (b : bool) : not b = true <-> b = false.
+Lemma not_bool_eq_true b : not b = true <-> b = false.
 Proof. split; destruct b; auto. Qed.
 
-Lemma not_bool_eq_false_lemma (b : bool) : not b = false <-> b = true.
+Lemma not_bool_eq_false b : not b = false <-> b = true.
 Proof. split; destruct b; auto. Qed.
 
-Hint Rewrite not_bool_eq_true_lemma not_bool_eq_false_lemma : SAWCoreBitvectors.
-
-(* Lemma sym_bool_true_eq_lemma (b : bool) : true = b <-> b = true. *)
-(* Proof. split; auto. Qed. *)
 
-(* Lemma sym_bool_false_eq_lemma (b : bool) : false = b <-> b = false. *)
-(* Proof. split; auto. Qed. *)
+(** Lemmas about bitvector equality **)
 
-(* Hint Rewrite sym_bool_true_eq_lemma sym_bool_false_eq_lemma : SAWCoreBitvectors. *)
+Lemma bvEq_cons w h0 h1 a0 a1 :
+  bvEq (S w) (VectorDef.cons _ h0 w a0) (VectorDef.cons _ h1 w a1) =
+  and (boolEq h0 h1) (bvEq w a0 a1).
+Proof. reflexivity. Qed.
 
-Lemma boolEq_eq  a b : boolEq a b = true <-> a = b. Admitted.
-Lemma boolEq_neq a b : boolEq a b = false <-> a <> b. Admitted.
-Hint Rewrite boolEq_eq boolEq_neq : SAWCoreBitvectors.
+Lemma bvEq_refl w a : bvEq w a a = true.
+Proof.
+  induction a; eauto.
+  rewrite bvEq_cons, boolEq_refl, IHa; eauto.
+Qed.
 
-Lemma bool_eq_if_true (b : bool) : (if b then true else false) = true <-> b = true.
-Proof. split; intro H; destruct b; reflexivity || inversion H. Qed.
-Lemma bool_eq_if_false (b : bool) : (if b then true else false) = false <-> b = false.
-Proof. split; intro H; destruct b; reflexivity || inversion H. Qed.
-Lemma bool_eq_if_inv_true (b : bool) : (if b then false else true) = true <-> b = false.
-Proof. split; intro H; destruct b; reflexivity || inversion H. Qed.
-Lemma bool_eq_if_inv_false (b : bool) : (if b then false else true) = false <-> b = true.
-Proof. split; intro H; destruct b; reflexivity || inversion H. Qed.
+Lemma bvEq_eq  w a b : bvEq w a b = true <-> a = b.
+Proof.
+  split; intro; induction a; dependent destruction b; eauto.
+  - rewrite bvEq_cons, and_bool_eq_true in H.
+    destruct H; rewrite boolEq_eq in H; apply IHa in H0.
+    subst; reflexivity.
+  - injection H as; apply inj_pair2 in H0; subst.
+    rewrite bvEq_cons, and_bool_eq_true; split.
+    + apply boolEq_refl.
+    + apply bvEq_refl.
+Qed.
 
-Hint Rewrite bool_eq_if_true bool_eq_if_false bool_eq_if_false bool_eq_if_true : SAWCoreBitvectors.
+(* the other direction only holds if we assume LEM *)
+Lemma bvEq_neq w a b : bvEq w a b = false -> a <> b.
+Proof.
+  intro; induction a; dependent destruction b; eauto.
+  intro; injection H0 as; apply inj_pair2 in H1.
+  rewrite bvEq_cons, and_bool_eq_false in H.
+  destruct H; [ rewrite boolEq_neq in H | apply IHa in H ].
+  all: contradiction.
+Qed.
 
-Lemma bool_if_lemma (b : bool) : (if b then true else false) = b.
-Proof. destruct b; reflexivity. Qed.
 
-Lemma bool_if_not_lemma (b : bool) : (if b then false else true) = not b.
-Proof. destruct b; reflexivity. Qed.
+(** Proof automation - computing and rewriting bv funs **)
 
-Hint Rewrite bool_if_lemma bool_if_not_lemma : SAWCoreBitvectors_eqs.
+Hint Extern 1 (StartAutomation _) => progress compute_bv_funs: refinesFun.
 
 Lemma true_eq_scaffolding_true : Datatypes.true = SAWCoreScaffolding.true.
 Proof. reflexivity. Qed.
@@ -325,3 +322,199 @@ Lemma false_eq_scaffolding_false : Datatypes.false = SAWCoreScaffolding.false.
 Proof. reflexivity. Qed.
 
 Hint Rewrite true_eq_scaffolding_true false_eq_scaffolding_false : SAWCoreBitvectors_eqs.
+
+Ltac FreshIntroArg_bv_eq T :=
+  let e := fresh in
+    IntroArg_intro e;
+    compute_bv_funs in e;
+    match T with
+    | bool => (* try rewrite e; *)
+              autorewrite with SAWCoreBitvectors_eqs in e;
+              simpl in e; try fold true in e; try fold false in e
+    end;
+    apply (IntroArg_fold If _ _ e); clear e.
+
+Hint Extern 1 (FreshIntroArg _ (@eq ?T _ _) _) =>
+  progress (FreshIntroArg_bv_eq T) : refinesFun.
+
+
+(** Proof automation - IntroArg rules **)
+
+Lemma IntroArg_bvEq_eq n w a b goal :
+  IntroArg n (a = b) (fun _ => goal) ->
+  IntroArg n (SAWCorePrelude.bvEq w a b = true) (fun _ => goal).
+Proof. do 2 intro; apply H, bvEq_eq; eauto. Qed.
+Lemma IntroArg_bvEq_neq n w a b goal :
+  IntroArg n (a <> b) (fun _ => goal) ->
+  IntroArg n (SAWCorePrelude.bvEq w a b = false) (fun _ => goal).
+Proof. do 2 intro; apply H, bvEq_neq; eauto. Qed.
+
+Hint Extern 1 (IntroArg _ (SAWCorePrelude.bvEq _ _ _ = true) _) =>
+   simple apply IntroArg_bvEq_eq : refinesFun.
+Hint Extern 1 (IntroArg _ (SAWCorePrelude.bvEq _ _ _ = false) _) =>
+   simple apply IntroArg_bvEq_neq : refinesFun.
+
+Lemma IntroArg_bv_eq_if_true n (b : bool) goal :
+  IntroArg n (b = true) (fun _ => goal) ->
+  IntroArg n ((if b then intToBv 1 1 else intToBv 1 0) = intToBv 1 1) (fun _ => goal).
+Proof. do 2 intro; apply H; destruct b; easy. Qed.
+Lemma IntroArg_bv_eq_if_false n (b : bool) goal :
+  IntroArg n (b = false) (fun _ => goal) ->
+  IntroArg n ((if b then intToBv 1 1 else intToBv 1 0) = intToBv 1 0) (fun _ => goal).
+Proof. do 2 intro; apply H; destruct b; easy. Qed.
+Lemma IntroArg_bv_neq_if_true n (b : bool) goal :
+  IntroArg n (b = false) (fun _ => goal) ->
+  IntroArg n ((if b then intToBv 1 1 else intToBv 1 0) <> intToBv 1 1) (fun _ => goal).
+Proof. do 2 intro; apply H; destruct b; easy. Qed.
+Lemma IntroArg_bv_neq_if_false n (b : bool) goal :
+  IntroArg n (b = true) (fun _ => goal) ->
+  IntroArg n ((if b then intToBv 1 1 else intToBv 1 0) <> intToBv 1 0) (fun _ => goal).
+Proof. do 2 intro; apply H; destruct b; easy. Qed.
+
+Hint Extern 1 (IntroArg _ ((if _ then intToBv 1 (-1) else intToBv 1 0) = intToBv 1 1) _) =>
+   simple apply IntroArg_bv_eq_if_true : refinesFun.
+Hint Extern 1 (IntroArg _ ((if _ then intToBv 1 (-1) else intToBv 1 0) = intToBv 1 0) _) =>
+   simple apply IntroArg_bv_eq_if_false : refinesFun.
+Hint Extern 1 (IntroArg _ ((if _ then intToBv 1 (-1) else intToBv 1 0) <> intToBv 1 1) _) =>
+   simple apply IntroArg_bv_neq_if_true : refinesFun.
+Hint Extern 1 (IntroArg _ ((if _ then intToBv 1 (-1) else intToBv 1 0) <> intToBv 1 0) _) =>
+   simple apply IntroArg_bv_neq_if_false : refinesFun.
+
+Lemma IntroArg_and_bool_eq_true n (b c : bool) goal :
+  IntroArg n ((b = true) /\ (c = true)) (fun _ => goal) ->
+  IntroArg n (and b c = true) (fun _ => goal).
+Proof. do 2 intro; apply H, and_bool_eq_true; eauto. Qed.
+Lemma IntroArg_and_bool_eq_false n (b c : bool) goal :
+  IntroArg n ((b = false) \/ (c = false)) (fun _ => goal) ->
+  IntroArg n (and b c = false) (fun _ => goal).
+Proof. do 2 intro; apply H, and_bool_eq_false; eauto. Qed.
+
+Hint Extern 1 (IntroArg _ (and _ _ = true) _) =>
+   simple apply IntroArg_and_bool_eq_true : refinesFun.
+Hint Extern 1 (IntroArg _ (and _ _ = false) _) =>
+   simple apply IntroArg_and_bool_eq_false : refinesFun.
+
+Lemma IntroArg_or_bool_eq_true n (b c : bool) goal :
+  IntroArg n ((b = true) \/ (c = true)) (fun _ => goal) ->
+  IntroArg n (or b c = true) (fun _ => goal).
+Proof. do 2 intro; apply H, or_bool_eq_true; eauto. Qed.
+Lemma IntroArg_or_bool_eq_false n (b c : bool) goal :
+  IntroArg n ((b = false) /\ (c = false)) (fun _ => goal) ->
+  IntroArg n (or b c = false) (fun _ => goal).
+Proof. do 2 intro; apply H, or_bool_eq_false; eauto. Qed.
+
+Hint Extern 1 (IntroArg _ (or _ _ = true) _) =>
+   simple apply IntroArg_or_bool_eq_true : refinesFun.
+Hint Extern 1 (IntroArg _ (or _ _ = false) _) =>
+   simple apply IntroArg_or_bool_eq_false : refinesFun.
+
+Lemma IntroArg_not_bool_eq_true n (b : bool) goal :
+  IntroArg n (b = false) (fun _ => goal) ->
+  IntroArg n (not b = true) (fun _ => goal).
+Proof. do 2 intro; apply H, not_bool_eq_true; eauto. Qed.
+Lemma IntroArg_not_bool_eq_false n (b : bool) goal :
+  IntroArg n (b = true) (fun _ => goal) ->
+  IntroArg n (not b = false) (fun _ => goal).
+Proof. do 2 intro; apply H, not_bool_eq_false; eauto. Qed.
+
+Hint Extern 1 (IntroArg _ (not _ = true) _) =>
+   simple apply IntroArg_not_bool_eq_true : refinesFun.
+Hint Extern 1 (IntroArg _ (not _ = false) _) =>
+   simple apply IntroArg_not_bool_eq_false : refinesFun.
+
+Lemma IntroArg_boolEq_eq n a b goal :
+  IntroArg n (a = b) (fun _ => goal) ->
+  IntroArg n (boolEq a b = true) (fun _ => goal).
+Proof. do 2 intro; apply H, boolEq_eq; eauto. Qed.
+Lemma IntroArg_boolEq_neq n a b goal :
+  IntroArg n (a <> b) (fun _ => goal) ->
+  IntroArg n (boolEq a b = false) (fun _ => goal).
+Proof. do 2 intro; apply H, boolEq_neq; eauto. Qed.
+
+Hint Extern 1 (IntroArg _ (boolEq _ _ = true) _) =>
+   simple apply IntroArg_boolEq_eq : refinesFun.
+Hint Extern 1 (IntroArg _ (boolEq _ _ = false) _) =>
+   simple apply IntroArg_boolEq_neq : refinesFun.
+
+Lemma IntroArg_bool_eq_if_true n (b : bool) goal :
+  IntroArg n (b = true) (fun _ => goal) ->
+  IntroArg n ((if b then true else false) = true) (fun _ => goal).
+Proof. do 2 intro; apply H; destruct b; eauto. Qed.
+Lemma IntroArg_bool_eq_if_false n (b : bool) goal :
+  IntroArg n (b = false) (fun _ => goal) ->
+  IntroArg n ((if b then true else false) = false) (fun _ => goal).
+Proof. do 2 intro; apply H; destruct b; eauto. Qed.
+Lemma IntroArg_bool_eq_if_inv_true n (b : bool) goal :
+  IntroArg n (b = false) (fun _ => goal) ->
+  IntroArg n ((if b then false else true) = true) (fun _ => goal).
+Proof. do 2 intro; apply H; destruct b; eauto. Qed.
+Lemma IntroArg_bool_eq_if_inv_false n (b : bool) goal :
+  IntroArg n (b = true) (fun _ => goal) ->
+  IntroArg n ((if b then false else true) = false) (fun _ => goal).
+Proof. do 2 intro; apply H; destruct b; eauto. Qed.
+
+(* TODO Figure out a way to not be forced to add `Datatypes.` here... *)
+Hint Extern 1 (IntroArg _ ((if _ then true else false) = true) _) =>
+   simple apply IntroArg_bool_eq_if_true : refinesFun.
+Hint Extern 1 (IntroArg _ ((if _ then true else false) = false) _) =>
+   simple apply IntroArg_bool_eq_if_false : refinesFun.
+Hint Extern 1 (IntroArg _ ((if _ then false else true) = true) _) =>
+   simple apply IntroArg_bool_eq_if_inv_true : refinesFun.
+Hint Extern 1 (IntroArg _ ((if _ then false else true) = false) _) =>
+   simple apply IntroArg_bool_eq_if_inv_false : refinesFun.
+
+Lemma IntroArg_isBvsle_def n w a b goal
+  : IntroArg n (isBvsle w a b) (fun _ => goal) ->
+    IntroArg n (bvsle w a b = true) (fun _ => goal).
+Proof. do 2 intro; apply H, isBvsle_def; eauto. Qed.
+Lemma IntroArg_isBvsle_def_opp n w a b goal
+  : IntroArg n (isBvsle w b a) (fun _ => goal) ->
+    IntroArg n (bvslt w a b = false) (fun _ => goal).
+Proof. do 2 intro; apply H, isBvsle_def_opp; eauto. Qed.
+
+Hint Extern 3 (IntroArg _ (bvsle _ _ _ = true) _) =>
+   simple apply IntroArg_isBvsle_def : refinesFun.
+Hint Extern 3 (IntroArg _ (bvslt _ _ _ = false) _) =>
+   simple apply IntroArg_isBvsle_def_opp : refinesFun.
+
+Lemma IntroArg_isBvslt_def n w a b goal
+  : IntroArg n (isBvslt w a b) (fun _ => goal) ->
+    IntroArg n (bvslt w a b = true) (fun _ => goal).
+Proof. do 2 intro; apply H, isBvslt_def; eauto. Qed.
+Lemma IntroArg_isBvslt_def_opp n w a b goal
+  : IntroArg n (isBvslt w b a) (fun _ => goal) ->
+    IntroArg n (bvsle w a b = false) (fun _ => goal).
+Proof. do 2 intro; apply H, isBvslt_def_opp; eauto. Qed.
+
+Hint Extern 3 (IntroArg _ (bvslt  _ _ = true) _) =>
+   simple apply IntroArg_isBvslt_def : refinesFun.
+Hint Extern 3 (IntroArg _ (bvsle _ _ _ = false) _) =>
+   simple apply IntroArg_isBvslt_def_opp : refinesFun.
+
+Lemma IntroArg_isBvule_def n w a b goal
+  : IntroArg n (isBvule w a b) (fun _ => goal) ->
+    IntroArg n (bvule w a b = true) (fun _ => goal).
+Proof. do 2 intro; apply H, isBvule_def; eauto. Qed.
+Lemma IntroArg_isBvule_def_opp n w a b goal
+  : IntroArg n (isBvule w b a) (fun _ => goal) ->
+    IntroArg n (bvult w a b = false) (fun _ => goal).
+Proof. do 2 intro; apply H, isBvule_def_opp; eauto. Qed.
+
+Hint Extern 3 (IntroArg _ (bvule _ _ _ = true) _) =>
+   simple apply IntroArg_isBvule_def : refinesFun.
+Hint Extern 3 (IntroArg _ (bvult _ _ _ = false) _) =>
+   simple apply IntroArg_isBvule_def_opp : refinesFun.
+
+Lemma IntroArg_isBvult_def n w a b goal
+  : IntroArg n (isBvult w a b) (fun _ => goal) ->
+    IntroArg n (bvult w a b = true) (fun _ => goal).
+Proof. do 2 intro; apply H, isBvult_def; eauto. Qed.
+Lemma IntroArg_isBvult_def_opp n w a b goal
+  : IntroArg n (isBvult w b a) (fun _ => goal) ->
+    IntroArg n (bvule w a b = false) (fun _ => goal).
+Proof. do 2 intro; apply H, isBvult_def_opp; eauto. Qed.
+
+Hint Extern 3 (IntroArg _ (bvult _ _ _ = true) _) =>
+   simple apply IntroArg_isBvult_def : refinesFun.
+Hint Extern 3 (IntroArg _ (bvule _ _ _ = false) _) =>
+   simple apply IntroArg_isBvult_def_opp : refinesFun.