diff --git a/rr_frontend/translation/src/body/translation/basicblock.rs b/rr_frontend/translation/src/body/translation/basicblock.rs
index 927fcf2d08a5abe828ba0b4135e8a9bfccca16c1..2f74d8776976a90e159ccc8dd50febab8af132f0 100644
--- a/rr_frontend/translation/src/body/translation/basicblock.rs
+++ b/rr_frontend/translation/src/body/translation/basicblock.rs
@@ -6,8 +6,7 @@
 
 use std::collections::{btree_map, BTreeMap, HashMap, HashSet};
 
-use log::{info, trace, warn};
-use radium::coq;
+use log::info;
 use rr_rustc_interface::hir::def_id::DefId;
 use rr_rustc_interface::middle::mir::interpret::{ConstValue, ErrorHandled, Scalar};
 use rr_rustc_interface::middle::mir::tcx::PlaceTy;
@@ -20,20 +19,9 @@ use rr_rustc_interface::middle::ty::fold::TypeFolder;
 use rr_rustc_interface::middle::ty::{ConstKind, Ty, TyKind};
 use rr_rustc_interface::middle::{mir, ty};
 use rr_rustc_interface::{abi, ast, middle};
-use typed_arena::Arena;
 
 use super::TX;
 use crate::base::*;
-use crate::body::checked_op_analysis::CheckedOpLocalAnalysis;
-use crate::environment::borrowck::facts;
-use crate::environment::polonius_info::PoloniusInfo;
-use crate::environment::procedure::Procedure;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::regions::inclusion_tracker::InclusionTracker;
-use crate::spec_parsers::parse_utils::ParamLookup;
-use crate::spec_parsers::verbose_function_spec_parser::{
-    ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
-};
 use crate::traits::{registry, resolution};
 use crate::{base, consts, procedures, regions, search, traits, types};
 
diff --git a/rr_frontend/translation/src/body/translation/calls.rs b/rr_frontend/translation/src/body/translation/calls.rs
index 3be93470555480ac58dc92392d2c5e212cef6b3a..5229e096f89e83c286d0df33400b403f10fdfdf8 100644
--- a/rr_frontend/translation/src/body/translation/calls.rs
+++ b/rr_frontend/translation/src/body/translation/calls.rs
@@ -4,10 +4,7 @@
 // If a copy of the BSD-3-clause license was not distributed with this
 // file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
 
-use std::collections::{btree_map, BTreeMap, HashMap, HashSet};
-
-use log::{info, trace, warn};
-use radium::coq;
+use log::{info, trace};
 use rr_rustc_interface::hir::def_id::DefId;
 use rr_rustc_interface::middle::mir::interpret::{ConstValue, ErrorHandled, Scalar};
 use rr_rustc_interface::middle::mir::tcx::PlaceTy;
@@ -20,22 +17,12 @@ use rr_rustc_interface::middle::ty::fold::TypeFolder;
 use rr_rustc_interface::middle::ty::{ConstKind, Ty, TyKind};
 use rr_rustc_interface::middle::{mir, ty};
 use rr_rustc_interface::{abi, ast, middle};
-use typed_arena::Arena;
 
 use super::TX;
 use crate::base::*;
-use crate::body::checked_op_analysis::CheckedOpLocalAnalysis;
 use crate::environment::borrowck::facts;
-use crate::environment::polonius_info::PoloniusInfo;
-use crate::environment::procedure::Procedure;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::regions::inclusion_tracker::InclusionTracker;
-use crate::spec_parsers::parse_utils::ParamLookup;
-use crate::spec_parsers::verbose_function_spec_parser::{
-    ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
-};
-use crate::traits::{registry, resolution};
-use crate::{base, consts, procedures, regions, search, traits, types};
+use crate::traits::resolution;
+use crate::{regions, types};
 
 /// Get the syntypes of function arguments for a procedure call.
 fn get_arg_syntypes_for_procedure_call<'tcx, 'def>(
diff --git a/rr_frontend/translation/src/body/translation/constants.rs b/rr_frontend/translation/src/body/translation/constants.rs
index 34e616362265b033316feb4833d01814bcce08df..dd9a5206d002e7f5ea1395aa50e58363722c7382 100644
--- a/rr_frontend/translation/src/body/translation/constants.rs
+++ b/rr_frontend/translation/src/body/translation/constants.rs
@@ -4,10 +4,7 @@
 // If a copy of the BSD-3-clause license was not distributed with this
 // file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
 
-use std::collections::{btree_map, BTreeMap, HashMap, HashSet};
-
-use log::{info, trace, warn};
-use radium::coq;
+use log::info;
 use rr_rustc_interface::hir::def_id::DefId;
 use rr_rustc_interface::middle::mir::interpret::{ConstValue, ErrorHandled, Scalar};
 use rr_rustc_interface::middle::mir::tcx::PlaceTy;
@@ -20,22 +17,9 @@ use rr_rustc_interface::middle::ty::fold::TypeFolder;
 use rr_rustc_interface::middle::ty::{ConstKind, Ty, TyKind};
 use rr_rustc_interface::middle::{mir, ty};
 use rr_rustc_interface::{abi, ast, middle};
-use typed_arena::Arena;
 
 use super::TX;
 use crate::base::*;
-use crate::body::checked_op_analysis::CheckedOpLocalAnalysis;
-use crate::environment::borrowck::facts;
-use crate::environment::polonius_info::PoloniusInfo;
-use crate::environment::procedure::Procedure;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::regions::inclusion_tracker::InclusionTracker;
-use crate::spec_parsers::parse_utils::ParamLookup;
-use crate::spec_parsers::verbose_function_spec_parser::{
-    ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
-};
-use crate::traits::{registry, resolution};
-use crate::{base, consts, procedures, regions, search, traits, types};
 
 impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
     /// Translate a scalar at a specific type to a `radium::Expr`.
diff --git a/rr_frontend/translation/src/body/translation/loops.rs b/rr_frontend/translation/src/body/translation/loops.rs
index 6f8ef41f6d78cc3fb695c0ad3c94b1308dbc640c..e6bcc1f0ce8c55da512f81e32e77c4653a4a9f4d 100644
--- a/rr_frontend/translation/src/body/translation/loops.rs
+++ b/rr_frontend/translation/src/body/translation/loops.rs
@@ -4,9 +4,7 @@
 // If a copy of the BSD-3-clause license was not distributed with this
 // file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
 
-use std::collections::{btree_map, BTreeMap, HashMap, HashSet};
-
-use log::{info, trace, warn};
+use log::info;
 use radium::coq;
 use rr_rustc_interface::hir::def_id::DefId;
 use rr_rustc_interface::middle::mir::interpret::{ConstValue, ErrorHandled, Scalar};
@@ -20,22 +18,9 @@ use rr_rustc_interface::middle::ty::fold::TypeFolder;
 use rr_rustc_interface::middle::ty::{ConstKind, Ty, TyKind};
 use rr_rustc_interface::middle::{mir, ty};
 use rr_rustc_interface::{abi, ast, middle};
-use typed_arena::Arena;
 
 use super::TX;
 use crate::base::*;
-use crate::body::checked_op_analysis::CheckedOpLocalAnalysis;
-use crate::environment::borrowck::facts;
-use crate::environment::polonius_info::PoloniusInfo;
-use crate::environment::procedure::Procedure;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::regions::inclusion_tracker::InclusionTracker;
-use crate::spec_parsers::parse_utils::ParamLookup;
-use crate::spec_parsers::verbose_function_spec_parser::{
-    ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
-};
-use crate::traits::{registry, resolution};
-use crate::{base, consts, procedures, regions, search, traits, types};
 
 impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
     /// Parse the attributes on spec closure `did` as loop annotations and add it as an invariant
diff --git a/rr_frontend/translation/src/body/translation/mod.rs b/rr_frontend/translation/src/body/translation/mod.rs
index 5c3f407e2e31f247b403eb610f5287b014cb4b77..8372bba3b2e7b6d4db714128358aa8e33b5c2105 100644
--- a/rr_frontend/translation/src/body/translation/mod.rs
+++ b/rr_frontend/translation/src/body/translation/mod.rs
@@ -12,10 +12,9 @@ mod place;
 mod rvalue;
 mod terminator;
 
-use std::collections::{btree_map, BTreeMap, HashMap, HashSet};
+use std::collections::{HashMap, HashSet};
 
-use log::{info, trace, warn};
-use radium::coq;
+use log::info;
 use rr_rustc_interface::hir::def_id::DefId;
 use rr_rustc_interface::middle::mir::interpret::{ConstValue, ErrorHandled, Scalar};
 use rr_rustc_interface::middle::mir::tcx::PlaceTy;
@@ -35,14 +34,10 @@ use crate::body::checked_op_analysis::CheckedOpLocalAnalysis;
 use crate::environment::borrowck::facts;
 use crate::environment::polonius_info::PoloniusInfo;
 use crate::environment::procedure::Procedure;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
+use crate::environment::{polonius_info, Environment};
 use crate::regions::inclusion_tracker::InclusionTracker;
-use crate::spec_parsers::parse_utils::ParamLookup;
-use crate::spec_parsers::verbose_function_spec_parser::{
-    ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
-};
-use crate::traits::{registry, resolution};
-use crate::{base, consts, procedures, regions, search, traits, types};
+use crate::traits::registry;
+use crate::{base, consts, procedures, regions, types};
 
 /// Struct that keeps track of all information necessary to translate a MIR Body to a `radium::Function`.
 /// `'a` is the lifetime of the translator and ends after translation has finished.
diff --git a/rr_frontend/translation/src/body/translation/place.rs b/rr_frontend/translation/src/body/translation/place.rs
index e25574446872ee6f7d0b44466ff6222d284af1ff..4625823b03f7283d1065e585743350956b7b383a 100644
--- a/rr_frontend/translation/src/body/translation/place.rs
+++ b/rr_frontend/translation/src/body/translation/place.rs
@@ -4,10 +4,7 @@
 // If a copy of the BSD-3-clause license was not distributed with this
 // file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
 
-use std::collections::{btree_map, BTreeMap, HashMap, HashSet};
-
-use log::{info, trace, warn};
-use radium::coq;
+use log::info;
 use rr_rustc_interface::hir::def_id::DefId;
 use rr_rustc_interface::middle::mir::interpret::{ConstValue, ErrorHandled, Scalar};
 use rr_rustc_interface::middle::mir::tcx::PlaceTy;
@@ -20,22 +17,10 @@ use rr_rustc_interface::middle::ty::fold::TypeFolder;
 use rr_rustc_interface::middle::ty::{ConstKind, Ty, TyKind};
 use rr_rustc_interface::middle::{mir, ty};
 use rr_rustc_interface::{abi, ast, middle};
-use typed_arena::Arena;
 
 use super::TX;
 use crate::base::*;
-use crate::body::checked_op_analysis::CheckedOpLocalAnalysis;
-use crate::environment::borrowck::facts;
-use crate::environment::polonius_info::PoloniusInfo;
-use crate::environment::procedure::Procedure;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::regions::inclusion_tracker::InclusionTracker;
-use crate::spec_parsers::parse_utils::ParamLookup;
-use crate::spec_parsers::verbose_function_spec_parser::{
-    ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
-};
-use crate::traits::{registry, resolution};
-use crate::{base, consts, procedures, regions, search, traits, types};
+use crate::types;
 
 impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
     /// Translate a place to a Caesium lvalue.
diff --git a/rr_frontend/translation/src/body/translation/rvalue.rs b/rr_frontend/translation/src/body/translation/rvalue.rs
index 426d3c021455f5ac5c86f1c404016c9c4b6b2cdc..0ea174c498930b39ef7ed484d1ac00da486fa79c 100644
--- a/rr_frontend/translation/src/body/translation/rvalue.rs
+++ b/rr_frontend/translation/src/body/translation/rvalue.rs
@@ -4,9 +4,7 @@
 // If a copy of the BSD-3-clause license was not distributed with this
 // file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
 
-use std::collections::{btree_map, BTreeMap, HashMap, HashSet};
-
-use log::{info, trace, warn};
+use log::{info, trace};
 use radium::coq;
 use rr_rustc_interface::hir::def_id::DefId;
 use rr_rustc_interface::index::IndexVec;
@@ -21,22 +19,10 @@ use rr_rustc_interface::middle::ty::fold::TypeFolder;
 use rr_rustc_interface::middle::ty::{ConstKind, Ty, TyKind};
 use rr_rustc_interface::middle::{mir, ty};
 use rr_rustc_interface::{abi, ast, middle};
-use typed_arena::Arena;
 
 use super::TX;
 use crate::base::*;
-use crate::body::checked_op_analysis::CheckedOpLocalAnalysis;
-use crate::environment::borrowck::facts;
-use crate::environment::polonius_info::PoloniusInfo;
-use crate::environment::procedure::Procedure;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::regions::inclusion_tracker::InclusionTracker;
-use crate::spec_parsers::parse_utils::ParamLookup;
-use crate::spec_parsers::verbose_function_spec_parser::{
-    ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
-};
-use crate::traits::{registry, resolution};
-use crate::{base, consts, procedures, regions, search, traits, types};
+use crate::regions;
 
 impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
     /// Translate an aggregate expression.
diff --git a/rr_frontend/translation/src/body/translation/terminator.rs b/rr_frontend/translation/src/body/translation/terminator.rs
index 4f73ccc98d3ee82256d03940440b826317569d0b..ca749be7a0f50adee360245bb0fc008a2aab3ef2 100644
--- a/rr_frontend/translation/src/body/translation/terminator.rs
+++ b/rr_frontend/translation/src/body/translation/terminator.rs
@@ -4,10 +4,9 @@
 // If a copy of the BSD-3-clause license was not distributed with this
 // file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
 
-use std::collections::{btree_map, BTreeMap, HashMap, HashSet};
+use std::collections::HashMap;
 
 use log::{info, trace, warn};
-use radium::coq;
 use rr_rustc_interface::hir::def_id::DefId;
 use rr_rustc_interface::middle::mir::interpret::{ConstValue, ErrorHandled, Scalar};
 use rr_rustc_interface::middle::mir::tcx::PlaceTy;
@@ -20,22 +19,11 @@ use rr_rustc_interface::middle::ty::fold::TypeFolder;
 use rr_rustc_interface::middle::ty::{ConstKind, Ty, TyKind};
 use rr_rustc_interface::middle::{mir, ty};
 use rr_rustc_interface::{abi, ast, middle};
-use typed_arena::Arena;
 
 use super::TX;
 use crate::base::*;
-use crate::body::checked_op_analysis::CheckedOpLocalAnalysis;
 use crate::environment::borrowck::facts;
-use crate::environment::polonius_info::PoloniusInfo;
-use crate::environment::procedure::Procedure;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::regions::inclusion_tracker::InclusionTracker;
-use crate::spec_parsers::parse_utils::ParamLookup;
-use crate::spec_parsers::verbose_function_spec_parser::{
-    ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
-};
-use crate::traits::{registry, resolution};
-use crate::{base, consts, procedures, regions, search, traits, types};
+use crate::search;
 
 impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
     /// Check if a call goes to `std::rt::begin_panic`