diff --git a/heapster-saw/examples/arrays_proofs.v b/heapster-saw/examples/arrays_proofs.v
index 531dd7142a..e1504a8a9e 100644
--- a/heapster-saw/examples/arrays_proofs.v
+++ b/heapster-saw/examples/arrays_proofs.v
@@ -41,6 +41,7 @@ Proof.
      there are multiple. For this poof though, it doesn't. *)
   all: try assumption.
   (* Proving that the loop invariant holds inductively: *)
+  - discriminate e_maybe.
   - transitivity a2.
     + assumption.
     + apply isBvsle_suc_r; eauto.
@@ -251,6 +252,7 @@ Proof.
       rewrite <- e_assuming; reflexivity.
   - (* (e_if4 is a contradiction) *)
     admit.
+  - admit.
   - rewrite e_assuming.
     change (intToBv 64 2) with (bvAdd 64 (intToBv 64 1) (intToBv 64 1)).
     rewrite <- bvAdd_assoc.
diff --git a/heapster-saw/examples/linked_list_proofs.v b/heapster-saw/examples/linked_list_proofs.v
index 85ad8ee8aa..266274a81b 100644
--- a/heapster-saw/examples/linked_list_proofs.v
+++ b/heapster-saw/examples/linked_list_proofs.v
@@ -312,7 +312,7 @@ Section any.
               (returnM (intToBv 64 0))
               (fun y l' rec =>
                  f y >>= fun call_ret_val =>
-                  if not (bvEq 64 call_ret_val (intToBv 64 0))
+                  if negb (bvEq 64 call_ret_val (intToBv 64 0))
                   then returnM (intToBv 64 1) else rec).
 
   Lemma any_fun_ref : refinesFun any any_fun.
diff --git a/saw-core-coq/.gitignore b/saw-core-coq/.gitignore
index 159b7da69f..8952e041f0 100644
--- a/saw-core-coq/.gitignore
+++ b/saw-core-coq/.gitignore
@@ -3,3 +3,4 @@
 *.v.d
 *.vok
 *.vos
+.lia.cache
diff --git a/saw-core-coq/coq/_CoqProject b/saw-core-coq/coq/_CoqProject
index 88baafbdfb..66f5300e6b 100644
--- a/saw-core-coq/coq/_CoqProject
+++ b/saw-core-coq/coq/_CoqProject
@@ -9,6 +9,7 @@ handwritten/CryptolToCoq/CompMExtra.v
 handwritten/CryptolToCoq/CoqVectorsExtra.v
 handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v
 handwritten/CryptolToCoq/SAWCoreBitvectors.v
+handwritten/CryptolToCoq/SAWCoreBitvectorsZifyU64.v
 handwritten/CryptolToCoq/SAWCorePrelude_proofs.v
 handwritten/CryptolToCoq/SAWCorePreludeExtra.v
 handwritten/CryptolToCoq/SAWCoreScaffolding.v
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
index 581843c983..87966b38e8 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v
@@ -23,15 +23,12 @@ Tactic Notation "dependent" "destruction" ident(H) :=
 (*   match goal with H: _ |- _ => constr:(H) end. *)
 
 Tactic Notation "unfold_projs" :=
-  unfold SAWCoreScaffolding.fst, SAWCoreScaffolding.snd;
   cbn [ Datatypes.fst Datatypes.snd projT1 ].
 
 Tactic Notation "unfold_projs" "in" constr(N) :=
-  unfold SAWCoreScaffolding.fst, SAWCoreScaffolding.snd in N;
   cbn [ Datatypes.fst Datatypes.snd projT1 ] in N.
 
 Tactic Notation "unfold_projs" "in" "*" :=
-  unfold SAWCoreScaffolding.fst, SAWCoreScaffolding.snd in *;
   cbn [ Datatypes.fst Datatypes.snd projT1 ] in *.
 
 Ltac split_prod_hyps :=
@@ -769,11 +766,11 @@ Hint Extern 999 (refinesFun _ _) => shelve : refinesFun.
 
 Definition refinesFun_multiFixM_fst' lrt (F:lrtPi (LRT_Cons lrt LRT_Nil)
                                               (lrtTupleType (LRT_Cons lrt LRT_Nil))) f
-  (ref_f:refinesFun (SAWCoreScaffolding.fst (F f)) f) :
+  (ref_f:refinesFun (fst (F f)) f) :
   refinesFun (fst (multiFixM F)) f := refinesFun_multiFixM_fst lrt F f ref_f.
 
 Definition refinesFun_fst lrt B f1 (fs:B) f2 (r:@refinesFun lrt f1 f2) :
-  refinesFun (SAWCoreScaffolding.fst (f1, fs)) f2 := r.
+  refinesFun (fst (f1, fs)) f2 := r.
 
 Hint Resolve refinesFun_fst | 1 : refinesFun.
 Hint Resolve refinesFun_multiFixM_fst' | 1 : refinesFun.
@@ -849,7 +846,7 @@ 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; unfold Eq, Refl, SAWCoreScaffolding.Bool;
+  unfold_projs;
   apply StartAutomation_fold;
   prove_refinement_core with opts.
 
@@ -951,7 +948,7 @@ Module CompMExtraNotation.
   Declare Scope fun_syntax.
 
 
-  Infix "&&" := SAWCoreScaffolding.and : fun_syntax.
+  Infix "&&" := andb : fun_syntax.
   Infix "<=" := (SAWCoreVectorsAsCoqVectors.bvsle _) : fun_syntax.
   Notation " a <P b" := (SAWCorePrelude.bvultWithProof _ a b) (at level 98) : fun_syntax.
   Notation " a == b" := (SAWCorePrelude.bvEq _ a b) (at level 100) : fun_syntax.
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v
index 2afacbeb1e..75371e79c1 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v
@@ -18,11 +18,11 @@ Import ListNotations.
 (** It is annoying to have to wrap natural numbers into [TCNum] to use them at
 type [Num], so these coercions will do it for us.
  *)
-Coercion TCNum : Nat >-> Num.
+Coercion TCNum : nat >-> Num.
 Definition natToNat (n : nat) : Nat := n.
 Coercion natToNat : nat >-> Nat.
 
-Theorem Eq_TCNum a b : a = b -> Eq _ (TCNum a) (TCNum b).
+Theorem Eq_TCNum a b : a = b -> eq (TCNum a) (TCNum b).
 Proof.
   intros EQ.
   apply f_equal.
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
index 4a5dad9cf1..eeef4d8fc7 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
@@ -83,7 +83,7 @@ Ltac compute_bv_funs_tac H t compute_bv_binrel compute_bv_binop
 
 Ltac unfold_bv_funs := unfold bvNat, bvultWithProof, bvuleWithProof,
                               bvsge, bvsgt, bvuge, bvugt, bvSCarry, bvSBorrow,
-                              xor, xorb.
+                              xorb.
 
 Tactic Notation "compute_bv_funs" :=
   unfold_bv_funs;
@@ -354,7 +354,7 @@ Proof. holds_for_bits_up_to_3. Qed.
 (** Lemmas about bitvector xor **)
 
 Lemma bvXor_same n x :
-  SAWCorePrelude.bvXor n x x = SAWCorePrelude.replicate n Bool false.
+  SAWCorePrelude.bvXor n x x = SAWCorePrelude.replicate n bool false.
 Proof.
   unfold SAWCorePrelude.bvXor, SAWCorePrelude.bvZipWith, SAWCorePrelude.zipWith, SAWCorePrelude.replicate.
   induction x; auto; simpl; f_equal; auto.
@@ -362,7 +362,7 @@ Proof.
 Qed.
 
 Lemma bvXor_zero n x :
-  SAWCorePrelude.bvXor n x (SAWCorePrelude.replicate n Bool false) = x.
+  SAWCorePrelude.bvXor n x (SAWCorePrelude.replicate n bool false) = x.
 Proof.
   unfold SAWCorePrelude.bvXor, SAWCorePrelude.bvZipWith, SAWCorePrelude.zipWith, SAWCorePrelude.replicate.
   induction x; auto; simpl. f_equal; auto; cbn.
@@ -375,7 +375,7 @@ Lemma bvXor_assoc n x y z :
 Proof.
   unfold SAWCorePrelude.bvXor, SAWCorePrelude.bvZipWith, SAWCorePrelude.zipWith.
   induction n; auto; simpl. f_equal; auto; cbn.
-  unfold xor. rewrite Bool.xorb_assoc_reverse. reflexivity.
+  rewrite Bool.xorb_assoc_reverse. reflexivity.
   remember (S n).
   destruct x; try solve [inversion Heqn0; clear Heqn0; subst]. injection Heqn0.
   destruct y; try solve [inversion Heqn0; clear Heqn0; subst]. injection Heqn0.
@@ -388,7 +388,7 @@ Lemma bvXor_comm n x y :
 Proof.
   unfold SAWCorePrelude.bvXor, SAWCorePrelude.bvZipWith, SAWCorePrelude.zipWith.
   induction n; auto; simpl. f_equal; auto; cbn.
-  unfold xor. apply Bool.xorb_comm.
+  apply Bool.xorb_comm.
   remember (S n).
   destruct x; try solve [inversion Heqn0; clear Heqn0; subst]. injection Heqn0.
   destruct y; try solve [inversion Heqn0; clear Heqn0; subst]. injection Heqn0.
@@ -407,38 +407,38 @@ 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).
+Lemma and_bool_eq_true b c : andb 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 b c : and b c = false <-> (b = false) \/ (c = false).
+Lemma and_bool_eq_false b c : andb b c = false <-> (b = false) \/ (c = false).
 Proof.
   split.
   - destruct b, c; auto.
   - intro; destruct H; destruct b, c; auto.
 Qed.
 
-Lemma or_bool_eq_true b c : or b c = true <-> (b = true) \/ (c = true).
+Lemma or_bool_eq_true b c : orb 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 b c : or b c = false <-> (b = false) /\ (c = false).
+Lemma or_bool_eq_false b c : orb b c = false <-> (b = false) /\ (c = false).
 Proof.
   split.
   - destruct b, c; auto.
   - intro; destruct H; destruct b, c; auto.
 Qed.
 
-Lemma not_bool_eq_true b : not b = true <-> b = false.
+Lemma not_bool_eq_true b : negb b = true <-> b = false.
 Proof. split; destruct b; auto. Qed.
 
-Lemma not_bool_eq_false b : not b = false <-> b = true.
+Lemma not_bool_eq_false b : negb b = false <-> b = true.
 Proof. split; destruct b; auto. Qed.
 
 
@@ -446,7 +446,7 @@ Proof. split; destruct b; auto. Qed.
 
 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).
+  andb (boolEq h0 h1) (bvEq w a0 a1).
 Proof. reflexivity. Qed.
 
 Lemma bvEq_refl w a : bvEq w a a = true.
@@ -485,13 +485,6 @@ Qed.
 
 Hint Extern 1 (StartAutomation _) => progress compute_bv_funs: refinesFun.
 
-Lemma true_eq_scaffolding_true : Datatypes.true = SAWCoreScaffolding.true.
-Proof. reflexivity. Qed.
-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;
@@ -551,14 +544,14 @@ Proof. intros H eq; apply H; destruct b; easy. Qed.
 
 Lemma IntroArg_and_bool_eq_true n (b c : bool) goal :
   IntroArg n (b = true) (fun _ => FreshIntroArg n (c = true) (fun _ => goal)) ->
-  IntroArg n (and b c = true) (fun _ => goal).
+  IntroArg n (andb b c = true) (fun _ => goal).
 Proof.
   intros H eq; apply H; apply and_bool_eq_true in eq; destruct eq; eauto.
 Qed.
 Lemma IntroArg_and_bool_eq_false n (b c : bool) goal :
   IntroArg n (b = false) (fun _ => goal) ->
   IntroArg n (c = false) (fun _ => goal) ->
-  IntroArg n (and b c = false) (fun _ => goal).
+  IntroArg n (andb b c = false) (fun _ => goal).
 Proof.
   intros Hl Hr eq; apply and_bool_eq_false in eq.
   destruct eq; [ apply Hl | apply Hr ]; eauto.
@@ -572,14 +565,14 @@ Qed.
 Lemma IntroArg_or_bool_eq_true n (b c : bool) goal :
   IntroArg n (b = true) (fun _ => goal) ->
   IntroArg n (c = true) (fun _ => goal) ->
-  IntroArg n (or b c = true) (fun _ => goal).
+  IntroArg n (orb b c = true) (fun _ => goal).
 Proof.
   intros Hl Hr eq; apply or_bool_eq_true in eq.
   destruct eq; [ apply Hl | apply Hr ]; eauto.
 Qed.
 Lemma IntroArg_or_bool_eq_false n (b c : bool) goal :
   IntroArg n (b = false) (fun _ => FreshIntroArg n (c = false) (fun _ => goal)) ->
-  IntroArg n (or b c = false) (fun _ => goal).
+  IntroArg n (orb b c = false) (fun _ => goal).
 Proof.
   intros H eq; apply H; apply or_bool_eq_false in eq; destruct eq; eauto.
 Qed.
@@ -591,11 +584,11 @@ Qed.
 
 Lemma IntroArg_not_bool_eq_true n (b : bool) goal :
   IntroArg n (b = false) (fun _ => goal) ->
-  IntroArg n (not b = true) (fun _ => goal).
+  IntroArg n (negb b = true) (fun _ => goal).
 Proof. intros H eq; 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).
+  IntroArg n (negb b = false) (fun _ => goal).
 Proof. intros H eq; apply H, not_bool_eq_false; eauto. Qed.
 
 (* Hint Extern 1 (IntroArg _ (not _ = true) _) => *)
@@ -647,9 +640,9 @@ Hint Extern 1 (IntroArg _ (@eq bool ?x ?y) _) =>
   lazymatch y with
   | true => lazymatch x with
     | SAWCorePrelude.bvEq _ _ _ => simple apply IntroArg_bvEq_eq
-    | and _ _ => simple apply IntroArg_and_bool_eq_true
-    | or _ _ => simple apply IntroArg_or_bool_eq_true
-    | not _ => simple apply IntroArg_not_bool_eq_true
+    | andb _ _ => simple apply IntroArg_and_bool_eq_true
+    | orb _ _ => simple apply IntroArg_or_bool_eq_true
+    | negb _ => simple apply IntroArg_not_bool_eq_true
     | boolEq _ _ => simple apply IntroArg_boolEq_eq
     | if _ then true   else false  => simple apply IntroArg_bool_eq_if_true
     | if _ then 1%bool else 0%bool => simple apply IntroArg_bool_eq_if_true
@@ -658,9 +651,9 @@ Hint Extern 1 (IntroArg _ (@eq bool ?x ?y) _) =>
     end
   | false => lazymatch x with
     | SAWCorePrelude.bvEq _ _ _ => simple apply IntroArg_bvEq_neq
-    | and _ _ => simple apply IntroArg_and_bool_eq_false
-    | or _ _ => simple apply IntroArg_or_bool_eq_false
-    | not _ => simple apply IntroArg_not_bool_eq_false
+    | andb _ _ => simple apply IntroArg_and_bool_eq_false
+    | orb _ _ => simple apply IntroArg_or_bool_eq_false
+    | negb _ => simple apply IntroArg_not_bool_eq_false
     | boolEq _ _ => simple apply IntroArg_boolEq_neq
     | if _ then true   else false  => simple apply IntroArg_bool_eq_if_false
     | if _ then 1%bool else 0%bool => simple apply IntroArg_bool_eq_if_false
@@ -694,10 +687,6 @@ Proof. intros H eq; apply H; eauto. Qed.
 Hint Extern 1 (IntroArg _ (iteDep (fun _ => Maybe (Eq _ _ _)) true _ _ = _) _) =>
    simple apply IntroArg_iteDep_Maybe_Eq_true : refinesFun.
 Hint Extern 1 (IntroArg _ (iteDep (fun _ => Maybe (Eq _ _ _)) false _ _ = _) _) =>
-simple apply IntroArg_iteDep_Maybe_Eq_false : refinesFun.
-Hint Extern 1 (IntroArg _ (iteDep (fun _ => Maybe (Eq _ _ _)) Datatypes.true _ _ = _) _) =>
-   simple apply IntroArg_iteDep_Maybe_Eq_true : refinesFun.
-Hint Extern 1 (IntroArg _ (iteDep (fun _ => Maybe (Eq _ _ _)) Datatypes.false _ _ = _) _) =>
    simple apply IntroArg_iteDep_Maybe_Eq_false : refinesFun.
 
 Lemma IntroArg_isBvsle_def n w a b goal
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectorsZifyU64.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectorsZifyU64.v
new file mode 100644
index 0000000000..877620e802
--- /dev/null
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectorsZifyU64.v
@@ -0,0 +1,377 @@
+From Coq Require Import Classes.Morphisms.
+From Coq Require Import Lia.
+From Coq Require Import ZArith.BinInt.
+From Coq Require Import ZifyBool.
+From Coq Require Import ZifyClasses.
+
+From CryptolToCoq Require Import SAWCoreBitvectors.
+From CryptolToCoq Require Import SAWCorePrelude.
+From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
+
+Import SAWCorePrelude.
+
+(* This file defines the necessary Zify-related instances to be able to use the
+   `lia` tactic on many theorems involving `bitvector 64` equalities and
+   inequalities. This file includes a small number of proofs to test that `lia`
+   is working as intended. The design was heavily inspired by the Zify instances
+   for Coq's Uint63, which can be found here:
+   https://github.com/coq/coq/blob/756c560ab5d19a1568cf41caac6f0d67a97b08c6/theories/micromega/ZifyUint63.v
+
+   This is far from complete, however. Be aware of the following caveats:
+
+   1. These instances only work over unsigned arithmetic, so theorems involving
+      signed arithmetic are not supported. If we wanted to support signed
+      arithmetic, we would likely need to take inspiration from how Coq's Zify
+      instances for the Sint63 type work:
+      https://github.com/coq/coq/blob/756c560ab5d19a1568cf41caac6f0d67a97b08c6/theories/micromega/ZifySint63.v
+
+   2. There are likely many operations that are not covered here. If there is
+      an unsupported operation that you would like to see added, please file an
+      issue to the saw-script repo.
+
+   3. These instances only support bitvectors where the bit width is 64.
+      Ideally, we would make the Zify instances parametric in the bit width, but
+      this is surprisingly difficult to accomplish. At a minimum, this would
+      require some upstream changes to Coq. See, for instance,
+      https://github.com/coq/coq/issues/16404.
+
+      For now, we simply provide the machinery at 64 bits, which is a common
+      case. If there is enough demand, we can also provide similar machinery
+      for bitvectors at other common bit widths.
+*)
+
+(* Unfortunately, https://github.com/coq/coq/issues/16404 prevents us from
+   simply defining instances for `bitvector 64`, so we provide a thin wrapper
+   around it and define instances for it. We may be able to remove this
+   workaround once the upstream Coq issue is fixed and enough time has passed.
+*)
+Definition bitvector_64 := bitvector 64.
+
+(* Notations *)
+
+(* 2^64 *)
+Notation modulus := 0x10000000000000000%Z.
+
+Notation Zadd_mod_64 x y :=
+  (Z.modulo (Z.add x y) modulus).
+
+Notation Zsub_mod_64 x y :=
+  (Z.modulo (Z.sub x y) modulus).
+
+Notation Zmul_mod_64 x y :=
+  (Z.modulo (Z.mul x y) modulus).
+
+Notation bv64_bounded x :=
+  (Z.le 0 x /\ Z.lt x modulus).
+
+(* Auxiliary lemmas *)
+
+Lemma bvToInt_inj w a b :
+  bvToInt w a = bvToInt w b ->
+  a = b.
+Proof. holds_for_bits_up_to_3. Qed.
+
+Lemma of_nat_bvToNat_bvToInt w a :
+  Z.of_nat (bvToNat w a) = bvToInt w a.
+Proof. holds_for_bits_up_to_3. Qed.
+
+Lemma msb_Ztestbit w a :
+  msb w a = Z.testbit (bvToInt (S w) a) (Z.of_nat w).
+Proof. holds_for_bits_up_to_3. Qed.
+
+Global Instance Proper_bvToInt_le w :
+  Proper (isBvule w ==> Z.le) (bvToInt w).
+Proof. holds_for_bits_up_to_3. Qed.
+
+Global Instance Proper_bvToInt_lt w :
+  Proper (isBvult w ==> Z.lt) (bvToInt w).
+Proof. holds_for_bits_up_to_3. Qed.
+
+(* See zify_ubv64.cry for a version of this lemma that can be proven with
+   an SMT solver. In particular, run the following:
+
+   > :prove bvAdd_Zadd_mod`{3}
+ *)
+Lemma bvAdd_Zadd_mod_64 a b :
+  bvToInt 64 (bvAdd 64 a b) =
+  Zadd_mod_64 (bvToInt 64 a) (bvToInt 64 b).
+Admitted.
+
+(* See zify_ubv64.cry for a version of this lemma that can be proven with
+   an SMT solver. In particular, run the following:
+
+   > :prove bvSub_Zsub_mod`{3}
+ *)
+Lemma bvSub_Zsub_mod_64 a b :
+  bvToInt 64 (bvSub 64 a b) =
+  Zsub_mod_64 (bvToInt 64 a) (bvToInt 64 b).
+Admitted.
+
+(* See zify_ubv64.cry for a version of this lemma that can be proven with
+   an SMT solver. In particular, run the following:
+
+   > :prove bvMul_Zmul_mod`{3}
+ *)
+Lemma bvMul_Zmul_mod_64 a b :
+  bvToInt 64 (bvMul 64 a b) =
+  Zmul_mod_64 (bvToInt 64 a) (bvToInt 64 b).
+Admitted.
+
+(* See zify_ubv64.cry for a version of this lemma that can be proven with
+   an SMT solver. In particular, run the following:
+
+   > :prove bvToInt_intToBv`{3}
+ *)
+Lemma bvToInt_intToBv_64 (a : Z) :
+  bvToInt 64 (intToBv 64 a) = Z.modulo a modulus.
+Admitted.
+
+Lemma bvule_Zleb w a b :
+  bvule w a b =
+  Z.leb (bvToInt w a) (bvToInt w b).
+Proof. holds_for_bits_up_to_3. Qed.
+
+Lemma bvult_Zltb w a b :
+  bvult w a b =
+  Z.ltb (bvToInt w a) (bvToInt w b).
+Proof. holds_for_bits_up_to_3. Qed.
+
+Lemma bvEq_Zeqb w a b :
+  bvEq w a b =
+  Z.eqb (bvToInt w a) (bvToInt w b).
+Proof. holds_for_bits_up_to_3. Qed.
+
+Lemma Zle_bvToInt_to_isBvule w a b :
+  Z.le (bvToInt w a) (bvToInt w b) ->
+  isBvule w a b.
+Proof. holds_for_bits_up_to_3. Qed.
+
+Lemma Zlt_bvToInt_to_isBvult w a b :
+  Z.lt (bvToInt w a) (bvToInt w b) ->
+  isBvult w a b.
+Proof. holds_for_bits_up_to_3. Qed.
+
+Lemma bvToInt_lt_max w a :
+  Z.lt (bvToInt w a) (Z.pow 2 (Z.of_nat w)).
+Proof. holds_for_bits_up_to_3. Qed.
+
+Lemma bvToInt_64_bounded :
+  forall (x : bitvector 64),
+  bv64_bounded (bvToInt 64 x).
+Proof.
+  intros x. split.
+  - change 0%Z with (bvToInt 64 (intToBv 64 0)).
+    apply Proper_bvToInt_le.
+    apply isBvule_zero_n.
+  - change modulus with (Z.pow 2 (Z.of_nat 64)).
+    apply bvToInt_lt_max.
+Qed.
+
+(* Zify-related instances *)
+
+Global Instance Inj_bv64_Z : InjTyp bitvector_64 Z :=
+  { inj := bvToInt 64
+  ; pred := fun x => bv64_bounded x
+  ; cstr := bvToInt_64_bounded
+  }.
+Add Zify InjTyp Inj_bv64_Z.
+
+Global Instance Op_bvumin : CstOp (bvumin 64 : bitvector_64) :=
+  { TCst := 0%Z
+  ; TCstInj := eq_refl
+  }.
+Add Zify CstOp Op_bvumin.
+
+Global Instance Op_bvumax : CstOp (bvumax 64 : bitvector_64) :=
+  { TCst := 0xffffffffffffffff%Z
+  ; TCstInj := eq_refl
+  }.
+Add Zify CstOp Op_bvumax.
+
+Global Instance Op_bvsmin : CstOp (bvsmin 64 : bitvector_64) :=
+  { TCst := 0x8000000000000000%Z
+  ; TCstInj := eq_refl
+  }.
+Add Zify CstOp Op_bvsmin.
+
+Global Instance Op_bvsmax : CstOp (bvsmax 64 : bitvector_64) :=
+  { TCst := 0x7fffffffffffffff%Z
+  ; TCstInj := eq_refl
+  }.
+Add Zify CstOp Op_bvsmax.
+
+Global Program Instance Op_msb : UnOp (msb 63 : bitvector_64 -> bool) :=
+  { TUOp := fun x => Z.testbit x 63
+  ; TUOpInj := _
+  }.
+Next Obligation.
+  apply msb_Ztestbit.
+Qed.
+Add Zify UnOp Op_msb.
+
+Global Instance Op_intToBv : UnOp (intToBv 64 : Z -> bitvector_64) :=
+  { TUOp := fun x => Z.modulo x modulus
+  ; TUOpInj := bvToInt_intToBv_64
+  }.
+Add Zify UnOp Op_intToBv.
+
+Global Instance Op_bvToNat : UnOp (bvToNat 64 : bitvector_64 -> nat) :=
+  { TUOp := fun x => x
+  ; TUOpInj := of_nat_bvToNat_bvToInt 64
+  }.
+Add Zify UnOp Op_bvToNat.
+
+Global Instance Op_bvNat : UnOp (bvNat 64 : nat -> bitvector_64) :=
+  { TUOp := fun x => Z.modulo x modulus
+  ; TUOpInj := fun n => bvToInt_intToBv_64 (Z.of_nat n)
+  }.
+Add Zify UnOp Op_bvNat.
+
+Global Instance Op_bvAdd : BinOp (bvAdd 64 : bitvector_64 -> bitvector_64 -> bitvector_64) :=
+  { TBOp := fun x y => Zadd_mod_64 x y
+  ; TBOpInj := bvAdd_Zadd_mod_64
+  }.
+Add Zify BinOp Op_bvAdd.
+
+Global Instance Op_bvSub : BinOp (bvSub 64 : bitvector_64 -> bitvector_64 -> bitvector_64) :=
+  { TBOp := fun x y => Zsub_mod_64 x y
+  ; TBOpInj := bvSub_Zsub_mod_64
+  }.
+Add Zify BinOp Op_bvSub.
+
+Global Instance Op_bvMul : BinOp (bvMul 64 :bitvector_64 -> bitvector_64 -> bitvector_64) :=
+  { TBOp := fun x y => Zmul_mod_64 x y
+  ; TBOpInj := bvMul_Zmul_mod_64
+  }.
+Add Zify BinOp Op_bvMul.
+
+Global Instance Op_bvule : BinOp (bvule 64 : bitvector_64 -> bitvector_64 -> bool) :=
+  { TBOp := Z.leb
+  ; TBOpInj := bvule_Zleb 64
+  }.
+Add Zify BinOp Op_bvule.
+
+Global Instance Op_bvult : BinOp (bvult 64 : bitvector_64 -> bitvector_64 -> bool) :=
+  { TBOp := Z.ltb
+  ; TBOpInj := bvult_Zltb 64
+  }.
+Add Zify BinOp Op_bvult.
+
+Global Instance Op_bvEq : BinOp (bvEq 64 : bitvector_64 -> bitvector_64 -> bool) :=
+  { TBOp := Z.eqb
+  ; TBOpInj := bvEq_Zeqb 64
+  }.
+Add Zify BinOp Op_bvEq.
+
+Global Program Instance Rel_isBvule : BinRel (isBvule 64 : bitvector_64 -> bitvector_64 -> Prop) :=
+  { TR := Z.le
+  ; TRInj := _
+  }.
+Next Obligation.
+  split.
+  - apply Proper_bvToInt_le.
+  - apply Zle_bvToInt_to_isBvule.
+Qed.
+Add Zify BinRel Rel_isBvule.
+
+Global Program Instance Rel_isBvult : BinRel (isBvult 64 : bitvector_64 -> bitvector_64 -> Prop) :=
+  { TR := Z.lt
+  ; TRInj := _
+  }.
+Next Obligation.
+  split.
+  - apply Proper_bvToInt_lt.
+  - apply Zlt_bvToInt_to_isBvult.
+Qed.
+Add Zify BinRel Rel_isBvult.
+
+Global Program Instance Rel_eq : BinRel (@eq bitvector_64) :=
+  { TR := @eq Z
+  ; TRInj := _
+  }.
+Next Obligation.
+  split; intros H.
+  - rewrite -> H. reflexivity.
+  - apply (bvToInt_inj _ _ _ H).
+Qed.
+Add Zify BinRel Rel_eq.
+
+Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true).
+
+(* Test cases *)
+
+Lemma bv64_refl (x : bitvector 64) : x = x.
+Proof. lia. Qed.
+
+Lemma bvAdd_comm (x y : bitvector 64) : bvAdd 64 x y = bvAdd 64 y x.
+Proof. lia. Qed.
+
+Lemma isBvult_bvSub (x y : bitvector 64) : isBvult 64 (bvSub 64 x (intToBv 64 1)) y ->
+                                           isBvult 64 (bvSub 64 y x) y.
+Proof. lia. Qed.
+
+Lemma isBvule_bvSub (x y : bitvector 64) : isBvule 64 x y ->
+                                           isBvule 64 (bvSub 64 y x) y.
+Proof. lia. Qed.
+
+Lemma isBvult_is_Bvule (x y z : bitvector 64) :
+  isBvult 64 x y -> isBvule 64 y z -> isBvult 64 x z.
+Proof. lia. Qed.
+
+Lemma bvNat_bvToNat_inv (x : bitvector 64) : bvNat 64 (bvToNat 64 x) = x.
+Proof. lia. Qed.
+
+Lemma isBvule_antisymm a b : isBvule 64 a b -> isBvule 64 b a -> a = b.
+Proof. lia. Qed.
+
+Lemma bvEq_neq':
+  forall (a b : bitvector 64), bvEq 64 a b = false <-> a <> b.
+Proof. lia. Qed.
+
+Lemma bvSub_bvAdd_cancel a b : bvSub 64 (bvAdd 64 a b) b = a.
+Proof. lia. Qed.
+
+Lemma bvSub_bvAdd_distrib a b c :
+  bvSub 64 a (bvAdd 64 b c) = bvSub 64 (bvSub 64 a b) c.
+Proof. lia. Qed.
+
+Lemma bvSub_left_cancel a b :
+  bvSub 64 b (bvSub 64 b a) = a.
+Proof. lia. Qed.
+
+Lemma bvToNat_bvAdd_succ a :
+  isBvult 64 a (bvumax 64) ->
+  bvToNat 64 (bvAdd 64 a (intToBv 64 1)) = S (bvToNat 64 a).
+Proof. lia. Qed.
+
+Lemma isBvult_bvSub_zero
+        (a b : bitvector 64) :
+      isBvult 64 a b ->
+      isBvult 64 (intToBv 64 0) (bvSub 64 b a).
+Proof. lia. Qed.
+
+Lemma isBvult_bvToNat
+        (a b : bitvector 64) :
+      isBvult 64 a b ->
+      bvToNat 64 a < bvToNat 64 b.
+Proof. lia. Qed.
+
+Lemma isBvule_bvToNat
+        (a b : bitvector 64) :
+      isBvule 64 a b ->
+      bvToNat 64 a <= bvToNat 64 b.
+Proof. lia. Qed.
+
+Lemma bvToNat_bvSub
+        (a b : bitvector 64) :
+      isBvult 64 a b ->
+      bvToNat 64 (bvSub 64 b a) = bvToNat 64 b - bvToNat 64 a.
+Proof. lia. Qed.
+
+Lemma bvToNat_intToBv_0 :
+  bvToNat 64 (intToBv 64 0) = 0.
+Proof. lia. Qed.
+
+Lemma bvAdd_succ n :
+  bvAdd 64 (bvNat 64 n) (intToBv 64 1) = bvNat 64 (S n).
+Proof. lia. Qed.
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
index 05b4f07f10..86e41a5d22 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
@@ -89,6 +89,6 @@ Proof.
   all: try rewrite IHD; try rewrite IHD1; try rewrite IHD2; try rewrite H; try easy.
   (* All that remains is the IRT_BVVec case, which requires functional extensionality
      and the fact that genBVVec and atBVVec define an isomorphism *)
-  intros; rewrite <- (gen_at_BVVec _ _ _ u).
+  etransitivity; [ | apply gen_at_BVVec ].
   f_equal; repeat (apply functional_extensionality_dep; intro); eauto.
 Qed.
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePrelude_proofs.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePrelude_proofs.v
index 29845b25e4..df79fe61bb 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePrelude_proofs.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePrelude_proofs.v
@@ -121,7 +121,7 @@ Proof.
 Qed.
 
 Lemma gen_sawAt T {HT : Inhabited T}
-  : forall (m : Nat) a, gen m T (fun i => sawAt m T a i) = a.
+  : forall (m : nat) a, gen m T (fun i => sawAt m T a i) = a.
 Proof.
   apply Vector.t_ind.
   {
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v
index 67dd26a5c6..26f31c1f9f 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v
@@ -44,12 +44,12 @@ Proof. intros; exact inhabitant. Qed.
 
 Definition sort (n : nat) := Type.
 
-Instance Inhabited_Type : Inhabited Type :=
+Global Instance Inhabited_Type : Inhabited Type :=
   MkInhabited Type unit.
-Instance Inhabited_sort (n:nat) : Inhabited (sort n) :=
+Global Instance Inhabited_sort (n:nat) : Inhabited (sort n) :=
   MkInhabited (sort n) unit.
 
-Instance Inhabited_Intro (a:Type) (b:a -> Type) (Hb: forall x, Inhabited (b x))
+Global Instance Inhabited_Intro (a:Type) (b:a -> Type) (Hb: forall x, Inhabited (b x))
   : Inhabited (forall x, b x)
   := MkInhabited (forall x, b x) (fun x => @inhabitant (b x) (Hb x)).
 
@@ -61,46 +61,60 @@ Global Hint Extern 5 (Inhabited ?A) =>
  *** Definitions for things in the Prelude
  ***)
 
+(** DEPRECATED: Use [string] instead. *)
 Definition String := String.string.
 
-Instance Inhabited_String : Inhabited String :=
+Global Instance Inhabited_String : Inhabited String :=
   MkInhabited String ""%string.
-Instance Inhabited_string : Inhabited String.string :=
+Global Instance Inhabited_string : Inhabited String.string :=
   MkInhabited String.string ""%string.
 
-Definition equalString (s1 s2: String) : bool :=
+Definition equalString (s1 s2: string) : bool :=
   match String.string_dec s1 s2 with
   | left _ => true
   | right _ => false
   end.
 
-Definition appendString : String -> String -> String :=
+Definition appendString : string -> string -> string :=
   String.append.
 
 Definition Unit        := tt.
 Definition UnitType    := unit.
 Definition UnitType__rec := unit_rect.
 
+(** DEPRECATED: Use [bool] instead. *)
 Definition Bool   := bool.
+
+(** DEPRECATED: Use [eq] instead. *)
 Definition Eq     := @eq.
+
+(** DEPRECATED: Use [eq_refl] instead. *)
 Definition Refl   := @eq_refl.
-Definition true      := true.
+
 Definition ite (a : Type) (b : Bool) (t e : a) : a := if b then t else e.
+
+(** DEPRECATED: Use [andb] instead. *)
 Definition and    := andb.
-Definition false      := false.
+
+(** DEPRECATED: Use [negb] instead. *)
 Definition not      := negb.
+
+(** DEPRECATED: Use [orb] instead. *)
 Definition or     := orb.
+
+(** DEPRECATED: Use [xorb] instead. *)
 Definition xor    := xorb.
+
 Definition boolEq := Coq.Bool.Bool.eqb.
 
-Instance Inhabited_Unit : Inhabited UnitType :=
+Global Instance Inhabited_Unit : Inhabited UnitType :=
   MkInhabited UnitType tt.
-Instance Inhabited_Bool : Inhabited Bool :=
+Global Instance Inhabited_Bool : Inhabited Bool :=
   MkInhabited Bool false.
 
-Instance Inhabited_unit : Inhabited unit :=
+Global Instance Inhabited_unit : Inhabited unit :=
   MkInhabited unit tt.
-Instance Inhabited_bool : Inhabited bool :=
+Global Instance Inhabited_bool : Inhabited bool :=
   MkInhabited bool false.
 
 (* SAW uses an alternate form of eq_rect where the motive function P also
@@ -110,66 +124,66 @@ Definition Eq__rec (A : Type) (x : A) (P: forall y, x=y -> Type) (p:P x eq_refl)
   dependent inversion e; assumption.
 Defined.
 
-Theorem boolEq__eq (b1 b2:Bool) : Eq Bool (boolEq b1 b2) (ite Bool b1 b2 (not b2)).
+Theorem boolEq__eq (b1 b2:bool) : (boolEq b1 b2) = (ite bool b1 b2 (negb b2)).
 Proof.
   destruct b1, b2; reflexivity.
 Qed.
 
-Definition coerce (a b : sort 0) (p : Eq (sort 0) a b) (x : a) : b :=
+Definition coerce (a b : sort 0) (p : @eq (sort 0) a b) (x : a) : b :=
   match p in eq _ a' return a' with
   | eq_refl _ => x
   end
 .
 
-(* SAW's prelude defines iteDep as a Bool eliminator whose arguments are
+(* SAW's prelude defines iteDep as a bool eliminator whose arguments are
 reordered to look more like if-then-else. *)
-Definition iteDep (P : Bool -> Type) (b : Bool) : P true -> P false -> P b :=
+Definition iteDep (P : bool -> Type) (b : bool) : P true -> P false -> P b :=
   fun Ptrue Pfalse => bool_rect P Ptrue Pfalse b.
 
-Definition ite_eq_iteDep : forall (a : Type) (b : Bool) (x y : a),
+Definition ite_eq_iteDep : forall (a : Type) (b : bool) (x y : a),
     @eq a (ite a b x y) (iteDep (fun _ => a) b x y).
 Proof.
   reflexivity.
 Defined.
 
-Definition iteDep_True : forall (p : Bool -> Type), forall (f1 : p true), forall (f2 : p false), (@eq (p true) (iteDep p true f1 f2)) f1.
+Definition iteDep_True : forall (p : bool -> Type), forall (f1 : p true), forall (f2 : p false), (@eq (p true) (iteDep p true f1 f2)) f1.
 Proof.
   reflexivity.
 Defined.
 
-Definition iteDep_False : forall (p : Bool -> Type), forall (f1 : p true), forall (f2 : p false), (@eq (p false) (iteDep p false f1 f2)) f2.
+Definition iteDep_False : forall (p : bool -> Type), forall (f1 : p true), forall (f2 : p false), (@eq (p false) (iteDep p false f1 f2)) f2.
 Proof.
   reflexivity.
 Defined.
 
-Definition not__eq (b : Bool) : @eq Bool (not b) (ite Bool b false true).
+Definition not__eq (b : bool) : @eq bool (negb b) (ite bool b false true).
 Proof.
   reflexivity.
 Defined.
 
-Definition and__eq (b1 b2 : Bool) : @eq Bool (and b1 b2) (ite Bool b1 b2 false).
+Definition and__eq (b1 b2 : bool) : @eq bool (andb b1 b2) (ite bool b1 b2 false).
 Proof.
   reflexivity.
 Defined.
 
-Definition or__eq (b1 b2 : Bool) : @eq Bool (or b1 b2) (ite Bool b1 true b2).
+Definition or__eq (b1 b2 : bool) : @eq bool (orb b1 b2) (ite bool b1 true b2).
 Proof.
   reflexivity.
 Defined.
 
-Definition xor__eq (b1 b2 : Bool) : @eq Bool (xor b1 b2) (ite Bool b1 (not b2) b2).
+Definition xor__eq (b1 b2 : bool) : @eq bool (xorb b1 b2) (ite bool b1 (negb b2) b2).
 Proof.
   destruct b1; destruct b2; reflexivity.
 Defined.
 
 (*
-Definition eq__eq (b1 b2 : Bool) : @eq Bool (eq b1 b2) (ite Bool b1 b2 (not b2)).
+Definition eq__eq (b1 b2 : bool) : @eq bool (eq b1 b2) (ite bool b1 b2 (negb b2)).
 Proof.
   destruct b1; destruct b2; reflexivity.
 Defined.
 *)
 
-Theorem ite_bit (b c d : Bool) : Eq Bool (ite Bool b c d) (and (or (not b) c) (or b d)).
+Theorem ite_bit (b c d : bool) : @eq bool (ite bool b c d) (andb (orb (negb b) c) (orb b d)).
 Proof.
   destruct b, c, d; reflexivity.
 Qed.
@@ -180,28 +194,31 @@ Definition sawCoerce {T : Type} (a b : Type) (_ : T) (x : a) := x.
 (* TODO: doesn't actually coerce *)
 Definition sawUnsafeCoerce (a b : Type) (x : a) := x.
 
+(** DEPRECATED: Use [nat] instead. *)
 Definition Nat := nat.
+
+(** DEPRECATED: Use [nat_rect] instead. *)
 Definition Nat_rect := nat_rect.
 
-Instance Inhabited_Nat : Inhabited Nat :=
+Global Instance Inhabited_Nat : Inhabited Nat :=
   MkInhabited Nat 0%nat.
-Instance Inhabited_nat : Inhabited nat :=
+Global Instance Inhabited_nat : Inhabited nat :=
   MkInhabited nat 0%nat.
 
 Global Hint Resolve (0%nat : nat) : inh.
 Global Hint Resolve (0%nat : Nat) : inh.
 
 Definition IsLeNat := @le.
-Definition IsLeNat_base (n:Nat) : IsLeNat n n := le_n n.
-Definition IsLeNat_succ (n m:Nat) : IsLeNat n m -> IsLeNat n (S m) := le_S n m.
+Definition IsLeNat_base (n:nat) : IsLeNat n n := le_n n.
+Definition IsLeNat_succ (n m:nat) : IsLeNat n m -> IsLeNat n (S m) := le_S n m.
 
 Definition IsLeNat__rec
-  (n : Nat)
-  (p : forall (x : Nat), IsLeNat n x -> Prop)
+  (n : nat)
+  (p : forall (x : nat), IsLeNat n x -> Prop)
   (Hbase : p n (IsLeNat_base n))
-  (Hstep : forall (x : Nat) (H : IsLeNat n x), p x H -> p (S x) (IsLeNat_succ n x H))
-  : forall (m : Nat) (Hm : IsLeNat n m), p m Hm :=
-  fix rec (m:Nat) (Hm : IsLeNat n m) {struct Hm} : p m Hm :=
+  (Hstep : forall (x : nat) (H : IsLeNat n x), p x H -> p (S x) (IsLeNat_succ n x H))
+  : forall (m : nat) (Hm : IsLeNat n m), p m Hm :=
+  fix rec (m:nat) (Hm : IsLeNat n m) {struct Hm} : p m Hm :=
             match Hm as Hm' in le _ m' return p m' Hm' with
             | le_n _ => Hbase
             | le_S _ m H => Hstep m H (rec m H)
@@ -212,9 +229,9 @@ Definition IsLeNat__rec
 Definition uncurry (a b c : Type) (f : a -> b -> c) (p : a * (b * unit)) : c  :=
   f (fst p) (fst (snd p)).
 
-Definition widthNat (n : Nat) : Nat := 1 + Nat.log2 n.
+Definition widthNat (n : nat) : nat := 1 + Nat.log2 n.
 
-Definition divModNat (x y : Nat) : (Nat * Nat) :=
+Definition divModNat (x y : nat) : (nat * nat) :=
   match y with
   | 0 => (y, y)
   | S y'=>
@@ -222,18 +239,21 @@ Definition divModNat (x y : Nat) : (Nat * Nat) :=
     (p, y' - q)
   end.
 
-Definition id := @id.
 Definition PairType := prod.
 Definition PairValue := @pair.
 Definition Pair__rec := prod_rect.
-Definition fst {A B} := @fst A B.
-Definition snd {A B} := @snd A B.
+
+(* NOTE: SAW core pair projections do not take type arguments, so these must be
+implicit arguments in the translation *)
+Arguments Datatypes.fst {_ _}.
+Arguments Datatypes.snd {_ _}.
+
 Definition Zero := O.
 Definition Succ := S.
 
-Instance Inhabited_Pair (a b:Type) {Ha : Inhabited a} {Hb : Inhabited b} : Inhabited (PairType a b) :=
+Global Instance Inhabited_Pair (a b:Type) {Ha : Inhabited a} {Hb : Inhabited b} : Inhabited (PairType a b) :=
     MkInhabited (PairType a b) (PairValue a b inhabitant inhabitant).
-Instance Inhabited_prod (a b:Type) {Ha : Inhabited a} {Hb : Inhabited b} : Inhabited (prod a b) :=
+Global Instance Inhabited_prod (a b:Type) {Ha : Inhabited a} {Hb : Inhabited b} : Inhabited (prod a b) :=
     MkInhabited (prod a b) (pair inhabitant inhabitant).
 
 
@@ -251,15 +271,15 @@ Definition intMin : Integer -> Integer -> Integer := Z.min.
 Definition intMax : Integer -> Integer -> Integer := Z.max.
 Definition intNeg : Integer -> Integer := Z.opp.
 Definition intAbs : Integer -> Integer := Z.abs.
-Definition intEq : Integer -> Integer -> Bool := Z.eqb.
-Definition intLe : Integer -> Integer -> Bool := Z.leb.
-Definition intLt : Integer -> Integer -> Bool := Z.ltb.
-Definition intToNat : Integer -> Nat := Z.to_nat.
-Definition natToInt : Nat -> Integer := Z.of_nat.
+Definition intEq : Integer -> Integer -> bool := Z.eqb.
+Definition intLe : Integer -> Integer -> bool := Z.leb.
+Definition intLt : Integer -> Integer -> bool := Z.ltb.
+Definition intToNat : Integer -> nat := Z.to_nat.
+Definition natToInt : nat -> Integer := Z.of_nat.
 
-Instance Inhabited_Intger : Inhabited Integer :=
+Global Instance Inhabited_Intger : Inhabited Integer :=
   MkInhabited Integer 0%Z.
-Instance Inhabited_Z : Inhabited Z :=
+Global Instance Inhabited_Z : Inhabited Z :=
   MkInhabited Z 0%Z.
 
 Global Hint Resolve (0%Z : Z) : inh.
@@ -272,21 +292,21 @@ Global Hint Resolve (0%Z : Integer) : inh.
 
 (* NOTE: the following will be nonsense for values of n <= 1 *)
 Definition IntMod (n : nat) := Z.
-Definition toIntMod (n : Nat) : Integer -> IntMod n := fun i => Z.modulo i (Z.of_nat n).
-Definition fromIntMod (n : Nat) : (IntMod n) -> Integer := ZModulo.to_Z (Pos.of_nat n).
+Definition toIntMod (n : nat) : Integer -> IntMod n := fun i => Z.modulo i (Z.of_nat n).
+Definition fromIntMod (n : nat) : (IntMod n) -> Integer := ZModulo.to_Z (Pos.of_nat n).
 Local Notation "[| a |]_ n" := (to_Z (Pos.of_nat n) a) (at level 0, a at level 99).
-Definition intModEq (n : Nat) (a : IntMod n) (b : IntMod n) : Bool
+Definition intModEq (n : nat) (a : IntMod n) (b : IntMod n) : bool
   := Z.eqb [| a |]_n [| b |]_n.
-Definition intModAdd : forall (n : Nat), (IntMod n) -> (IntMod n) -> IntMod n
+Definition intModAdd : forall (n : nat), (IntMod n) -> (IntMod n) -> IntMod n
   := fun _ => ZModulo.add.
-Definition intModSub : forall (n : Nat), (IntMod n) -> (IntMod n) -> IntMod n
+Definition intModSub : forall (n : nat), (IntMod n) -> (IntMod n) -> IntMod n
   := fun _ => ZModulo.sub.
-Definition intModMul : forall (n : Nat), (IntMod n) -> (IntMod n) -> IntMod n
+Definition intModMul : forall (n : nat), (IntMod n) -> (IntMod n) -> IntMod n
   := fun _ => ZModulo.mul.
-Definition intModNeg : forall (n : Nat), (IntMod n) -> IntMod n
+Definition intModNeg : forall (n : nat), (IntMod n) -> IntMod n
   := fun _ => ZModulo.opp.
 
-Instance Inhabited_IntMod (n:nat) : Inhabited (IntMod n) :=
+Global Instance Inhabited_IntMod (n:nat) : Inhabited (IntMod n) :=
   MkInhabited (IntMod n) 0%Z.
 
 (***
@@ -302,15 +322,15 @@ Variant RecordTypeNil : Type :=
   RecordNil : RecordTypeNil.
 
 (* A non-empty record type *)
-Variant RecordTypeCons (str:String.string) (tp:Type) (rest_tp:Type) : Type :=
+Variant RecordTypeCons (str:string) (tp:Type) (rest_tp:Type) : Type :=
   RecordCons (x:tp) (rest:rest_tp) : RecordTypeCons str tp rest_tp.
 
 Arguments RecordTypeCons str%string_scope tp rest_tp.
 Arguments RecordCons str%string_scope {tp rest_tp} x rest.
 
-Instance Inhabited_RecordNil : Inhabited RecordTypeNil :=
+Global Instance Inhabited_RecordNil : Inhabited RecordTypeNil :=
     MkInhabited RecordTypeNil RecordNil.
-Instance Inhabited_RecordCons (fnm:String.string) (tp rest_tp:Type)
+Global Instance Inhabited_RecordCons (fnm:string) (tp rest_tp:Type)
   {Htp : Inhabited tp} {Hrest : Inhabited rest_tp}
   : Inhabited (RecordTypeCons fnm tp rest_tp)
   := MkInhabited (RecordTypeCons fnm tp rest_tp) (RecordCons fnm inhabitant inhabitant).
@@ -328,14 +348,14 @@ Definition recordTail {str tp rest_tp} (r:RecordTypeCons str tp rest_tp) : rest_
   end.
 
 (* An inductive description of a string being a field in a record type *)
-Inductive IsRecordField (str:String) : Type -> Type :=
+Inductive IsRecordField (str:string) : Type -> Type :=
 | IsRecordField_Base tp rtp : IsRecordField str (RecordTypeCons str tp rtp)
 | IsRecordField_Step str' tp rtp : IsRecordField str rtp ->
                                    IsRecordField str (RecordTypeCons str' tp rtp).
 
 (* We want to use this as a typeclass, with its constructors for instances *)
 Existing Class IsRecordField.
-Hint Constructors IsRecordField : typeclass_instances.
+Global Hint Constructors IsRecordField : typeclass_instances.
 
 (* If str is a field in record type rtp, get its associated type *)
 Fixpoint getRecordFieldType rtp str `{irf:IsRecordField str rtp} : Type :=
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqLists.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqLists.v
index fde4c7bef3..2df6f21317 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqLists.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqLists.v
@@ -2,11 +2,23 @@ From Coq.Lists          Require Import List.
 From Coq.Numbers.NatInt Require        NZLog.
 From Coq.Strings        Require        String.
 From CryptolToCoq       Require Import SAWCoreScaffolding.
+From Coq                Require Import ZifyClasses.
 
 Import ListNotations.
 
 Definition Vec (n : nat) (a : Type) : Type := list a.
 
+(* Work around https://github.com/coq/coq/issues/16803. Without this, using
+   `lia` on `bitvector` values will fail to typecheck on pre-8.17 versions of
+   Coq. Once our Coq support window shifts enough, we can drop this workaround.
+*)
+Constraint Vec.u1 <= mkapp2.u0.
+Constraint Vec.u1 <= mkapp2.u1.
+Constraint Vec.u1 <= mkapp2.u2.
+Constraint Vec.u1 <= mkrel.u0.
+Constraint Vec.u1 <= mkapp.u0.
+Constraint Vec.u1 <= mkapp.u1.
+
 Fixpoint gen (n : nat) (a : Type) (f : nat -> a) {struct n} : Vec n a.
   refine (
       match n with
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
index 9b610324ff..b656f8a52c 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
@@ -8,6 +8,7 @@ From Coq Require Import Strings.String.
 From Coq Require Import Vectors.Vector.
 From Coq Require Import Bool.Bool.
 From Coq Require Import BinNums.
+From Coq Require Import ZifyClasses.
 
 From CryptolToCoq Require Import SAWCoreScaffolding.
 
@@ -24,6 +25,17 @@ Import VectorNotations.
 
 Definition Vec (n : nat) (a : Type) : Type := VectorDef.t a n.
 
+(* Work around https://github.com/coq/coq/issues/16803. Without this, using
+   `lia` on `bitvector` values will fail to typecheck on pre-8.17 versions of
+   Coq. Once our Coq support window shifts enough, we can drop this workaround.
+*)
+Constraint Vec.u1 <= mkapp2.u0.
+Constraint Vec.u1 <= mkapp2.u1.
+Constraint Vec.u1 <= mkapp2.u2.
+Constraint Vec.u1 <= mkrel.u0.
+Constraint Vec.u1 <= mkapp.u0.
+Constraint Vec.u1 <= mkapp.u1.
+
 Fixpoint gen (n : nat) (a : Type) (f : nat -> a) {struct n} : Vec n a.
   refine (
       match n with
@@ -103,35 +115,35 @@ Fixpoint atWithDefault (n : nat) (a : Type) (default : a) (v : Vec n a) (index :
   ).
 Defined.
 
-Definition map (a b : Type) (f : a -> b) (n : Nat) (xs : Vec n a) :=
+Definition map (a b : Type) (f : a -> b) (n : nat) (xs : Vec n a) :=
   VectorDef.map f xs.
 
-Fixpoint foldr (a b : Type) (n : Nat) (f : a -> b -> b) (base : b) (v : Vec n a) : b :=
+Fixpoint foldr (a b : Type) (n : nat) (f : a -> b -> b) (base : b) (v : Vec n a) : b :=
   match v with
   | Vector.nil => base
   | Vector.cons hd _ tl => f hd (foldr _ _ _ f base tl)
   end.
 
-Fixpoint foldl (a b : Type) (n : Nat) (f : b -> a -> b) (acc : b) (v : Vec n a) : b :=
+Fixpoint foldl (a b : Type) (n : nat) (f : b -> a -> b) (acc : b) (v : Vec n a) : b :=
   match v with
   | Vector.nil => acc
   | Vector.cons hd _ tl => foldl _ _ _ f (f acc hd) tl
   end.
 
-Fixpoint scanl (a b : Type) (n : Nat) (f : b -> a -> b) (acc : b) (v : Vec n a) : Vec (S n) b :=
+Fixpoint scanl (a b : Type) (n : nat) (f : b -> a -> b) (acc : b) (v : Vec n a) : Vec (S n) b :=
   match v in VectorDef.t _ n return Vec (S n) b with
   | Vector.nil => [ acc ]
   | Vector.cons h n' tl => Vector.cons b acc (S n') (scanl a b n' f (f acc h) tl)
   end.
 
-Fixpoint foldl_dep (a : Type) (b : Nat -> Type) (n : Nat)
+Fixpoint foldl_dep (a : Type) (b : nat -> Type) (n : nat)
          (f : forall n, b n -> a -> b (S n)) (base : b O) (v : Vec n a) : b n :=
   match v with
   | Vector.nil => base
   | Vector.cons hd _ tl => foldl_dep a (fun n => b (S n)) _ (fun n => f (S n)) (f _ base hd) tl
   end.
 
-Fixpoint tuple_foldl_dep (a : Type) (b : Nat -> Type) (n : Nat)
+Fixpoint tuple_foldl_dep (a : Type) (b : nat -> Type) (n : nat)
          (f : forall n, b n -> a -> b (S n)) (base : b O) (t : n .-tuple a) : b n :=
   match n, t with
   | O, _ => base
@@ -141,7 +153,7 @@ Fixpoint tuple_foldl_dep (a : Type) (b : Nat -> Type) (n : Nat)
 
 Definition EmptyVec := Vector.nil.
 
-Definition coerceVec (a : sort 0) (m n : Nat) (H : Eq Nat m n) (v : Vec m a) : Vec n a :=
+Definition coerceVec (a : sort 0) (m n : nat) (H : m = n) (v : Vec m a) : Vec n a :=
   match
     eq_sym H in eq _ n'
     return Vec n' a -> Vec n a
@@ -165,7 +177,7 @@ Qed.
 
 (* NOTE: This version of `zip` accepts two vectors of different size, unlike the
  * one in `CoqVectorsExtra.v` *)
-Fixpoint zipFunctional (a b : sort 0) (m n : Nat) (xs : Vec m a) (ys : Vec n b)
+Fixpoint zipFunctional (a b : sort 0) (m n : nat) (xs : Vec m a) (ys : Vec n b)
   : Vec (Nat.min m n) (a * b) :=
   match
     xs in Vector.t _ m'
@@ -184,10 +196,10 @@ Fixpoint zipFunctional (a b : sort 0) (m n : Nat) (xs : Vec m a) (ys : Vec n b)
 .
 
 Definition zipWithFunctional
-           (a b c : Type) (f : a -> b -> c) (n : Nat) (xs : Vec n a) (ys : Vec n b) :=
+           (a b c : Type) (f : a -> b -> c) (n : nat) (xs : Vec n a) (ys : Vec n b) :=
   VectorDef.map (fun p => f (fst p) (snd p)) (zipFunctional _ _ _ _ xs ys).
 
-Notation bitvector n := (Vec n Bool).
+Notation bitvector n := (Vec n bool).
 
 (* NOTE BITS are stored in reverse order than bitvector *)
 Definition bvToBITS {size : nat} : bitvector size -> BITS size
@@ -206,23 +218,23 @@ Definition joinLSB {n} (v : bitvector n) (lsb : bool) : bitvector n.+1 :=
 
 Definition bvToNatFolder (n : nat) (b : bool) := b + n.*2.
 
-Definition bvToNat (size : Nat) (v : bitvector size) : Nat :=
+Definition bvToNat (size : nat) (v : bitvector size) : nat :=
   Vector.fold_left bvToNatFolder 0 v.
 
 (* This is used to write literals of bitvector type, e.g. intToBv 64 3 *)
-Definition intToBv (n : Nat) (z : Z) : bitvector n := bitsToBv (fromZ z).
+Definition intToBv (n : nat) (z : Z) : bitvector n := bitsToBv (fromZ z).
 
 Arguments intToBv : simpl never.
 
 (* NOTE This can cause Coq to stack overflow, avoid it as much as possible! *)
-Definition bvNat (size : Nat) (number : Nat) : bitvector size :=
+Definition bvNat (size : nat) (number : nat) : bitvector size :=
   intToBv size (Z.of_nat number).
 
 Arguments bvNat /.
 
-Definition bvToInt (n : Nat) (b : bitvector n) : Z := toPosZ (bvToBITS b).
+Definition bvToInt (n : nat) (b : bitvector n) : Z := toPosZ (bvToBITS b).
 
-Definition sbvToInt (n : Nat) (b : bitvector n) : Z
+Definition sbvToInt (n : nat) (b : bitvector n) : Z
   := match n, b with
      | O, _ => 0
      | S n, b => toZ (bvToBITS b)
@@ -334,47 +346,47 @@ Definition shiftR (n : nat) (A : Type) (x : A) (v : Vector.t A n) (i : nat) : Ve
   iter i (shiftR1 n A x) v.
 
 (* This is annoying to implement, so using BITS conversion *)
-Definition bvult (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=
+Definition bvult (n : nat) (a : bitvector n) (b : bitvector n) : bool :=
   ltB (bvToBITS a) (bvToBITS b).
 Global Opaque bvult.
 
-Definition bvugt (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=
+Definition bvugt (n : nat) (a : bitvector n) (b : bitvector n) : bool :=
   bvult n b a.
 
 (* This is annoying to implement, so using BITS conversion *)
-Definition bvule (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=
+Definition bvule (n : nat) (a : bitvector n) (b : bitvector n) : bool :=
   leB (bvToBITS a) (bvToBITS b).
 Global Opaque bvule.
 
-Definition bvuge (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=
+Definition bvuge (n : nat) (a : bitvector n) (b : bitvector n) : bool :=
   bvule n b a.
 
-Definition sign {n : nat} (a : bitvector n) : Bool :=
+Definition sign {n : nat} (a : bitvector n) : bool :=
   match a with
   | Vector.nil => false
   | Vector.cons b _ _ => b
   end.
 
-Definition bvslt (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=
+Definition bvslt (n : nat) (a : bitvector n) (b : bitvector n) : bool :=
   let c := bvSub n a b
    in ((sign a && ~~ sign b) || (sign a && sign c) || (~~ sign b && sign c))%bool.
       (* ^ equivalent to: boolEq (bvSBorrow s a b) (sign (bvSub n a b))  *)
 Global Opaque bvslt.
 
-Definition bvsgt (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=
+Definition bvsgt (n : nat) (a : bitvector n) (b : bitvector n) : bool :=
   bvslt n b a.
 
-Definition bvsle (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=
+Definition bvsle (n : nat) (a : bitvector n) (b : bitvector n) : bool :=
   (bvslt n a b || (Vector.eqb _ eqb a b))%bool.
 Global Opaque bvsle.
 
-Definition bvsge (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=
+Definition bvsge (n : nat) (a : bitvector n) (b : bitvector n) : bool :=
   bvsle n b a.
 
-Definition bvAddOverflow n (a : bitvector n) (b : bitvector n) : Bool :=
+Definition bvAddOverflow n (a : bitvector n) (b : bitvector n) : bool :=
   let c := bvAdd n a b
    in ((sign a && sign b && ~~ sign c) || (~~ sign a && ~~ sign b && sign c))%bool.
 
-Definition bvSubOverflow n (a : bitvector n) (b : bitvector n) : Bool :=
+Definition bvSubOverflow n (a : bitvector n) (b : bitvector n) : bool :=
   let c := bvSub n a b
    in ((sign a && ~~ sign b && ~~ sign c) || (~~ sign a && sign b && sign c))%bool.
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
index 1bae02a363..6c22eac36d 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
@@ -151,8 +151,7 @@ rename ident = IdentSpecialTreatment
   }
 
 -- | Replace any occurrences of identifier applied to @n@ arguments with the
--- supplied Coq term. If @n=0@ and the supplied Coq term is an identifier then
--- this is the same as 'rename'.
+-- supplied Coq term
 replaceDropArgs :: Int -> Coq.Term -> IdentSpecialTreatment
 replaceDropArgs n term = IdentSpecialTreatment
   { atDefSite = DefSkip
@@ -173,9 +172,32 @@ skip = IdentSpecialTreatment
   , atUseSite = UsePreserve
   }
 
+-- | The Coq built-in @Datatypes@ module
+datatypesModule :: ModuleName
+datatypesModule =
+  -- NOTE: SAW core convention is most specific module name component first, so
+  -- this is really Coq.Init.Datatypes
+  mkModuleName ["Datatypes", "Init", "Coq"]
+
+-- | The Coq built-in @Logic@ module
+logicModule :: ModuleName
+logicModule =
+  -- NOTE: SAW core convention is most specific module name component first, so
+  -- this is really Coq.Init.Logic
+  mkModuleName ["Logic", "Init", "Coq"]
+
+-- | The Coq built-in @String@ module.
+stringModule :: ModuleName
+stringModule =
+  -- NOTE: SAW core convention is most specific module name component first, so
+  -- this is really Coq.Strings.String
+  mkModuleName ["String", "Strings", "Coq"]
+
+-- | The @SAWCoreScaffolding@ module
 sawDefinitionsModule :: ModuleName
 sawDefinitionsModule = mkModuleName ["SAWCoreScaffolding"]
 
+-- | The @CompM@ module
 compMModule :: ModuleName
 compMModule = mkModuleName ["CompM"]
 
@@ -278,25 +300,25 @@ sawCorePreludeSpecialTreatmentMap configuration =
 
   -- Boolean
   ++
-  [ ("and",           mapsTo sawDefinitionsModule "and")
+  [ ("Bool",          mapsTo datatypesModule "bool")
+  , ("True",          mapsTo datatypesModule "true")
+  , ("False",         mapsTo datatypesModule "false")
+  , ("and",           mapsTo datatypesModule "andb")
   , ("and__eq",       mapsTo sawDefinitionsModule "and__eq")
-  , ("Bool",          mapsTo sawDefinitionsModule "Bool")
+  , ("or",            mapsTo datatypesModule "orb")
+  , ("or__eq",        mapsTo sawDefinitionsModule "or__eq")
+  , ("xor",           mapsTo datatypesModule "xorb")
+  , ("xor__eq",       mapsTo sawDefinitionsModule "xor__eq")
+  , ("not",           mapsTo datatypesModule "negb")
+  , ("not__eq",       mapsTo sawDefinitionsModule "not__eq")
   , ("boolEq",        mapsTo sawDefinitionsModule "boolEq")
   , ("boolEq__eq",    mapsTo sawDefinitionsModule "boolEq__eq")
-  , ("False",         mapsTo sawDefinitionsModule "false")
   , ("ite",           mapsTo sawDefinitionsModule "ite")
   , ("iteDep",        mapsTo sawDefinitionsModule "iteDep")
   , ("iteDep_True",   mapsTo sawDefinitionsModule "iteDep_True")
   , ("iteDep_False",  mapsTo sawDefinitionsModule "iteDep_False")
   , ("ite_bit",       skip) -- FIXME: change this
   , ("ite_eq_iteDep", mapsTo sawDefinitionsModule "ite_eq_iteDep")
-  , ("not",           mapsTo sawDefinitionsModule "not")
-  , ("not__eq",       mapsTo sawDefinitionsModule "not__eq")
-  , ("or",            mapsTo sawDefinitionsModule "or")
-  , ("or__eq",        mapsTo sawDefinitionsModule "or__eq")
-  , ("True",          mapsTo sawDefinitionsModule "true")
-  , ("xor",           mapsTo sawDefinitionsModule "xor")
-  , ("xor__eq",       mapsTo sawDefinitionsModule "xor__eq")
   ]
 
   -- Pairs
@@ -310,9 +332,9 @@ sawCorePreludeSpecialTreatmentMap configuration =
 
   -- Equality
   ++
-  [ ("Eq",      mapsTo sawDefinitionsModule "Eq")
+  [ ("Eq",      mapsToExpl logicModule "eq")
   , ("Eq__rec", mapsTo sawDefinitionsModule "Eq__rec")
-  , ("Refl",    mapsTo sawDefinitionsModule "Refl")
+  , ("Refl",    mapsToExpl logicModule "eq_refl")
   ]
 
   -- Nat le
@@ -325,20 +347,20 @@ sawCorePreludeSpecialTreatmentMap configuration =
 
   -- Strings
   ++
-  [ ("String", mapsTo sawDefinitionsModule "String")
+  [ ("String", mapsTo stringModule "string")
   , ("equalString", mapsTo sawDefinitionsModule "equalString")
   , ("appendString", mapsTo sawDefinitionsModule "appendString")
   ]
 
   -- Utility functions
   ++
-  [ ("id", mapsTo sawDefinitionsModule "id")
+  [ ("id", mapsTo datatypesModule "id")
   ]
 
   -- Natural numbers
   ++
   [ ("divModNat", mapsTo sawDefinitionsModule "divModNat")
-  , ("Nat",       mapsTo sawDefinitionsModule "Nat")
+  , ("Nat",       mapsTo datatypesModule "nat")
   , ("widthNat",  mapsTo sawDefinitionsModule "widthNat")
   , ("Zero",      mapsTo sawCoreScaffoldingModule   "Zero")
   , ("Succ",      mapsTo sawCoreScaffoldingModule   "Succ")
@@ -565,7 +587,7 @@ escapeIdent str
 
 zipSnippet :: String
 zipSnippet = [i|
-Fixpoint zip (a b : sort 0) (m n : Nat) (xs : Vec m a) (ys : Vec n b)
+Fixpoint zip (a b : sort 0) (m n : nat) (xs : Vec m a) (ys : Vec n b)
   : Vec (minNat m n) (a * b) :=
   match
     xs in Vector.t _ m'
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
index aacaca2232..bba983d1e5 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
@@ -280,9 +280,9 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
     PairValue x y -> Coq.App (Coq.Var "pair") <$> traverse translateTerm [x, y]
     PairType x y  -> Coq.App (Coq.Var "prod") <$> traverse translateTerm [x, y]
     PairLeft t    ->
-      Coq.App <$> pure (Coq.Var "SAWCoreScaffolding.fst") <*> traverse translateTerm [t]
+      Coq.App <$> pure (Coq.Var "fst") <*> traverse translateTerm [t]
     PairRight t   ->
-      Coq.App <$> pure (Coq.Var "SAWCoreScaffolding.snd") <*> traverse translateTerm [t]
+      Coq.App <$> pure (Coq.Var "snd") <*> traverse translateTerm [t]
     -- TODO: maybe have more customizable translation of data types
     DataTypeApp n is as -> translateIdentWithArgs (primName n) (is ++ as)
     CtorApp n is as -> translateIdentWithArgs (primName n) (is ++ as)