diff --git a/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v b/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
index cf2950a91f..28b94c7cd2 100644
--- a/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
+++ b/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
@@ -583,8 +583,11 @@ Definition ecRotR : forall (m : @Num), forall (ix : Type), forall (a : Type), @P
 Definition ecCat : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq m a -> @seq n a -> @seq (@tcAdd m n) a :=
   @finNumRec (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq m a -> @seq n a -> @seq (@tcAdd m n) a) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m a -> @seq n a -> @seq (@tcAdd (@TCNum m) n) a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) => @SAWCorePrelude.append m n a) (fun (a : Type) => @SAWCorePrelude.streamAppend a m)).
 
-Definition ecSplitAt : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> prod (@seq m a) (@seq n a) :=
-  @finNumRec (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> prod (@seq m a) (@seq n a)) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCNum m) n) a -> prod (@SAWCoreVectorsAsCoqVectors.Vec m a) (@seq n a)) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCorePrelude.addNat m n) a) => pair (@SAWCorePrelude.take a m n xs) (@SAWCorePrelude.drop a m n xs)) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => pair (@SAWCorePrelude.streamTake a m xs) (@SAWCorePrelude.streamDrop a m xs))).
+Definition ecTake : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq m a :=
+  @CryptolPrimitivesForSAWCore.Num_rect (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq m a) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCNum m) n) a -> @SAWCoreVectorsAsCoqVectors.Vec m a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCorePrelude.addNat m n) a) => @SAWCorePrelude.take a m n xs) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => @SAWCorePrelude.streamTake a m xs)) (@CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCInf) n) a -> @SAWCorePrelude.Stream a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCorePrelude.Stream a) => xs) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => xs)).
+
+Definition ecDrop : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq n a :=
+  @finNumRec (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq n a) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCNum m) n) a -> @seq n a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCorePrelude.addNat m n) a) => @SAWCorePrelude.drop a m n xs) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => @SAWCorePrelude.streamDrop a m xs)).
 
 Definition ecJoin : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq m (@seq n a) -> @seq (@tcMul m n) a :=
   fun (m : @Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : @Num) => forall (n : @Num), forall (a : Type), @seq m1 (@seq n a) -> @seq (@tcMul m1 n) a) (fun (m1 : @SAWCoreScaffolding.Nat) => @finNumRec (fun (n : @Num) => forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m1 (@seq n a) -> @seq (@tcMul (@TCNum m1) n) a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) => @SAWCorePrelude.join m1 n a)) (@finNumRec (fun (n : @Num) => forall (a : Type), @SAWCorePrelude.Stream (@seq n a) -> @seq (@tcMul (@TCInf) n) a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) => @SAWCorePrelude.natCase (fun (n' : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.Stream (@SAWCoreVectorsAsCoqVectors.Vec n' a) -> @seq (@SAWCorePrelude.if0Nat (@Num) n' (@TCNum 0) (@TCInf)) a) (fun (s : @SAWCorePrelude.Stream (@SAWCoreVectorsAsCoqVectors.Vec 0 a)) => @SAWCoreVectorsAsCoqVectors.EmptyVec a) (fun (n' : @SAWCoreScaffolding.Nat) (s : @SAWCorePrelude.Stream (@SAWCoreVectorsAsCoqVectors.Vec (@SAWCoreScaffolding.Succ n') a)) => @SAWCorePrelude.streamJoin a n' s) n)) m.
diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
index c088de3a04..428d2342ba 100644
--- a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
+++ b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
@@ -182,8 +182,7 @@ Definition not_True : @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCor
 Definition not_False : @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) :=
   @trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (if @SAWCoreScaffolding.false then @SAWCoreScaffolding.false else @SAWCoreScaffolding.true) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.not__eq (@SAWCoreScaffolding.false)) (@ite_false (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.true)).
 
-Definition not_not : forall (x : @SAWCoreScaffolding.Bool), let var__0   := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in
-  @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.not x)) x :=
+Definition not_not : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.not x)) x :=
   fun (x : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.not b)) b) x (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true))) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.false) not_True (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not)) not_False) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false))) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.false) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) not_False (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not)) not_True).
 
 Definition and_True1 : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.true) x) x :=
@@ -198,8 +197,7 @@ Definition and_True2 : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffoldin
 Definition and_False2 : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.false) :=
   fun (x : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and b (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.false)) x (@and_True1 (@SAWCoreScaffolding.false)) (@and_False1 (@SAWCoreScaffolding.false)).
 
-Definition and_assoc : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), forall (z : @SAWCoreScaffolding.Bool), let var__0   := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in
-  @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.and y z)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.and x y) z) :=
+Definition and_assoc : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), forall (z : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.and y z)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.and x y) z) :=
   fun (x : @SAWCoreScaffolding.Bool) (y : @SAWCoreScaffolding.Bool) (z : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.and y b)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.and x y) b)) z (@trans2 (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.and y (@SAWCoreScaffolding.true))) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.and x y) (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.and x y) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and y (@SAWCoreScaffolding.true)) y (@and_True2 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x)) (@and_True2 (@SAWCoreScaffolding.and x y))) (@trans2 (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.and y (@SAWCoreScaffolding.false))) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.and x y) (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.false) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.and y (@SAWCoreScaffolding.false))) (@SAWCoreScaffolding.and x (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.false) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and y (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.false) (@and_False2 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x)) (@and_False2 x)) (@and_False2 (@SAWCoreScaffolding.and x y))).
 
 Definition and_idem : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and x x) x :=
@@ -217,8 +215,7 @@ Definition or_True2 : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding
 Definition or_False2 : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.false)) x :=
   fun (x : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or b (@SAWCoreScaffolding.false)) b) x (@or_True1 (@SAWCoreScaffolding.false)) (@or_False1 (@SAWCoreScaffolding.false)).
 
-Definition or_assoc : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), forall (z : @SAWCoreScaffolding.Bool), let var__0   := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in
-  @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.or y z)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.or x y) z) :=
+Definition or_assoc : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), forall (z : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.or y z)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.or x y) z) :=
   fun (x : @SAWCoreScaffolding.Bool) (y : @SAWCoreScaffolding.Bool) (z : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.or y b)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.or x y) b)) z (@trans2 (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.or y (@SAWCoreScaffolding.true))) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.or x y) (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.true) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.or y (@SAWCoreScaffolding.true))) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.true) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or y (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.true) (@or_True2 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x)) (@or_True2 x)) (@or_True2 (@SAWCoreScaffolding.or x y))) (@trans2 (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x (@SAWCoreScaffolding.or y (@SAWCoreScaffolding.false))) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.or x y) (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.or x y) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or y (@SAWCoreScaffolding.false)) y (@or_False2 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x)) (@or_False2 (@SAWCoreScaffolding.or x y))).
 
 Definition or_idem : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or x x) x :=
@@ -263,26 +260,19 @@ Definition boolEq_False2 : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffo
 Definition boolEq_same : forall (x : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.boolEq x x) (@SAWCoreScaffolding.true) :=
   fun (x : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.boolEq b b) (@SAWCoreScaffolding.true)) x (@boolEq_True1 (@SAWCoreScaffolding.true)) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.boolEq (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) (@boolEq_False1 (@SAWCoreScaffolding.false)) not_False).
 
-Definition not_or : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), let var__0   := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in
-  let var__1   := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in
-  @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.or x y)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not x) (@SAWCoreScaffolding.not y)) :=
+Definition not_or : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.or x y)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not x) (@SAWCoreScaffolding.not y)) :=
   fun (x : @SAWCoreScaffolding.Bool) (y : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.or b y)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not b) (@SAWCoreScaffolding.not y))) x (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.or (@SAWCoreScaffolding.true) y)) (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.not y)) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.or (@SAWCoreScaffolding.true) y)) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.false) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.true) y) (@SAWCoreScaffolding.true) (@or_True1 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not)) not_True) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.not y)) (@sym (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.false) (@and_False1 (@SAWCoreScaffolding.not y))) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@sym (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.false) not_True) (@SAWCoreScaffolding.Bool) (fun (z : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.and z (@SAWCoreScaffolding.not y))))) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.or (@SAWCoreScaffolding.false) y)) (@SAWCoreScaffolding.not y) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.not y)) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.false) y) y (@or_False1 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not)) (@sym (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.not y) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.not y) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) not_False (@SAWCoreScaffolding.Bool) (fun (z : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.and z (@SAWCoreScaffolding.not y))) (@and_True1 (@SAWCoreScaffolding.not y))))).
 
-Definition not_and : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), let var__0   := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in
-  let var__1   := @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool -> @SAWCoreScaffolding.Bool in
-  @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.and x y)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not x) (@SAWCoreScaffolding.not y)) :=
+Definition not_and : forall (x : @SAWCoreScaffolding.Bool), forall (y : @SAWCoreScaffolding.Bool), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.and x y)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not x) (@SAWCoreScaffolding.not y)) :=
   fun (x : @SAWCoreScaffolding.Bool) (y : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.and b y)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not b) (@SAWCoreScaffolding.not y))) x (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.and (@SAWCoreScaffolding.true) y)) (@SAWCoreScaffolding.not y) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.not y)) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.true) y) y (@and_True1 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not)) (@sym (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.not y) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.not y) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.false) not_True (@SAWCoreScaffolding.Bool) (fun (z : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.or z (@SAWCoreScaffolding.not y))) (@or_False1 (@SAWCoreScaffolding.not y))))) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.and (@SAWCoreScaffolding.false) y)) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.not y)) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.and (@SAWCoreScaffolding.false) y)) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.and (@SAWCoreScaffolding.false) y) (@SAWCoreScaffolding.false) (@and_False1 y) (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not)) not_False) (@trans (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.not y)) (@sym (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.or (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.not y)) (@SAWCoreScaffolding.true) (@or_True1 (@SAWCoreScaffolding.not y))) (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@sym (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) not_False) (@SAWCoreScaffolding.Bool) (fun (z : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.or z (@SAWCoreScaffolding.not y))))).
 
-Definition ite_not : forall (a : Type), forall (b : @SAWCoreScaffolding.Bool), forall (x : a), forall (y : a), let var__0   := forall (a1 : Type), @SAWCoreScaffolding.Bool -> a1 -> a1 -> a1 in
-  @SAWCoreScaffolding.Eq a (if @SAWCoreScaffolding.not b then x else y) (if b then y else x) :=
+Definition ite_not : forall (a : Type), forall (b : @SAWCoreScaffolding.Bool), forall (x : a), forall (y : a), @SAWCoreScaffolding.Eq a (if @SAWCoreScaffolding.not b then x else y) (if b then y else x) :=
   fun (a : Type) (b : @SAWCoreScaffolding.Bool) (x : a) (y : a) => @SAWCoreScaffolding.iteDep (fun (b' : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq a (if @SAWCoreScaffolding.not b' then x else y) (if b' then y else x)) b (@trans a (if @SAWCoreScaffolding.not (@SAWCoreScaffolding.true) then x else y) y (if @SAWCoreScaffolding.true then y else x) (@trans a (if @SAWCoreScaffolding.not (@SAWCoreScaffolding.true) then x else y) (if @SAWCoreScaffolding.false then x else y) y (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.false) not_True a (fun (z : @SAWCoreScaffolding.Bool) => if z then x else y)) (@ite_false a x y)) (@sym a (if @SAWCoreScaffolding.true then y else x) y (@ite_true a y x))) (@trans a (if @SAWCoreScaffolding.not (@SAWCoreScaffolding.false) then x else y) x (if @SAWCoreScaffolding.false then y else x) (@trans a (if @SAWCoreScaffolding.not (@SAWCoreScaffolding.false) then x else y) (if @SAWCoreScaffolding.true then x else y) x (@eq_cong (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.not (@SAWCoreScaffolding.false)) (@SAWCoreScaffolding.true) not_False a (fun (z : @SAWCoreScaffolding.Bool) => if z then x else y)) (@ite_true a x y)) (@sym a (if @SAWCoreScaffolding.false then y else x) x (@ite_false a y x))).
 
-Definition ite_nest1 : forall (a : Type), forall (b : @SAWCoreScaffolding.Bool), forall (x : a), forall (y : a), forall (z : a), let var__0   := forall (a1 : Type), @SAWCoreScaffolding.Bool -> a1 -> a1 -> a1 in
-  @SAWCoreScaffolding.Eq a (if b then if b then x else y else z) (if b then x else z) :=
+Definition ite_nest1 : forall (a : Type), forall (b : @SAWCoreScaffolding.Bool), forall (x : a), forall (y : a), forall (z : a), @SAWCoreScaffolding.Eq a (if b then if b then x else y else z) (if b then x else z) :=
   fun (a : Type) (b : @SAWCoreScaffolding.Bool) (x : a) (y : a) (z : a) => @SAWCoreScaffolding.iteDep (fun (b' : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq a (if b' then if b' then x else y else z) (if b' then x else z)) b (@trans a (if @SAWCoreScaffolding.true then if @SAWCoreScaffolding.true then x else y else z) x (if @SAWCoreScaffolding.true then x else z) (@trans a (if @SAWCoreScaffolding.true then if @SAWCoreScaffolding.true then x else y else z) (if @SAWCoreScaffolding.true then x else y) x (@ite_true a (if @SAWCoreScaffolding.true then x else y) z) (@ite_true a x y)) (@sym a (if @SAWCoreScaffolding.true then x else z) x (@ite_true a x z))) (@trans a (if @SAWCoreScaffolding.false then if @SAWCoreScaffolding.false then x else y else z) z (if @SAWCoreScaffolding.false then x else z) (@ite_false a (if @SAWCoreScaffolding.false then x else y) z) (@sym a (if @SAWCoreScaffolding.false then x else z) z (@ite_false a x z))).
 
-Definition ite_nest2 : forall (a : Type), forall (b : @SAWCoreScaffolding.Bool), forall (x : a), forall (y : a), forall (z : a), let var__0   := forall (a1 : Type), @SAWCoreScaffolding.Bool -> a1 -> a1 -> a1 in
-  @SAWCoreScaffolding.Eq a (if b then x else if b then y else z) (if b then x else z) :=
+Definition ite_nest2 : forall (a : Type), forall (b : @SAWCoreScaffolding.Bool), forall (x : a), forall (y : a), forall (z : a), @SAWCoreScaffolding.Eq a (if b then x else if b then y else z) (if b then x else z) :=
   fun (a : Type) (b : @SAWCoreScaffolding.Bool) (x : a) (y : a) (z : a) => @SAWCoreScaffolding.iteDep (fun (b' : @SAWCoreScaffolding.Bool) => @SAWCoreScaffolding.Eq a (if b' then x else if b' then y else z) (if b' then x else z)) b (@trans a (if @SAWCoreScaffolding.true then x else if @SAWCoreScaffolding.true then y else z) x (if @SAWCoreScaffolding.true then x else z) (@ite_true a x (if @SAWCoreScaffolding.true then y else z)) (@sym a (if @SAWCoreScaffolding.true then x else z) x (@ite_true a x z))) (@trans a (if @SAWCoreScaffolding.false then x else if @SAWCoreScaffolding.false then y else z) z (if @SAWCoreScaffolding.false then x else z) (@trans a (if @SAWCoreScaffolding.false then x else if @SAWCoreScaffolding.false then y else z) (if @SAWCoreScaffolding.false then y else z) z (@ite_false a x (if @SAWCoreScaffolding.false then y else z)) (@ite_false a y z)) (@sym a (if @SAWCoreScaffolding.false then x else z) z (@ite_false a x z))).
 
 (* Prelude.ite_bit was skipped *)
@@ -510,8 +500,7 @@ Fixpoint zip (a b : sort 0) (m n : Nat) (xs : Vec m a) (ys : Vec n b)
 Definition reverse : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec n a -> @SAWCoreVectorsAsCoqVectors.Vec n a :=
   fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec n a) => @SAWCoreVectorsAsCoqVectors.gen n a (fun (i : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.sawAt n a xs (@subNat (@subNat n 1) i)).
 
-Definition transpose : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) -> let var__0   := @SAWCoreScaffolding.Nat -> Type -> Type in
-  @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreVectorsAsCoqVectors.Vec m a) :=
+Definition transpose : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) -> @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreVectorsAsCoqVectors.Vec m a) :=
   fun (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (a : Type) (xss : @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a)) => @SAWCoreVectorsAsCoqVectors.gen n (@SAWCoreVectorsAsCoqVectors.Vec m a) (fun (j : @SAWCoreScaffolding.Nat) => @SAWCoreVectorsAsCoqVectors.gen m a (fun (i : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.sawAt n a (@SAWCorePrelude.sawAt m (@SAWCoreVectorsAsCoqVectors.Vec n a) xss i) j)).
 
 Definition vecEq : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), (a -> a -> @SAWCoreScaffolding.Bool) -> @SAWCoreVectorsAsCoqVectors.Vec n a -> @SAWCoreVectorsAsCoqVectors.Vec n a -> @SAWCoreScaffolding.Bool :=
@@ -520,8 +509,7 @@ Definition vecEq : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), (a -
 Definition take : forall (a : Type), forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), @SAWCoreVectorsAsCoqVectors.Vec (@addNat m n) a -> @SAWCoreVectorsAsCoqVectors.Vec m a :=
   fun (a : Type) (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (v : @SAWCoreVectorsAsCoqVectors.Vec (@addNat m n) a) => @SAWCoreVectorsAsCoqVectors.gen m a (fun (i : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.sawAt (@addNat m n) a v i).
 
-Definition vecCong : forall (a : Type), forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Nat) m n -> let var__0   := @SAWCoreScaffolding.Nat -> Type -> Type in
-  @SAWCoreScaffolding.Eq Type (@SAWCoreVectorsAsCoqVectors.Vec m a) (@SAWCoreVectorsAsCoqVectors.Vec n a) :=
+Definition vecCong : forall (a : Type), forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Nat) m n -> @SAWCoreScaffolding.Eq Type (@SAWCoreVectorsAsCoqVectors.Vec m a) (@SAWCoreVectorsAsCoqVectors.Vec n a) :=
   fun (a : Type) (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (eq : @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Nat) m n) => @eq_cong (@SAWCoreScaffolding.Nat) m n eq Type (fun (i : @SAWCoreScaffolding.Nat) => @SAWCoreVectorsAsCoqVectors.Vec i a).
 
 (* Prelude.coerceVec was skipped *)
@@ -539,8 +527,7 @@ Definition slice : forall (a : Type), forall (m : @SAWCoreScaffolding.Nat), fora
 Definition join : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) -> @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a :=
   fun (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (a : Type) (v : @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a)) => @SAWCoreVectorsAsCoqVectors.gen (@mulNat m n) a (fun (i : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.sawAt n a (@SAWCorePrelude.sawAt m (@SAWCoreVectorsAsCoqVectors.Vec n a) v (@divNat i n)) (@modNat i n)).
 
-Definition split : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a -> let var__0   := @SAWCoreScaffolding.Nat -> Type -> Type in
-  @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) :=
+Definition split : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a -> @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) :=
   fun (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (a : Type) (v : @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a) => @SAWCoreVectorsAsCoqVectors.gen m (@SAWCoreVectorsAsCoqVectors.Vec n a) (fun (i : @SAWCoreScaffolding.Nat) => @SAWCoreVectorsAsCoqVectors.gen n a (fun (j : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.sawAt (@mulNat m n) a v (@addNat (@mulNat i n) j))).
 
 Definition append : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m a -> @SAWCoreVectorsAsCoqVectors.Vec n a -> @SAWCoreVectorsAsCoqVectors.Vec (@addNat m n) a :=
@@ -557,8 +544,7 @@ Definition append : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreSc
 Definition joinLittleEndian : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) -> @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a :=
   fun (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (a : Type) (v : @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a)) => @join m n a (@reverse m (@SAWCoreVectorsAsCoqVectors.Vec n a) v).
 
-Definition splitLittleEndian : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a -> let var__0   := @SAWCoreScaffolding.Nat -> Type -> Type in
-  @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) :=
+Definition splitLittleEndian : forall (m : @SAWCoreScaffolding.Nat), forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a -> @SAWCoreVectorsAsCoqVectors.Vec m (@SAWCoreVectorsAsCoqVectors.Vec n a) :=
   fun (m : @SAWCoreScaffolding.Nat) (n : @SAWCoreScaffolding.Nat) (a : Type) (v : @SAWCoreVectorsAsCoqVectors.Vec (@mulNat m n) a) => @reverse m (@SAWCoreVectorsAsCoqVectors.Vec n a) (@split m n a v).
 
 Definition msb : forall (n : @SAWCoreScaffolding.Nat), @SAWCoreVectorsAsCoqVectors.Vec (@SAWCoreScaffolding.Succ n) (@SAWCoreScaffolding.Bool) -> @SAWCoreScaffolding.Bool :=
@@ -874,11 +860,9 @@ Definition bvultWithProof : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @
 Definition bvuleWithProof : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @Maybe (@SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvule n v1 v2) (@SAWCoreScaffolding.true)) :=
   fun (n : @SAWCoreScaffolding.Nat) (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) => @SAWCoreScaffolding.iteDep (fun (b : @SAWCoreScaffolding.Bool) => @Maybe (@SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) b (@SAWCoreScaffolding.true))) (@SAWCoreVectorsAsCoqVectors.bvule n v1 v2) (@Just (@SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.true)) (@SAWCoreScaffolding.Refl (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true))) (@Nothing (@SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.false) (@SAWCoreScaffolding.true))).
 
-Axiom bvEqToEqNat : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @SAWCoreScaffolding.Eq (@SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) v1 v2 -> let var__0   := forall (n1 : @SAWCoreScaffolding.Nat), @SAWCoreVectorsAsCoqVectors.Vec n1 (@SAWCoreScaffolding.Bool) -> @SAWCoreScaffolding.Nat in
-  @eqNat (@SAWCoreVectorsAsCoqVectors.bvToNat n v1) (@SAWCoreVectorsAsCoqVectors.bvToNat n v2) .
+Axiom bvEqToEqNat : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @SAWCoreScaffolding.Eq (@SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) v1 v2 -> @eqNat (@SAWCoreVectorsAsCoqVectors.bvToNat n v1) (@SAWCoreVectorsAsCoqVectors.bvToNat n v2) .
 
-Axiom bvultToIsLtNat : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n v1 v2) (@SAWCoreScaffolding.true) -> let var__0   := forall (n1 : @SAWCoreScaffolding.Nat), @SAWCoreVectorsAsCoqVectors.Vec n1 (@SAWCoreScaffolding.Bool) -> @SAWCoreScaffolding.Nat in
-  @IsLtNat (@SAWCoreVectorsAsCoqVectors.bvToNat n v1) (@SAWCoreVectorsAsCoqVectors.bvToNat n v2) .
+Axiom bvultToIsLtNat : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n v1 v2) (@SAWCoreScaffolding.true) -> @IsLtNat (@SAWCoreVectorsAsCoqVectors.bvToNat n v1) (@SAWCoreVectorsAsCoqVectors.bvToNat n v2) .
 
 Axiom genWithProof : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), (forall (i : @SAWCoreScaffolding.Nat), @IsLtNat i n -> a) -> @SAWCoreVectorsAsCoqVectors.Vec n a .
 
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs
index e14bcefbe3..34dfc2d7b6 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs
@@ -113,7 +113,11 @@ Import ListNotations.
 translateTermAsDeclImports ::
   TranslationConfiguration -> Coq.Ident -> Term -> Either (TranslationError Term) (Doc ann)
 translateTermAsDeclImports configuration name t = do
-  doc <- TermTranslation.translateDefDoc configuration Nothing [] name t
+  doc <-
+    TermTranslation.translateDefDoc
+      configuration
+      (TermTranslation.TranslationReader Nothing)
+      [] name t
   return $ vcat [preamble configuration, hardline <> doc]
 
 translateSAWModule :: TranslationConfiguration -> Module -> Doc ann
@@ -131,7 +135,11 @@ translateSAWModule configuration m =
      ]
 
 translateCryptolModule ::
-  TranslationConfiguration -> [String] -> CryptolModule -> Either (TranslationError Term) (Doc ann)
+  TranslationConfiguration ->
+  -- | List of already translated global declarations
+  [String] ->
+  CryptolModule ->
+  Either (TranslationError Term) (Doc ann)
 translateCryptolModule configuration globalDecls m =
   let decls = CryptolModuleTranslation.translateCryptolModule
               configuration
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs
index 8f47a8c931..4ce29b872b 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs
@@ -8,10 +8,10 @@ import           Control.Monad                      (forM)
 import           Control.Monad.State                (modify)
 import qualified Data.Map                           as Map
 
-import           Cryptol.ModuleSystem.Name
-import           Cryptol.Utils.Ident
+import           Cryptol.ModuleSystem.Name          (Name, nameIdent)
+import           Cryptol.Utils.Ident                (unpackIdent)
 import qualified Language.Coq.AST                   as Coq
-import           Verifier.SAW.Term.Functor
+import           Verifier.SAW.Term.Functor          (Term)
 import           Verifier.SAW.Translation.Coq.Monad
 import qualified Verifier.SAW.Translation.Coq.Term  as TermTranslation
 import           Verifier.SAW.TypedTerm
@@ -23,21 +23,28 @@ translateTypedTermMap tm = forM (Map.assocs tm) translateAndRegisterEntry
     translateAndRegisterEntry (name, symbol) = do
       let t = ttTerm symbol
       let nameStr = unpackIdent (nameIdent name)
-      term <- TermTranslation.withLocalLocalEnvironment $ do
+      term <- TermTranslation.withLocalTranslationState $ do
         modify $ set TermTranslation.localEnvironment [nameStr]
         TermTranslation.translateTerm t
       let decl = TermTranslation.mkDefinition nameStr term
       modify $ over TermTranslation.globalDeclarations (nameStr :)
       return decl
 
+-- | Translates a Cryptol Module into a list of Coq declarations.  This is done
+-- by going through the term map corresponding to the module, translating all
+-- terms, and accumulating the translated declarations of all top-level
+-- declarations encountered.
 translateCryptolModule ::
-  TranslationConfiguration -> [String] -> CryptolModule -> Either (TranslationError Term) [Coq.Decl]
+  TranslationConfiguration ->
+  -- | List of already translated global declarations
+  [String] ->
+  CryptolModule ->
+  Either (TranslationError Term) [Coq.Decl]
 translateCryptolModule configuration globalDecls (CryptolModule _ tm) =
-  case TermTranslation.runTermTranslationMonad
-       configuration
-       Nothing
-       globalDecls
-       []
-       (translateTypedTermMap tm) of
-  Left e -> Left e
-  Right (_, st) -> Right (reverse (view TermTranslation.localDeclarations st))
+  reverse . view TermTranslation.topLevelDeclarations . snd
+  <$> TermTranslation.runTermTranslationMonad
+      configuration
+      (TermTranslation.TranslationReader Nothing) -- TODO: this should be Just no?
+      globalDecls
+      []
+      (translateTypedTermMap tm)
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs
index f2a441a037..21d69675f4 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs
@@ -17,6 +17,7 @@ module Verifier.SAW.Translation.Coq.Monad
   , TranslationConfigurationMonad
   , TranslationMonad
   , TranslationError(..)
+  , WithTranslationConfiguration(..)
   , runTranslationMonad
   ) where
 
@@ -77,19 +78,32 @@ data TranslationConfiguration = TranslationConfiguration
   -- - SAWCoreVectorsAsSSReflectSeqs
   }
 
-type TranslationConfigurationMonad m =
-  ( MonadReader TranslationConfiguration m
+-- | The functional dependency of 'MonadReader' makes it not compositional, so
+-- we have to jam together different structures that want to be in the 'Reader'
+-- into a single datatype.  This type allows adding extra configuration on top
+-- of the translation configuration.
+data WithTranslationConfiguration r = WithTranslationConfiguration
+  { translationConfiguration :: TranslationConfiguration
+  , otherConfiguration :: r
+  }
+
+-- | Some computations will rely solely on access to the configuration, so we
+-- provide it separately.
+type TranslationConfigurationMonad r m =
+  ( MonadReader (WithTranslationConfiguration r) m
   )
 
-type TranslationMonad s m =
+type TranslationMonad r s m =
   ( Except.MonadError (TranslationError Term)  m
-  , TranslationConfigurationMonad m
+  , TranslationConfigurationMonad r m
   , MonadState s m
   )
 
 runTranslationMonad ::
   TranslationConfiguration ->
+  r ->
   s ->
-  (forall m. TranslationMonad s m => m a) ->
+  (forall m. TranslationMonad r s m => m a) ->
   Either (TranslationError Term) (a, s)
-runTranslationMonad configuration state m = runStateT (runReaderT m configuration) state
+runTranslationMonad configuration r s m =
+  runStateT (runReaderT m (WithTranslationConfiguration configuration r)) s
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs
index 23dfb81774..67ba2b0d40 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs
@@ -24,10 +24,8 @@ Portability : portable
 
 module Verifier.SAW.Translation.Coq.SAWModule where
 
-import           Control.Lens                                  (makeLenses, view)
 import qualified Control.Monad.Except                          as Except
 import           Control.Monad.Reader                          hiding (fail)
-import           Control.Monad.State                           hiding (fail)
 import           Prelude                                       hiding (fail)
 import           Prettyprinter                                 (Doc)
 
@@ -36,26 +34,22 @@ import qualified Language.Coq.Pretty                           as Coq
 import           Verifier.SAW.Module
 import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.Term.Functor
-import           Verifier.SAW.Translation.Coq.Monad
+import qualified Verifier.SAW.Translation.Coq.Monad            as M
 import           Verifier.SAW.Translation.Coq.SpecialTreatment
 import qualified Verifier.SAW.Translation.Coq.Term             as TermTranslation
+import Verifier.SAW.Translation.Coq.Monad
 
 -- import Debug.Trace
 
-data ModuleTranslationState = ModuleTranslationState
-  { _currentModule  :: Maybe ModuleName
-  }
-  deriving (Show)
-makeLenses ''ModuleTranslationState
-
-type ModuleTranslationMonad m = TranslationMonad ModuleTranslationState m
+type ModuleTranslationMonad m =
+  M.TranslationMonad TermTranslation.TranslationReader () m
 
 runModuleTranslationMonad ::
-  TranslationConfiguration -> Maybe ModuleName ->
+  M.TranslationConfiguration -> Maybe ModuleName ->
   (forall m. ModuleTranslationMonad m => m a) ->
-  Either (TranslationError Term) (a, ModuleTranslationState)
-runModuleTranslationMonad configuration modname =
-  runTranslationMonad configuration (ModuleTranslationState modname)
+  Either (M.TranslationError Term) (a, ())
+runModuleTranslationMonad configuration modName =
+  M.runTranslationMonad configuration (TermTranslation.TranslationReader modName) ()
 
 dropPi :: Coq.Term -> Coq.Term
 dropPi (Coq.Pi (_ : t) r) = Coq.Pi t r
@@ -162,15 +156,19 @@ liftTermTranslationMonad ::
   (forall n. TermTranslation.TermTranslationMonad   n => n a) ->
   (forall m. ModuleTranslationMonad m => m a)
 liftTermTranslationMonad n = do
-  configuration <- ask
-  cur_mod <- view currentModule <$> get
-  let r = TermTranslation.runTermTranslationMonad configuration cur_mod [] [] n
+  configuration <- asks translationConfiguration
+  configReader <- asks otherConfiguration
+  let r = TermTranslation.runTermTranslationMonad configuration configReader [] [] n
   case r of
     Left  e      -> Except.throwError e
     Right (a, _) -> do
       return a
 
-translateDecl :: TranslationConfiguration -> Maybe ModuleName -> ModuleDecl -> Doc ann
+translateDecl ::
+  M.TranslationConfiguration ->
+  Maybe ModuleName ->
+  ModuleDecl ->
+  Doc ann
 translateDecl configuration modname decl =
   case decl of
   TypeDecl td -> do
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 0a54491e0c..92e83624ba 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
@@ -25,7 +25,7 @@ Portability : portable
 module Verifier.SAW.Translation.Coq.SpecialTreatment where
 
 import           Control.Lens                       (_1, _2, over)
-import           Control.Monad.Reader               (ask)
+import           Control.Monad.Reader               (asks)
 import qualified Data.Map                           as Map
 import           Data.String.Interpolate            (i)
 import qualified Data.Text                          as Text
@@ -70,10 +70,10 @@ translateModuleName mn =
   Map.findWithDefault mn mn moduleRenamingMap
 
 findSpecialTreatment ::
-  TranslationConfigurationMonad m =>
+  TranslationConfigurationMonad r m =>
   Ident -> m IdentSpecialTreatment
 findSpecialTreatment ident = do
-  configuration <- ask
+  configuration <- asks translationConfiguration
   let moduleMap =
         Map.findWithDefault Map.empty (identModule ident) (specialTreatmentMap configuration)
   let defaultTreatment =
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 d51d405819..ec1548c9aa 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
@@ -62,6 +62,13 @@ traceTerm :: String -> Term -> a -> a
 traceTerm ctx t a = trace (ctx ++ ": " ++ showTerm t) a
 -}
 
+newtype TranslationReader = TranslationReader
+  { _currentModule  :: Maybe ModuleName
+  }
+  deriving (Show)
+
+makeLenses ''TranslationReader
+
 data TranslationState = TranslationState
 
   { _globalDeclarations :: [String]
@@ -70,7 +77,7 @@ data TranslationState = TranslationState
   -- same file).  We want to translate those exactly once, so we need to keep
   -- track of which ones have already been translated.
 
-  , _localDeclarations :: [Coq.Decl]
+  , _topLevelDeclarations :: [Coq.Decl]
   -- ^ Because some terms capture their dependencies, translating one term may
   -- result in multiple declarations: one for the term itself, but also zero or
   -- many for its dependencies.  We store all of those in this, so that a caller
@@ -95,12 +102,14 @@ data TranslationState = TranslationState
   -- ^ The next available name to be used for a let-bound shared
   -- sub-expression.
 
-  , _currentModule :: Maybe ModuleName
   }
   deriving (Show)
 
 makeLenses ''TranslationState
 
+type TermTranslationMonad m =
+  TranslationMonad TranslationReader TranslationState m
+
 -- | The set of reserved identifiers in Coq, obtained from section
 -- "Gallina Specification Language" of the Coq reference manual.
 -- <https://coq.inria.fr/refman/language/gallina-specification-language.html>
@@ -134,52 +143,61 @@ getNamesOfAllDeclarations ::
 getNamesOfAllDeclarations = view allDeclarations <$> get
   where
     allDeclarations =
-      to (\ (TranslationState {..}) -> namedDecls _localDeclarations ++ _globalDeclarations)
-
-type TermTranslationMonad m = TranslationMonad TranslationState m
+      to (\ (TranslationState {..}) -> namedDecls _topLevelDeclarations ++ _globalDeclarations)
 
 runTermTranslationMonad ::
   TranslationConfiguration ->
-  Maybe ModuleName ->
+  TranslationReader ->
   [String] ->
   [Coq.Ident] ->
   (forall m. TermTranslationMonad m => m a) ->
   Either (TranslationError Term) (a, TranslationState)
-runTermTranslationMonad configuration modname globalDecls localEnv =
-  runTranslationMonad configuration
+runTermTranslationMonad configuration r globalDecls localEnv =
+  runTranslationMonad configuration r
   (TranslationState { _globalDeclarations = globalDecls
-                    , _localDeclarations  = []
+                    , _topLevelDeclarations  = []
                     , _localEnvironment   = localEnv
                     , _unavailableIdents  = Set.union reservedIdents (Set.fromList localEnv)
                     , _sharedNames        = IntMap.empty
                     , _nextSharedName     = "var__0"
-                    , _currentModule      = modname
                     })
 
 errorTermM :: TermTranslationMonad m => String -> m Coq.Term
 errorTermM str = return $ Coq.App (Coq.Var "error") [Coq.StringLit str]
 
 translateIdentWithArgs :: TermTranslationMonad m => Ident -> [Term] -> m Coq.Term
-translateIdentWithArgs i args =
-  (view currentModule <$> get) >>= \cur_modname ->
+translateIdentWithArgs i args = do
+  currentModuleName <- asks (view currentModule . otherConfiguration)
   let identToCoq ident =
-        if Just (identModule ident) == cur_modname then identName ident else
-          show (translateModuleName (identModule ident))
-          ++ "." ++ identName ident in
+        if Just (identModule ident) == currentModuleName
+          then identName ident
+          else
+            show (translateModuleName (identModule ident))
+            ++ "." ++ identName ident
+  specialTreatment <- findSpecialTreatment i
+  applySpecialTreatment identToCoq (atUseSite specialTreatment)
 
-  (atUseSite <$> findSpecialTreatment i) >>= \case
-    UsePreserve -> Coq.App (Coq.ExplVar $ identToCoq i) <$> mapM translateTerm args
-    UseRename targetModule targetName ->
-      Coq.App (Coq.ExplVar $ identToCoq $
-               mkIdent (fromMaybe (translateModuleName $ identModule i) targetModule)
-               (Text.pack targetName)) <$>
-      mapM translateTerm args
-    UseReplaceDropArgs n replacement
-      | length args >= n -> Coq.App replacement <$> mapM translateTerm (drop n args)
-    UseReplaceDropArgs n _ ->
-      errorTermM ("Identifier " ++ show i
-                  ++ " not applied to required number of args,"
-                  ++ " which is " ++ show n)
+  where
+
+    applySpecialTreatment identToCoq UsePreserve =
+      Coq.App (Coq.ExplVar $ identToCoq i) <$> mapM translateTerm args
+    applySpecialTreatment identToCoq (UseRename targetModule targetName) =
+      Coq.App
+        (Coq.ExplVar $ identToCoq $
+          mkIdent (fromMaybe (translateModuleName $ identModule i) targetModule)
+          (Text.pack targetName))
+          <$> mapM translateTerm args
+    applySpecialTreatment _identToCoq (UseReplaceDropArgs n replacement)
+      | length args >= n =
+        Coq.App replacement <$> mapM translateTerm (drop n args)
+    applySpecialTreatment _identToCoq (UseReplaceDropArgs n _) =
+      errorTermM (unwords
+        [ "Identifier"
+        , show i
+        , "not applied to required number of args, which is"
+        , show n
+        ]
+      )
 
 translateIdent :: TermTranslationMonad m => Ident -> m Coq.Term
 translateIdent i = translateIdentWithArgs i []
@@ -318,13 +336,34 @@ asApplyAllRecognizer :: Recognizer Term (Term, [Term])
 asApplyAllRecognizer t = do _ <- asApp t
                             return $ asApplyAll t
 
--- | Run a translation, but keep changes to the environment local to it,
--- restoring the current environment before returning.
-withLocalLocalEnvironment :: TermTranslationMonad m => m a -> m a
-withLocalLocalEnvironment action = do
-  s <- get
+-- | Run a translation, but keep some changes to the translation state local to
+-- that computation, restoring parts of the original translation state before
+-- returning.
+withLocalTranslationState :: TermTranslationMonad m => m a -> m a
+withLocalTranslationState action = do
+  before <- get
   result <- action
-  put s
+  after <- get
+  put (TranslationState
+    -- globalDeclarations is **not** restored, because we want to translate each
+    -- global declaration exactly once!
+    { _globalDeclarations = view globalDeclarations after
+    -- topLevelDeclarations is **not** restored, because it accumulates the
+    -- declarations witnessed in a given module so that we can extract it.
+    , _topLevelDeclarations = view topLevelDeclarations after
+    -- localEnvironment **is** restored, because the identifiers added to it
+    -- during translation are local to the term that was being translated.
+    , _localEnvironment = view localEnvironment before
+    -- unavailableIdents **is** restored, because the extra identifiers
+    -- unavailable in the term that was translated are local to it.
+    , _unavailableIdents = view unavailableIdents before
+    -- sharedNames **is** restored, because we are leaving the scope of the
+    -- locally shared names.
+    , _sharedNames = view sharedNames before
+    -- nextSharedName **is** restored, because we are leaving the scope of the
+    -- last names used.
+    , _nextSharedName = view nextSharedName before
+    })
   return result
 
 mkDefinition :: Coq.Ident -> Coq.Term -> Coq.Decl
@@ -354,7 +393,7 @@ translateParams ((n, ty):ps) = do
   return (Coq.Binder n' (Just ty') : ps')
 
 translatePi :: TermTranslationMonad m => [(LocalName, Term)] -> Term -> m Coq.Term
-translatePi binders body = withLocalLocalEnvironment $ do
+translatePi binders body = withLocalTranslationState $ do
   bindersT <- forM binders $ \ (b, bType) -> do
     bTypeT <- translateTerm bType
     b' <- freshenAndBindName b
@@ -389,7 +428,7 @@ nextVariant = reverse . go . reverse
 
 translateTermLet :: TermTranslationMonad m => Term -> m Coq.Term
 translateTermLet t =
-  withLocalLocalEnvironment $
+  withLocalTranslationState $
   do let counts = scTermCount False t
      let locals = fmap fst $ IntMap.filter keep counts
      names <- traverse (const nextName) locals
@@ -419,7 +458,7 @@ translateTerm t =
            Just x -> pure (Coq.Var x)
 
 translateTermUnshared :: TermTranslationMonad m => Term -> m Coq.Term
-translateTermUnshared t = withLocalLocalEnvironment $ do
+translateTermUnshared t = withLocalTranslationState $ do
   -- traceTerm "translateTerm" t $
   -- NOTE: env is in innermost-first order
   env <- view localEnvironment <$> get
@@ -487,7 +526,7 @@ translateTermUnshared t = withLocalLocalEnvironment $ do
                   do
                     len <- translateTerm n
                     (x', expr) <-
-                      withLocalLocalEnvironment $
+                      withLocalTranslationState $
                       do x' <- freshenAndBindName x
                          expr <- translateTerm body
                          pure (x', expr)
@@ -514,7 +553,7 @@ translateTermUnshared t = withLocalLocalEnvironment $ do
               case lambda of
               (asLambdaList -> ((recFn, _) : binders, body)) -> do
                 let (_binderPis, otherPis) = splitAt (length binders) pis
-                (recFn', bindersT, typeT, bodyT) <- withLocalLocalEnvironment $ do
+                (recFn', bindersT, typeT, bodyT) <- withLocalTranslationState $ do
                   -- this is very ugly...
                   recFn' <- freshenAndBindName recFn
                   bindersT <- mapM
@@ -543,7 +582,7 @@ translateTermUnshared t = withLocalLocalEnvironment $ do
 
   -- Constants come with a body
     Constant n body -> do
-      configuration <- ask
+      configuration <- asks translationConfiguration
       let renamed = translateConstant (notations configuration) n
       alreadyTranslatedDecls <- getNamesOfAllDeclarations
       let definitionsToSkip = skipDefinitions configuration
@@ -552,13 +591,13 @@ translateTermUnshared t = withLocalLocalEnvironment $ do
         else do
         b <-
           -- Translate body in a top-level name scope
-          withLocalLocalEnvironment $
+          withLocalTranslationState $
           do modify $ set localEnvironment []
              modify $ set unavailableIdents reservedIdents
              modify $ set sharedNames IntMap.empty
              modify $ set nextSharedName "var__0"
              translateTermLet body
-        modify $ over localDeclarations $ (mkDefinition renamed b :)
+        modify $ over topLevelDeclarations $ (mkDefinition renamed b :)
         Coq.Var <$> pure renamed
 
   where
@@ -590,16 +629,16 @@ defaultTermForType typ = do
 
 translateTermToDocWith ::
   TranslationConfiguration ->
-  Maybe ModuleName ->
+  TranslationReader ->
   [String] ->
   [String] ->
   (Coq.Term -> Doc ann) ->
   Term ->
   Either (TranslationError Term) (Doc ann)
-translateTermToDocWith configuration mn globalDecls localEnv f t = do
+translateTermToDocWith configuration r globalDecls localEnv f t = do
   (term, state) <-
-    runTermTranslationMonad configuration mn globalDecls localEnv (translateTermLet t)
-  let decls = view localDeclarations state
+    runTermTranslationMonad configuration r globalDecls localEnv (translateTermLet t)
+  let decls = view topLevelDeclarations state
   return $
     vcat $
     [ (vcat . intersperse hardline . map Coq.ppDecl . reverse) decls
@@ -609,10 +648,10 @@ translateTermToDocWith configuration mn globalDecls localEnv f t = do
 
 translateDefDoc ::
   TranslationConfiguration ->
-  Maybe ModuleName ->
+  TranslationReader ->
   [String] ->
   Coq.Ident -> Term ->
   Either (TranslationError Term) (Doc ann)
-translateDefDoc configuration mn globalDecls name =
-  translateTermToDocWith configuration mn globalDecls [name]
-  (\ term -> Coq.ppDecl (mkDefinition name term))
+translateDefDoc configuration r globalDecls name =
+  translateTermToDocWith configuration r globalDecls [name]
+  (Coq.ppDecl . mkDefinition name)