diff --git a/DynamoDbEncryption/runtimes/rust/Cargo.toml b/DynamoDbEncryption/runtimes/rust/Cargo.toml
index 802c0b926..4e75acfcc 100644
--- a/DynamoDbEncryption/runtimes/rust/Cargo.toml
+++ b/DynamoDbEncryption/runtimes/rust/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "aws-db-esdk"
-version = "1.0.0"
+version = "1.1.0"
 edition = "2021"
 rust-version = "1.81.0"
 keywords = ["cryptography", "security", "dynamodb", "encryption", "client-side"]
@@ -17,8 +17,8 @@ readme = "README.md"
 
 [dependencies]
 aws-config = "1.6.2"
-aws-lc-rs = "1.13.0"
-aws-lc-sys = "0.28.2"
+aws-lc-rs = "1.13.1"
+aws-lc-sys = "0.29.0"
 aws-sdk-dynamodb = "1.73.0"
 aws-sdk-kms = "1.67.0"
 aws-smithy-runtime-api = {version = "1.8.0", features = ["client"] }
diff --git a/DynamoDbEncryption/runtimes/rust/start_release.sh b/DynamoDbEncryption/runtimes/rust/start_release.sh
index 921fbd36c..f7f8aeefc 100755
--- a/DynamoDbEncryption/runtimes/rust/start_release.sh
+++ b/DynamoDbEncryption/runtimes/rust/start_release.sh
@@ -68,7 +68,7 @@ cargo clippy --example main
 
 # replace local path with latest dafny-runtime from crates.io
 cargo rm dafny_runtime
-cargo add dafny-runtime -F sync
+cargo add dafny-runtime -F sync -F small-int
 
 # Run cargo test and example tests
 cargo test --release
diff --git a/TestVectors/runtimes/rust/Cargo.toml b/TestVectors/runtimes/rust/Cargo.toml
index 9faf67d5d..dace76318 100644
--- a/TestVectors/runtimes/rust/Cargo.toml
+++ b/TestVectors/runtimes/rust/Cargo.toml
@@ -12,8 +12,8 @@ wrapped-client = []
 
 [dependencies]
 aws-config = "1.6.2"
-aws-lc-rs = "1.13.0"
-aws-lc-sys = "0.28.2"
+aws-lc-rs = "1.13.1"
+aws-lc-sys = "0.29.0"
 aws-sdk-dynamodb = "1.73.0"
 aws-sdk-kms = "1.67.0"
 aws-smithy-runtime-api = {version = "1.8.0", features = ["client"] }
diff --git a/releases/rust/db_esdk/dafny_runtime_rust/Cargo.toml b/releases/rust/db_esdk/dafny_runtime_rust/Cargo.toml
index ac3e72c39..297d60046 100644
--- a/releases/rust/db_esdk/dafny_runtime_rust/Cargo.toml
+++ b/releases/rust/db_esdk/dafny_runtime_rust/Cargo.toml
@@ -1,18 +1,18 @@
 [package]
-name = "dafny-runtime"
-version = "0.2.0"
+name = "dafny_runtime"
+version = "0.3.0"
 edition = "2021"
-keywords = ["dafny"]
-license = "ISC AND (Apache-2.0 OR ISC)"
-description = "dafny-runtime is the runtime support library for Rust code gerated from Dafny."
-repository = "https://github.com/aws/aws-database-encryption-sdk-dynamodb/tree/main/releases/rust/db_esdk/dafny_runtime_rust"
-authors = ["AWS-CryptoTools"]
-readme = "README.md"
 
 [dependencies]
-once_cell = "1.18.0"
-num = "0.4"
-itertools = "0.11.0"
+once_cell = "1.21.3"
+num = "0.4.3"
+itertools = "0.14.0"
 
 [features]
+# Use `dafny translate rs --rust-sync --include-runtime file.dfy`
+# to compile to code where values can be sent safely through threads
+# This will include the runtime with the sync feature
+
+# Use --features small-int to make DafnyInt use i128 instead of num::BigInt
 sync = []
+small-int = []
diff --git a/releases/rust/db_esdk/dafny_runtime_rust/src/big_int.rs b/releases/rust/db_esdk/dafny_runtime_rust/src/big_int.rs
new file mode 100644
index 000000000..859cd77d0
--- /dev/null
+++ b/releases/rust/db_esdk/dafny_runtime_rust/src/big_int.rs
@@ -0,0 +1,420 @@
+use crate::DafnyPrint;
+use crate::Rc;
+use num::bigint::BigInt;
+use num::rational::BigRational;
+use num::FromPrimitive;
+use num::ToPrimitive;
+use num::{bigint::ParseBigIntError, Integer, Num, One, Signed, Zero};
+use std::{
+    clone::Clone,
+    cmp::Ordering,
+    convert::From,
+    fmt::Formatter,
+    hash::Hash,
+    ops::{Add, Div, Mul, Neg, Rem, Sub},
+};
+
+// Zero-cost abstraction over a Rc<BigInt>
+
+#[derive(Clone)]
+pub struct DafnyInt {
+    data: Rc<BigInt>,
+}
+
+impl DafnyInt {
+    pub fn new(data: Rc<BigInt>) -> DafnyInt {
+        DafnyInt { data }
+    }
+    pub fn strong_count(&self) -> usize {
+        Rc::strong_count(&self.data)
+    }
+}
+
+impl AsRef<BigInt> for DafnyInt {
+    fn as_ref(&self) -> &BigInt {
+        &self.data
+    }
+}
+
+impl Default for DafnyInt {
+    fn default() -> Self {
+        DafnyInt::new(Rc::new(BigInt::zero()))
+    }
+}
+
+pub fn dafny_int_to_bigint(i: &DafnyInt) -> BigInt {
+    i.data.as_ref().clone()
+}
+pub fn bigint_to_dafny_int(i: &BigInt) -> DafnyInt {
+    DafnyInt {
+        data: Rc::new(i.clone()),
+    }
+}
+
+impl Zero for DafnyInt {
+    #[inline]
+    fn zero() -> Self {
+        DafnyInt {
+            data: Rc::new(BigInt::zero()),
+        }
+    }
+    #[inline]
+    fn is_zero(&self) -> bool {
+        self.data.is_zero()
+    }
+}
+impl One for DafnyInt {
+    #[inline]
+    fn one() -> Self {
+        DafnyInt {
+            data: Rc::new(BigInt::one()),
+        }
+    }
+}
+impl Num for DafnyInt {
+    type FromStrRadixErr = ParseBigIntError;
+
+    #[inline]
+    fn from_str_radix(s: &str, radix: u32) -> Result<Self, Self::FromStrRadixErr> {
+        Ok(DafnyInt {
+            data: Rc::new(BigInt::from_str_radix(s, radix)?),
+        })
+    }
+}
+impl Ord for DafnyInt {
+    #[inline]
+    fn cmp(&self, other: &Self) -> Ordering {
+        self.data.cmp(&other.data)
+    }
+}
+impl Signed for DafnyInt {
+    #[inline]
+    fn abs(&self) -> Self {
+        DafnyInt {
+            data: Rc::new(self.data.as_ref().abs()),
+        }
+    }
+
+    #[inline]
+    fn abs_sub(&self, other: &Self) -> Self {
+        DafnyInt {
+            data: Rc::new(self.data.as_ref().abs_sub(other.data.as_ref())),
+        }
+    }
+
+    #[inline]
+    fn signum(&self) -> Self {
+        DafnyInt {
+            data: Rc::new(self.data.as_ref().signum()),
+        }
+    }
+
+    #[inline]
+    fn is_positive(&self) -> bool {
+        self.data.as_ref().is_positive()
+    }
+
+    #[inline]
+    fn is_negative(&self) -> bool {
+        self.data.as_ref().is_negative()
+    }
+}
+
+// Comparison
+impl PartialOrd<DafnyInt> for DafnyInt {
+    #[inline]
+    fn partial_cmp(&self, other: &DafnyInt) -> Option<Ordering> {
+        Some(self.cmp(other))
+    }
+}
+
+impl DafnyInt {
+    #[inline]
+    pub fn parse_bytes(number: &[u8], radix: u32) -> DafnyInt {
+        DafnyInt {
+            data: Rc::new(BigInt::parse_bytes(number, radix).unwrap()),
+        }
+    }
+    pub fn from_usize(usize: usize) -> DafnyInt {
+        DafnyInt {
+            data: Rc::new(BigInt::from(usize)),
+        }
+    }
+    pub fn from_i32(i: i32) -> DafnyInt {
+        DafnyInt {
+            data: Rc::new(BigInt::from(i)),
+        }
+    }
+}
+
+// fn dafny_rational_to_int(r: &BigRational) -> BigInt {
+//     euclidian_division(r.numer().clone(), r.denom().clone())
+// }
+
+impl DafnyPrint for BigInt {
+    fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
+        write!(f, "{}", self)
+    }
+}
+
+fn divides_a_power_of_10(mut i: BigInt) -> (bool, BigInt, usize) {
+    let one: BigInt = One::one();
+
+    let mut factor = one.clone();
+    let mut log10 = 0;
+
+    let zero = Zero::zero();
+    let ten = BigInt::from_i32(10).unwrap();
+
+    if i <= zero {
+        return (false, factor, log10);
+    }
+
+    while i.is_multiple_of(&ten) {
+        i /= BigInt::from_i32(10).unwrap();
+        log10 += 1;
+    }
+
+    let two = BigInt::from_i32(2).unwrap();
+    let five = BigInt::from_i32(5).unwrap();
+
+    while i.is_multiple_of(&five) {
+        i /= &five;
+        factor *= &two;
+        log10 += 1;
+    }
+
+    while i.is_multiple_of(&two) {
+        i /= &two;
+        factor *= &two;
+        log10 += 1;
+    }
+
+    (i == one, factor, log10)
+}
+
+impl DafnyPrint for BigRational {
+    fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
+        if self.denom() == &One::one() || self.numer() == &Zero::zero() {
+            write!(f, "{}.0", self.numer())
+        } else {
+            let (divides, factor, log10) = divides_a_power_of_10(self.denom().clone());
+            if divides {
+                let mut num = self.numer().clone();
+                num *= factor;
+
+                if num.is_negative() {
+                    write!(f, "-")?;
+                    num = -num;
+                }
+
+                let digits = num.to_string();
+
+                if log10 < digits.len() {
+                    let digit_count = digits.len() - log10;
+                    write!(f, "{}", &digits[..digit_count])?;
+                    write!(f, ".")?;
+                    write!(f, "{}", &digits[digit_count..])
+                } else {
+                    let z = log10 - digits.len();
+                    write!(f, "0.")?;
+                    for _ in 0..z {
+                        write!(f, "0")?;
+                    }
+                    write!(f, "{}", digits)
+                }
+            } else {
+                write!(f, "({}.0 / {}.0)", self.numer(), self.denom())
+            }
+        }
+    }
+}
+
+impl From<DafnyInt> for u8 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_u8().unwrap()
+    }
+}
+impl From<DafnyInt> for u16 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_u16().unwrap()
+    }
+}
+impl From<DafnyInt> for u32 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_u32().unwrap()
+    }
+}
+impl From<DafnyInt> for u64 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_u64().unwrap()
+    }
+}
+impl From<DafnyInt> for u128 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_u128().unwrap()
+    }
+}
+impl From<DafnyInt> for i8 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_i8().unwrap()
+    }
+}
+impl From<DafnyInt> for i16 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_i16().unwrap()
+    }
+}
+impl From<DafnyInt> for i32 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_i32().unwrap()
+    }
+}
+impl From<DafnyInt> for i64 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_i64().unwrap()
+    }
+}
+impl From<DafnyInt> for i128 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_i128().unwrap()
+    }
+}
+impl From<DafnyInt> for usize {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_usize().unwrap()
+    }
+}
+
+impl ToPrimitive for DafnyInt {
+    fn to_i64(&self) -> Option<i64> {
+        self.data.to_i64()
+    }
+
+    fn to_u64(&self) -> Option<u64> {
+        self.data.to_u64()
+    }
+
+    // Override of functions
+    fn to_u128(&self) -> Option<u128> {
+        self.data.to_u128()
+    }
+
+    fn to_i128(&self) -> Option<i128> {
+        self.data.to_i128()
+    }
+}
+
+impl PartialEq<DafnyInt> for DafnyInt {
+    fn eq(&self, other: &DafnyInt) -> bool {
+        self.data.eq(&other.data)
+    }
+}
+impl Eq for DafnyInt {}
+impl Hash for DafnyInt {
+    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
+        self.data.hash(state);
+    }
+}
+
+impl DafnyPrint for DafnyInt {
+    fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
+        write!(f, "{}", self.data)
+    }
+}
+
+impl ::std::fmt::Debug for DafnyInt {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{}", self.data)
+    }
+}
+
+impl Add<DafnyInt> for DafnyInt {
+    type Output = DafnyInt;
+
+    fn add(self, rhs: DafnyInt) -> Self::Output {
+        DafnyInt {
+            data: Rc::new(self.data.as_ref() + rhs.data.as_ref()),
+        }
+    }
+}
+
+impl Mul<DafnyInt> for DafnyInt {
+    type Output = DafnyInt;
+
+    fn mul(self, rhs: DafnyInt) -> Self::Output {
+        DafnyInt {
+            data: Rc::new(self.data.as_ref() * rhs.data.as_ref()),
+        }
+    }
+}
+
+impl Div<DafnyInt> for DafnyInt {
+    type Output = DafnyInt;
+
+    fn div(self, rhs: DafnyInt) -> Self::Output {
+        DafnyInt {
+            data: Rc::new(self.data.as_ref() / rhs.data.as_ref()),
+        }
+    }
+}
+
+impl Sub<DafnyInt> for DafnyInt {
+    type Output = DafnyInt;
+
+    fn sub(self, rhs: DafnyInt) -> Self::Output {
+        DafnyInt {
+            data: Rc::new(self.data.as_ref() - rhs.data.as_ref()),
+        }
+    }
+}
+impl Rem<DafnyInt> for DafnyInt {
+    type Output = DafnyInt;
+
+    fn rem(self, rhs: DafnyInt) -> Self::Output {
+        DafnyInt {
+            data: Rc::new(self.data.as_ref() % rhs.data.as_ref()),
+        }
+    }
+}
+impl Neg for DafnyInt {
+    type Output = DafnyInt;
+
+    #[inline]
+    fn neg(self) -> Self::Output {
+        DafnyInt {
+            data: Rc::new(-self.data.as_ref()),
+        }
+    }
+}
+
+macro_rules! impl_dafnyint_from {
+    () => {};
+    ($type:ident) => {
+        impl ::std::convert::From<$type> for $crate::DafnyInt {
+            fn from(n: $type) -> Self {
+                $crate::DafnyInt {
+                    data: $crate::Rc::new(n.into()),
+                }
+            }
+        }
+        #[allow(trivial_numeric_casts)]
+        impl $crate::DafnyUsize for $type {
+            fn into_usize(self) -> usize {
+                self as usize
+            }
+        }
+    };
+}
+
+impl_dafnyint_from! { u8 }
+impl_dafnyint_from! { u16 }
+impl_dafnyint_from! { u32 }
+impl_dafnyint_from! { u64 }
+impl_dafnyint_from! { u128 }
+impl_dafnyint_from! { i8 }
+impl_dafnyint_from! { i16 }
+impl_dafnyint_from! { i32 }
+impl_dafnyint_from! { i64 }
+impl_dafnyint_from! { i128 }
+impl_dafnyint_from! { usize }
diff --git a/releases/rust/db_esdk/dafny_runtime_rust/src/lib.rs b/releases/rust/db_esdk/dafny_runtime_rust/src/lib.rs
index 1598acc51..f422c8de1 100644
--- a/releases/rust/db_esdk/dafny_runtime_rust/src/lib.rs
+++ b/releases/rust/db_esdk/dafny_runtime_rust/src/lib.rs
@@ -1,9 +1,39 @@
+#![allow(clippy::collapsible_else_if)]
+#![allow(clippy::multiple_bound_locations)]
+#![allow(clippy::missing_safety_doc)]
+#![allow(clippy::too_many_arguments)]
+#![allow(clippy::clone_on_copy)]
+#![warn(
+    absolute_paths_not_starting_with_crate,
+    explicit_outlives_requirements,
+    deprecated_in_future,
+    keyword_idents,
+    let_underscore_drop,
+    macro_use_extern_crate,
+    // missing_debug_implementations,
+    non_ascii_idents,
+    noop_method_call,
+    rust_2021_incompatible_closure_captures,
+    rust_2021_incompatible_or_patterns,
+    rust_2021_prefixes_incompatible_syntax,
+    rust_2021_prelude_collisions,
+    rust_2018_idioms,
+    single_use_lifetimes,
+    trivial_numeric_casts,
+    unit_bindings,
+    unreachable_pub,
+    unsafe_op_in_unsafe_fn,
+    unused_extern_crates,
+    unused_lifetimes,
+    unused_qualifications,
+)]
+
 #[cfg(test)]
 mod tests;
 
 mod system;
 pub use mem::MaybeUninit;
-use num::{bigint::ParseBigIntError, Integer, Num, One, Signed};
+use num::{One, Signed};
 pub use once_cell::unsync::Lazy;
 use std::{
     borrow::Borrow,
@@ -15,11 +45,21 @@ use std::{
     fmt::{Debug, Display, Formatter},
     hash::{Hash, Hasher},
     mem,
-    ops::{Add, Deref, Div, Fn, Mul, Neg, Rem, Sub},
+    ops::{Add, Deref, Fn, Sub},
     ptr::NonNull,
     vec::Vec,
 };
 
+#[cfg(not(feature = "small-int"))]
+mod big_int;
+#[cfg(not(feature = "small-int"))]
+pub use big_int::*;
+
+#[cfg(feature = "small-int")]
+mod small_int;
+#[cfg(feature = "small-int")]
+pub use small_int::*;
+
 #[cfg(not(feature = "sync"))]
 pub use ::std::{
     cell::RefCell,
@@ -32,8 +72,6 @@ pub use ::std::sync::{Arc as Rc, Mutex as RefCell, Weak};
 pub use system::*;
 
 pub use itertools;
-pub use num::bigint::BigInt;
-pub use num::rational::BigRational;
 pub use num::FromPrimitive;
 pub use num::NumCast;
 pub use num::ToPrimitive;
@@ -113,9 +151,6 @@ pub mod dafny_runtime_conversions {
     pub type DafnyChar = crate::DafnyChar;
     pub type DafnyCharUTF16 = crate::DafnyCharUTF16;
 
-    use num::BigInt;
-    use num::ToPrimitive;
-
     use ::std::collections::HashMap;
     use ::std::collections::HashSet;
     use ::std::hash::Hash;
@@ -136,8 +171,8 @@ pub mod dafny_runtime_conversions {
         pub fn dafny_class_to_boxed_struct<T: Clone>(ptr: DafnyClass<T>) -> Box<T> {
             Box::new(dafny_class_to_struct(ptr))
         }
-        pub unsafe fn dafny_class_to_rc_struct<T: Clone + ?Sized>(ptr: DafnyClass<T>) -> Rc<T> {
-            crate::rcmut::to_rc(ptr.0.unwrap())
+        pub unsafe fn dafny_class_to_rc_struct<T: Clone>(ptr: DafnyClass<T>) -> Rc<T> {
+            unsafe { crate::rcmut::to_rc(ptr.0.unwrap()) }
         }
         pub fn struct_to_dafny_class<T>(t: T) -> DafnyClass<T> {
             crate::Object::new(t)
@@ -146,7 +181,7 @@ pub mod dafny_runtime_conversions {
             struct_to_dafny_class(*t)
         }
         pub unsafe fn rc_struct_to_dafny_class<T: ?Sized>(t: Rc<T>) -> DafnyClass<T> {
-            crate::Object::from_rc(t)
+            unsafe { crate::Object::from_rc(t) }
         }
         // Conversions to and from Dafny arrays. They all take ownership
         pub unsafe fn dafny_array_to_vec<T: Clone>(ptr: DafnyArray<T>) -> Vec<T> {
@@ -169,10 +204,10 @@ pub mod dafny_runtime_conversions {
         pub type DafnyArray3<T> = crate::Ptr<crate::Array3<T>>;
         // Conversion to and from Dafny reference-counted classes. All these methods take ownership of the class.
         pub unsafe fn dafny_class_to_struct<T: Clone>(ptr: DafnyClass<T>) -> T {
-            *dafny_class_to_boxed_struct(ptr)
+            unsafe { *dafny_class_to_boxed_struct(ptr) }
         }
         pub unsafe fn dafny_class_to_boxed_struct<T: Clone>(ptr: DafnyClass<T>) -> Box<T> {
-            Box::from_raw(crate::Ptr::into_raw(ptr))
+            unsafe { Box::from_raw(crate::Ptr::into_raw(ptr)) }
         }
         pub fn struct_to_dafny_class<T>(t: T) -> DafnyClass<T> {
             boxed_struct_to_dafny_class(Box::new(t))
@@ -188,16 +223,7 @@ pub mod dafny_runtime_conversions {
             crate::Ptr::from_box(array.into_boxed_slice())
         }
         pub unsafe fn dafny_array2_to_vec<T: Clone>(ptr: DafnyArray2<T>) -> Vec<Vec<T>> {
-            Box::from_raw(crate::Ptr::into_raw(ptr)).to_vec()
-        }
-    }
-
-    pub fn dafny_int_to_bigint(i: &DafnyInt) -> BigInt {
-        i.data.as_ref().clone()
-    }
-    pub fn bigint_to_dafny_int(i: &BigInt) -> DafnyInt {
-        DafnyInt {
-            data: Rc::new(i.clone()),
+            unsafe { Box::from_raw(crate::Ptr::into_raw(ptr)).to_vec() }
         }
     }
 
@@ -207,7 +233,7 @@ pub mod dafny_runtime_conversions {
     {
         let mut array: Vec<T> = Vec::with_capacity(s.cardinality_usize());
         DafnySequence::<T>::append_recursive(&mut array, s);
-        array.iter().map(|x| elem_converter(x)).collect()
+        array.iter().map(elem_converter).collect()
     }
 
     // Used for external conversions
@@ -261,7 +287,7 @@ pub mod dafny_runtime_conversions {
         type DafnyString = Sequence<DafnyChar>;
 
         pub fn string_to_dafny_string(s: &str) -> DafnyString {
-            Sequence::from_array_owned(s.chars().map(|v| crate::DafnyChar(v)).collect())
+            Sequence::from_array_owned(s.chars().map(crate::DafnyChar).collect())
         }
         pub fn dafny_string_to_string(s: &DafnyString) -> String {
             let characters = s.to_array();
@@ -277,7 +303,7 @@ pub mod dafny_runtime_conversions {
         type DafnyString = Sequence<DafnyCharUTF16>;
 
         pub fn string_to_dafny_string(s: &str) -> DafnyString {
-            Sequence::from_array_owned(s.encode_utf16().map(|v| crate::DafnyCharUTF16(v)).collect())
+            Sequence::from_array_owned(s.encode_utf16().map(crate::DafnyCharUTF16).collect())
         }
         pub fn dafny_string_to_string(s: &DafnyString) -> String {
             let characters = s
@@ -319,8 +345,8 @@ pub mod dafny_runtime_conversions {
         let mut result: Vec<U> = Vec::new();
         for s in ms.data.iter() {
             // Push T as many times as its size
-            for _ in 0..s.1.data.to_usize().unwrap() {
-                result.push(converter(&s.0));
+            for _ in 0..s.1.as_usize() {
+                result.push(converter(s.0));
             }
         }
         result
@@ -331,7 +357,7 @@ pub mod dafny_runtime_conversions {
         T: DafnyTypeEq,
         U: Clone + Eq + Hash,
     {
-        DafnyMultiset::from_iterator(vec.into_iter().map(|u: &U| converter(u)))
+        DafnyMultiset::from_iterator(vec.iter().map(|u: &U| converter(u)))
     }
 }
 
@@ -343,16 +369,7 @@ pub trait DafnyUsize {
 // Dafny integers
 // **************
 
-// Zero-cost abstraction over a Rc<BigInt>
-#[derive(Clone)]
-pub struct DafnyInt {
-    data: Rc<BigInt>,
-}
-
 impl DafnyInt {
-    pub fn new(data: Rc<BigInt>) -> DafnyInt {
-        DafnyInt { data }
-    }
     pub fn as_usize(&self) -> usize {
         self.to_usize().unwrap()
     }
@@ -364,12 +381,6 @@ impl DafnyUsize for DafnyInt {
     }
 }
 
-impl AsRef<BigInt> for DafnyInt {
-    fn as_ref(&self) -> &BigInt {
-        &self.data
-    }
-}
-
 // truncate_u(x, u64)
 // = <DafnyInt as ToPrimitive>::to_u128(&x).unwrap() as u64;
 #[macro_export]
@@ -379,309 +390,20 @@ macro_rules! truncate {
     };
 }
 
-impl Into<u8> for DafnyInt {
-    fn into(self) -> u8 {
-        self.data.to_u8().unwrap()
-    }
-}
-impl Into<u16> for DafnyInt {
-    fn into(self) -> u16 {
-        self.data.to_u16().unwrap()
-    }
-}
-impl Into<u32> for DafnyInt {
-    fn into(self) -> u32 {
-        self.data.to_u32().unwrap()
-    }
-}
-impl Into<u64> for DafnyInt {
-    fn into(self) -> u64 {
-        self.data.to_u64().unwrap()
-    }
-}
-impl Into<u128> for DafnyInt {
-    fn into(self) -> u128 {
-        self.data.to_u128().unwrap()
-    }
-}
-impl Into<i8> for DafnyInt {
-    fn into(self) -> i8 {
-        self.data.to_i8().unwrap()
-    }
-}
-impl Into<i16> for DafnyInt {
-    fn into(self) -> i16 {
-        self.data.to_i16().unwrap()
-    }
-}
-impl Into<i32> for DafnyInt {
-    fn into(self) -> i32 {
-        self.data.to_i32().unwrap()
-    }
-}
-impl Into<i64> for DafnyInt {
-    fn into(self) -> i64 {
-        self.data.to_i64().unwrap()
-    }
-}
-impl Into<i128> for DafnyInt {
-    fn into(self) -> i128 {
-        self.data.to_i128().unwrap()
-    }
-}
-impl Into<usize> for DafnyInt {
-    fn into(self) -> usize {
-        self.data.to_usize().unwrap()
-    }
-}
-
-impl ToPrimitive for DafnyInt {
-    fn to_i64(&self) -> Option<i64> {
-        self.data.to_i64()
-    }
-
-    fn to_u64(&self) -> Option<u64> {
-        self.data.to_u64()
-    }
-
-    // Override of functions
-    fn to_u128(&self) -> Option<u128> {
-        self.data.to_u128()
-    }
-
-    fn to_i128(&self) -> Option<i128> {
-        self.data.to_i128()
-    }
-}
-
-impl Default for DafnyInt {
-    fn default() -> Self {
-        DafnyInt::new(Rc::new(BigInt::zero()))
-    }
-}
-
 impl NontrivialDefault for DafnyInt {
     fn nontrivial_default() -> Self {
         Self::default()
     }
 }
 
-impl PartialEq<DafnyInt> for DafnyInt {
-    fn eq(&self, other: &DafnyInt) -> bool {
-        self.data.eq(&other.data)
-    }
-}
-impl Eq for DafnyInt {}
-impl Hash for DafnyInt {
-    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
-        self.data.hash(state);
-    }
-}
-
-impl DafnyPrint for DafnyInt {
-    fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
-        write!(f, "{}", self.data)
-    }
-}
-
-impl ::std::fmt::Debug for DafnyInt {
-    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
-        write!(f, "{}", self.data)
-    }
-}
-
-impl Add<DafnyInt> for DafnyInt {
-    type Output = DafnyInt;
-
-    fn add(self, rhs: DafnyInt) -> Self::Output {
-        DafnyInt {
-            data: Rc::new(self.data.as_ref() + rhs.data.as_ref()),
-        }
-    }
-}
-
-impl Mul<DafnyInt> for DafnyInt {
-    type Output = DafnyInt;
-
-    fn mul(self, rhs: DafnyInt) -> Self::Output {
-        DafnyInt {
-            data: Rc::new(self.data.as_ref() * rhs.data.as_ref()),
-        }
-    }
-}
-
-impl Div<DafnyInt> for DafnyInt {
-    type Output = DafnyInt;
-
-    fn div(self, rhs: DafnyInt) -> Self::Output {
-        DafnyInt {
-            data: Rc::new(self.data.as_ref() / rhs.data.as_ref()),
-        }
-    }
-}
-
-impl Sub<DafnyInt> for DafnyInt {
-    type Output = DafnyInt;
-
-    fn sub(self, rhs: DafnyInt) -> Self::Output {
-        DafnyInt {
-            data: Rc::new(self.data.as_ref() - rhs.data.as_ref()),
-        }
-    }
-}
-impl Rem<DafnyInt> for DafnyInt {
-    type Output = DafnyInt;
-
-    fn rem(self, rhs: DafnyInt) -> Self::Output {
-        DafnyInt {
-            data: Rc::new(self.data.as_ref() % rhs.data.as_ref()),
-        }
-    }
-}
-impl Neg for DafnyInt {
-    type Output = DafnyInt;
-
-    #[inline]
-    fn neg(self) -> Self::Output {
-        DafnyInt {
-            data: Rc::new(-self.data.as_ref()),
-        }
-    }
-}
-impl Zero for DafnyInt {
-    #[inline]
-    fn zero() -> Self {
-        DafnyInt {
-            data: Rc::new(BigInt::zero()),
-        }
-    }
-    #[inline]
-    fn is_zero(&self) -> bool {
-        self.data.is_zero()
-    }
-}
-impl One for DafnyInt {
-    #[inline]
-    fn one() -> Self {
-        DafnyInt {
-            data: Rc::new(BigInt::one()),
-        }
-    }
-}
-impl Num for DafnyInt {
-    type FromStrRadixErr = ParseBigIntError;
-
-    #[inline]
-    fn from_str_radix(s: &str, radix: u32) -> Result<Self, Self::FromStrRadixErr> {
-        Ok(DafnyInt {
-            data: Rc::new(BigInt::from_str_radix(s, radix)?),
-        })
-    }
-}
-impl Ord for DafnyInt {
-    #[inline]
-    fn cmp(&self, other: &Self) -> Ordering {
-        self.data.cmp(&other.data)
-    }
-}
-impl Signed for DafnyInt {
-    #[inline]
-    fn abs(&self) -> Self {
-        DafnyInt {
-            data: Rc::new(self.data.as_ref().abs()),
-        }
-    }
-
-    #[inline]
-    fn abs_sub(&self, other: &Self) -> Self {
-        DafnyInt {
-            data: Rc::new(self.data.as_ref().abs_sub(other.data.as_ref())),
-        }
-    }
-
-    #[inline]
-    fn signum(&self) -> Self {
-        DafnyInt {
-            data: Rc::new(self.data.as_ref().signum()),
-        }
-    }
-
-    #[inline]
-    fn is_positive(&self) -> bool {
-        self.data.as_ref().is_positive()
-    }
-
-    #[inline]
-    fn is_negative(&self) -> bool {
-        self.data.as_ref().is_negative()
-    }
-}
-
-// Comparison
-impl PartialOrd<DafnyInt> for DafnyInt {
-    #[inline]
-    fn partial_cmp(&self, other: &DafnyInt) -> Option<Ordering> {
-        self.data.partial_cmp(&other.data)
-    }
-}
-
-impl DafnyInt {
-    #[inline]
-    pub fn parse_bytes(number: &[u8], radix: u32) -> DafnyInt {
-        DafnyInt {
-            data: Rc::new(BigInt::parse_bytes(number, radix).unwrap()),
-        }
-    }
-    pub fn from_usize(usize: usize) -> DafnyInt {
-        DafnyInt {
-            data: Rc::new(BigInt::from(usize)),
-        }
-    }
-    pub fn from_i32(i: i32) -> DafnyInt {
-        DafnyInt {
-            data: Rc::new(BigInt::from(i)),
-        }
-    }
-}
-
-macro_rules! impl_dafnyint_from {
-    () => {};
-    ($type:ident) => {
-        impl ::std::convert::From<$type> for $crate::DafnyInt {
-            fn from(n: $type) -> Self {
-                $crate::DafnyInt {
-                    data: $crate::Rc::new(n.into()),
-                }
-            }
-        }
-        impl $crate::DafnyUsize for $type {
-            fn into_usize(self) -> usize {
-                self as usize
-            }
-        }
-    };
-}
-
-impl_dafnyint_from! { u8 }
-impl_dafnyint_from! { u16 }
-impl_dafnyint_from! { u32 }
-impl_dafnyint_from! { u64 }
-impl_dafnyint_from! { u128 }
-impl_dafnyint_from! { i8 }
-impl_dafnyint_from! { i16 }
-impl_dafnyint_from! { i32 }
-impl_dafnyint_from! { i64 }
-impl_dafnyint_from! { i128 }
-impl_dafnyint_from! { usize }
-
-impl<'a> From<&'a [u8]> for DafnyInt {
+impl From<&[u8]> for DafnyInt {
     fn from(number: &[u8]) -> Self {
         DafnyInt::parse_bytes(number, 10)
     }
 }
 
 // Now the same but for &[u8, N] for any kind of such references
-impl<'a, const N: usize> From<&'a [u8; N]> for DafnyInt {
+impl<const N: usize> From<&[u8; N]> for DafnyInt {
     fn from(number: &[u8; N]) -> Self {
         DafnyInt::parse_bytes(number, 10)
     }
@@ -721,7 +443,7 @@ impl<T: DafnyType> Add<&Sequence<T>> for &Sequence<T> {
 }
 
 impl<T: DafnyType + Hash> Hash for Sequence<T> {
-    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
+    fn hash<H: Hasher>(&self, state: &mut H) {
         self.cardinality_usize().hash(state);
         let array = self.to_array();
         // Iterate over the elements
@@ -846,7 +568,7 @@ where
                 // Let's create an array of size length and fill it up recursively
                 // We don't materialize nested arrays because most of the time they are forgotten
                 let mut array: Vec<T> = Vec::with_capacity(*length);
-                Sequence::<T>::append_recursive_safe(&mut array, &None, left, right);
+                Sequence::<T>::append_recursive(&mut array, self);
                 let result = Rc::new(array);
                 #[cfg(not(feature = "sync"))]
                 {
@@ -870,62 +592,95 @@ where
         }
     }
 
-    pub fn append_recursive_safe(
-        array: &mut Vec<T>,
-        cache_borrow: &Option<&Rc<Vec<T>>>,
-        left: &Rc<RefCell<Sequence<T>>>,
-        right: &Rc<RefCell<Sequence<T>>>,
-    ) {
-        if let Some(values) = cache_borrow.as_ref() {
-            for value in values.iter() {
-                array.push(value.clone());
-            }
-            return;
-        }
-        #[cfg(not(feature = "sync"))]
-        {
-            Sequence::<T>::append_recursive(array, &left.as_ref().borrow());
-            Sequence::<T>::append_recursive(array, &right.as_ref().borrow());
-        }
-        #[cfg(feature = "sync")]
-        {
-            let left_guard = left.as_ref().lock().unwrap();
-            let right_guard = right.as_ref().lock().unwrap();
-            Sequence::<T>::append_recursive(array, &left_guard);
-            Sequence::<T>::append_recursive(array, &right_guard);
-        }
-    }
-
-    pub fn append_recursive(array: &mut Vec<T>, this: &Sequence<T>) {
+    pub fn append_simple(array: &mut Vec<T>, this: &Sequence<T>) -> bool {
         match this {
-            Sequence::ArraySequence { values, .. } =>
-            // The length of the elements
-            {
+            Sequence::ArraySequence { values, .. } => {
                 for value in values.iter() {
                     array.push(value.clone());
                 }
+                true
             }
-            Sequence::ConcatSequence {
-                cache: boxed, left, right, ..
-            } =>
-            // Let's create an array of size length and fill it up recursively
-            {
-                #[cfg(feature = "sync")]
-                let into_boxed = boxed.as_ref();
-                #[cfg(feature = "sync")]
-                let into_boxed_borrowed = into_boxed;
-                #[cfg(feature = "sync")]
-                let guard = into_boxed_borrowed.lock().unwrap();
-                #[cfg(feature = "sync")]
-                let borrowed: Option<&Rc<Vec<T>>> = guard.as_ref();
+            _ => false,
+        }
+    }
 
-                #[cfg(not(feature = "sync"))]
-                let into_boxed = boxed.as_ref().clone();
-                #[cfg(not(feature = "sync"))]
-                let into_boxed_borrowed = into_boxed.borrow();
-                #[cfg(not(feature = "sync"))]
-                let borrowed: Option<&Rc<Vec<T>>> = into_boxed_borrowed.as_ref();
-                Self::append_recursive_safe(array, &borrowed, left, right);
+    pub fn append_recursive(array: &mut Vec<T>, this: &Sequence<T>) {
+        let mut this_ptr: *const Sequence<T> = this;
+        loop {
+            // SAFETY: The invariant is that this_ptr is always a pointer to a sub-sequence of the original `this`parameter when following the field name 'right', which are allocated in this scope
+            match unsafe { &*this_ptr } {
+                Sequence::ArraySequence { values, .. } => {
+                    for value in values.iter() {
+                        array.push(value.clone());
+                    }
+                    return;
+                }
+                Sequence::ConcatSequence {
+                    cache: boxed,
+                    left,
+                    right,
+                    ..
+                } =>
+                // Let's create an array of size length and fill it up recursively
+                {
+                    #[cfg(feature = "sync")]
+                    let into_boxed = boxed.as_ref();
+                    #[cfg(feature = "sync")]
+                    let into_boxed_borrowed = into_boxed;
+                    #[cfg(feature = "sync")]
+                    let guard = into_boxed_borrowed.lock().unwrap();
+                    #[cfg(feature = "sync")]
+                    let borrowed: Option<&Rc<Vec<T>>> = guard.as_ref();
+
+                    #[cfg(not(feature = "sync"))]
+                    let into_boxed = boxed.as_ref().clone();
+                    #[cfg(not(feature = "sync"))]
+                    let into_boxed_borrowed = into_boxed.borrow();
+                    #[cfg(not(feature = "sync"))]
+                    let borrowed: Option<&Rc<Vec<T>>> = into_boxed_borrowed.as_ref();
+                    if let Some(values) = borrowed.as_ref() {
+                        for value in values.iter() {
+                            array.push(value.clone());
+                        }
+                        return;
+                    }
+                    #[cfg(not(feature = "sync"))]
+                    {
+                        let left_empty = left.as_ref().borrow().cardinality_usize() == 0;
+                        let right_empty = right.as_ref().borrow().cardinality_usize() == 0;
+                        if left_empty && right_empty {
+                            return;
+                        } else if left_empty {
+                            this_ptr = right.as_ref().as_ptr();
+                        } else if right_empty {
+                            this_ptr = left.as_ref().as_ptr();
+                        } else {
+                            if !Sequence::<T>::append_simple(array, &left.as_ref().borrow()) {
+                                Sequence::<T>::append_recursive(array, &left.as_ref().borrow());
+                            }
+                            this_ptr = right.as_ref().as_ptr();
+                        }
+                    }
+                    #[cfg(feature = "sync")]
+                    {
+                        let left_guard = left.as_ref().lock().unwrap();
+                        let right_guard = right.as_ref().lock().unwrap();
+                        let left_empty: bool = left_guard.cardinality_usize() == 0;
+                        let right_empty: bool = right_guard.cardinality_usize() == 0;
+                        if left_empty && right_empty {
+                            return;
+                        } else if left_empty {
+                            this_ptr = right_guard.deref();
+                        } else if right_empty {
+                            this_ptr = left_guard.deref();
+                        } else {
+                            if !Sequence::<T>::append_simple(array, &left_guard) {
+                                Sequence::<T>::append_recursive(array, &left_guard);
+                            }
+                            this_ptr = right_guard.deref();
+                        }
+                    }
+                }
             }
         }
     }
@@ -949,25 +704,22 @@ where
     }
 
     pub fn slice(&self, start: &DafnyInt, end: &DafnyInt) -> Sequence<T> {
-        let start_index = start.data.as_ref().to_usize().unwrap();
-        let end_index = end.data.as_ref().to_usize().unwrap();
-        let new_data = Sequence::from_array_owned(self.to_array()[start_index..end_index].to_vec());
-        new_data
+        let start_index = start.as_usize();
+        let end_index = end.as_usize();
+        Sequence::from_array_owned(self.to_array()[start_index..end_index].to_vec())
     }
     pub fn take(&self, end: &DafnyInt) -> Sequence<T> {
-        let end_index = end.data.as_ref().to_usize().unwrap();
-        let new_data = Sequence::from_array_owned(self.to_array()[..end_index].to_vec());
-        new_data
+        let end_index = end.as_usize();
+        Sequence::from_array_owned(self.to_array()[..end_index].to_vec())
     }
     pub fn drop(&self, start: &DafnyInt) -> Sequence<T> {
-        let start_index = start.data.as_ref().to_usize().unwrap();
-        let new_data = Sequence::from_array_owned(self.to_array()[start_index..].to_vec());
-        new_data
+        let start_index = start.as_usize();
+        Sequence::from_array_owned(self.to_array()[start_index..].to_vec())
     }
 
     pub fn update_index(&self, index: &DafnyInt, value: &T) -> Self {
         let mut result = self.to_array().as_ref().clone();
-        result[index.data.to_usize().unwrap()] = value.clone();
+        result[index.as_usize()] = value.clone();
         Sequence::from_array_owned(result)
     }
 
@@ -976,7 +728,7 @@ where
     }
 
     pub fn get(&self, index: &DafnyInt) -> T {
-        self.get_usize(index.data.to_usize().unwrap())
+        self.get_usize(index.as_usize())
     }
     pub fn iter(&self) -> SequenceIter<T> {
         SequenceIter {
@@ -1042,12 +794,10 @@ where
         if other.cardinality_usize() != values.len() {
             return false;
         }
-        let mut i: usize = 0;
-        for value in values.iter() {
+        for (i, value) in values.iter().enumerate() {
             if value != &other.get_usize(i) {
                 return false;
             }
-            i += 1;
         }
         true
     }
@@ -1158,7 +908,7 @@ where
                 return false;
             }
         }
-        return true;
+        true
     }
 }
 
@@ -1194,7 +944,7 @@ impl<K: DafnyTypeEq, V: DafnyType> Map<K, V> {
         converter_v: fn(&V) -> V2,
     ) -> HashMap<K2, V2>
     where
-        K2: Eq + std::hash::Hash,
+        K2: Eq + Hash,
         V2: Clone,
     {
         let mut result: HashMap<K2, V2> = HashMap::new();
@@ -1321,12 +1071,22 @@ impl<K: DafnyTypeEq> Map<K, DafnyInt> {
 
 pub struct MapBuilder<K, V>
 where
-    K: Clone + Eq + std::hash::Hash,
+    K: Clone + Eq + Hash,
     V: Clone,
 {
     data: HashMap<K, V>,
 }
 
+impl<K, V> Default for MapBuilder<K, V>
+where
+    K: DafnyTypeEq,
+    V: DafnyType,
+{
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
 impl<K, V> MapBuilder<K, V>
 where
     K: DafnyTypeEq,
@@ -1464,7 +1224,7 @@ impl<V: DafnyTypeEq> Set<V> {
         Self::from_hashset_owned(HashSet::new())
     }
     pub fn from_array(array: &Vec<V>) -> Set<V> {
-        Self::from_iterator(array.iter().map(|v| v.clone()))
+        Self::from_iterator(array.iter().cloned())
     }
     pub fn from_iterator<I>(data: I) -> Set<V>
     where
@@ -1493,7 +1253,7 @@ impl<V: DafnyTypeEq> Set<V> {
     pub fn contains(&self, value: &V) -> bool {
         self.data.contains(value)
     }
-    pub fn merge(self: &Self, other: &Set<V>) -> Set<V> {
+    pub fn merge(&self, other: &Set<V>) -> Set<V> {
         if self.cardinality_usize() == 0 {
             return other.clone();
         }
@@ -1510,7 +1270,7 @@ impl<V: DafnyTypeEq> Set<V> {
         Set::from_hashset_owned(result)
     }
 
-    pub fn intersect(self: &Self, other: &Set<V>) -> Set<V> {
+    pub fn intersect(&self, other: &Set<V>) -> Set<V> {
         if self.cardinality_usize() == 0 {
             return self.clone();
         }
@@ -1586,7 +1346,7 @@ impl<V: DafnyTypeEq> Set<V> {
         true
     }
 
-    pub fn elements(self: &Self) -> Set<V> {
+    pub fn elements(&self) -> Set<V> {
         self.clone()
     }
 
@@ -1605,11 +1365,17 @@ impl<V: DafnyTypeEq> Set<V> {
 
 pub struct SetBuilder<T>
 where
-    T: Clone + Eq + std::hash::Hash,
+    T: Clone + Eq + Hash,
 {
     data: HashMap<T, bool>,
 }
 
+impl<T: DafnyTypeEq> Default for SetBuilder<T> {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
 impl<T: DafnyTypeEq> SetBuilder<T> {
     pub fn new() -> SetBuilder<T> {
         SetBuilder {
@@ -1686,7 +1452,7 @@ impl<V: DafnyTypeEq> Multiset<V> {
         Self::from_hashmap_owned(map.clone())
     }
     pub fn from_array(data: &Vec<V>) -> Multiset<V> {
-        Self::from_iterator(data.iter().map(|x| x.clone()))
+        Self::from_iterator(data.iter().cloned())
     }
     pub fn from_iterator<I>(data: I) -> Multiset<V>
     where
@@ -1705,11 +1471,11 @@ impl<V: DafnyTypeEq> Multiset<V> {
         }
     }
     pub fn from_set(set: &Set<V>) -> Multiset<V> {
-        Self::from_iterator(set.data.iter().map(|v| v.clone()))
+        Self::from_iterator(set.data.iter().cloned())
     }
 
     pub fn cardinality_usize(&self) -> SizeT {
-        self.size.data.to_usize().unwrap()
+        self.size.as_usize()
     }
     pub fn cardinality(&self) -> DafnyInt {
         self.size.clone()
@@ -1828,7 +1594,7 @@ impl<V: DafnyTypeEq> Multiset<V> {
     pub fn iter(&self) -> impl Iterator<Item = V> + '_ {
         self.data
             .iter()
-            .flat_map(|(k, &ref v)| ::std::iter::repeat(k).take(v.clone().as_usize()))
+            .flat_map(|(k, v)| ::std::iter::repeat(k).take(v.clone().as_usize()))
             .cloned()
     }
 }
@@ -1883,7 +1649,7 @@ impl<V: DafnyTypeEq> DafnyPrint for Multiset<V> {
         f.write_str("multiset{")?;
         let mut first = true;
         for value in self.data.iter() {
-            for _count in 0..value.1.data.to_usize().unwrap() {
+            for _count in 0..value.1.as_usize() {
                 if !first {
                     f.write_str(", ")?;
                 }
@@ -1925,10 +1691,6 @@ impl<V: DafnyTypeEq> Hash for Multiset<V> {
     }
 }
 
-pub fn dafny_rational_to_int(r: &BigRational) -> BigInt {
-    euclidian_division(r.numer().clone(), r.denom().clone())
-}
-
 pub fn euclidian_division<A: Signed + Zero + One + Clone + PartialEq>(a: A, b: A) -> A {
     if !a.is_negative() {
         if !b.is_negative() {
@@ -2077,7 +1839,7 @@ impl<A: DafnyPrint> DafnyPrint for LazyFieldWrapper<A> {
 // Convert the DafnyPrint above into a macro so that we can create it for functions of any input arity
 macro_rules! dafny_print_function {
     ($($n:tt)*) => {
-        impl <B, $($n),*> $crate::DafnyPrint for $crate::Rc<dyn ::std::ops::Fn($($n),*) -> B + Send + Sync> {
+        impl <B, $($n),*> $crate::DafnyPrint for $crate::Rc<dyn ::std::ops::Fn($(&$n),*) -> B + Send + Sync> {
             fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result {
                 write!(f, "<function>")
             }
@@ -2088,7 +1850,7 @@ macro_rules! dafny_print_function {
 // Convert the DafnyPrint above into a macro so that we can create it for functions of any input arity
 macro_rules! dafny_print_function {
     ($($n:tt)*) => {
-        impl <B, $($n),*> $crate::DafnyPrint for $crate::Rc<dyn ::std::ops::Fn($($n),*) -> B> {
+        impl <B, $($n),*> $crate::DafnyPrint for $crate::Rc<dyn ::std::ops::Fn($(&$n),*) -> B> {
             fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result {
                 write!(f, "<function>")
             }
@@ -2210,7 +1972,7 @@ impl Default for DafnyCharUTF16 {
 impl DafnyPrint for DafnyCharUTF16 {
     #[inline]
     fn fmt_print(&self, f: &mut Formatter<'_>, in_seq: bool) -> std::fmt::Result {
-        let real_char = char::decode_utf16(vec![self.clone()].iter().map(|v| v.0))
+        let real_char = char::decode_utf16([*self].iter().map(|v| v.0))
             .map(|r| r.map_err(|e| e.unpaired_surrogate()))
             .collect::<Vec<_>>()[0];
         let rendered_char = match real_char {
@@ -2348,85 +2110,6 @@ impl<T: DafnyPrint> DafnyPrint for Option<T> {
     }
 }
 
-impl DafnyPrint for BigInt {
-    fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
-        write!(f, "{}", self)
-    }
-}
-
-fn divides_a_power_of_10(mut i: BigInt) -> (bool, BigInt, usize) {
-    let one: BigInt = One::one();
-
-    let mut factor = one.clone();
-    let mut log10 = 0;
-
-    let zero = Zero::zero();
-    let ten = BigInt::from_i32(10).unwrap();
-
-    if i <= zero {
-        return (false, factor, log10);
-    }
-
-    while i.is_multiple_of(&ten) {
-        i /= BigInt::from_i32(10).unwrap();
-        log10 += 1;
-    }
-
-    let two = BigInt::from_i32(2).unwrap();
-    let five = BigInt::from_i32(5).unwrap();
-
-    while i.is_multiple_of(&five) {
-        i /= &five;
-        factor *= &two;
-        log10 += 1;
-    }
-
-    while i.is_multiple_of(&two) {
-        i /= &two;
-        factor *= &two;
-        log10 += 1;
-    }
-
-    (i == one, factor, log10)
-}
-
-impl DafnyPrint for BigRational {
-    fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
-        if self.denom() == &One::one() || self.numer() == &Zero::zero() {
-            write!(f, "{}.0", self.numer())
-        } else {
-            let (divides, factor, log10) = divides_a_power_of_10(self.denom().clone());
-            if divides {
-                let mut num = self.numer().clone();
-                num *= factor;
-
-                if num.is_negative() {
-                    write!(f, "-")?;
-                    num = -num;
-                }
-
-                let digits = num.to_string();
-
-                if log10 < digits.len() {
-                    let digit_count = digits.len() - log10;
-                    write!(f, "{}", &digits[..digit_count])?;
-                    write!(f, ".")?;
-                    write!(f, "{}", &digits[digit_count..])
-                } else {
-                    let z = log10 - digits.len();
-                    write!(f, "0.")?;
-                    for _ in 0..z {
-                        write!(f, "0")?;
-                    }
-                    write!(f, "{}", digits)
-                }
-            } else {
-                write!(f, "({}.0 / {}.0)", self.numer(), self.denom())
-            }
-        }
-    }
-}
-
 impl<T: ?Sized + DafnyPrint> DafnyPrint for Rc<T> {
     fn fmt_print(&self, f: &mut Formatter<'_>, in_seq: bool) -> std::fmt::Result {
         self.as_ref().fmt_print(f, in_seq)
@@ -2483,16 +2166,11 @@ impl<T: DafnyPrint> DafnyPrint for HashSet<T> {
     fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
         write!(f, "{{")?;
 
-        let mut i = 0;
-
-        for item in self.iter() {
+        for (i, item) in self.iter().enumerate() {
             if i > 0 {
                 write!(f, ", ")?;
             }
-
             item.fmt_print(f, false)?;
-
-            i += 1;
         }
 
         write!(f, "}}")
@@ -2507,13 +2185,11 @@ pub fn char_lt(left: char, right: char) -> bool {
 }
 
 pub fn string_of(s: &str) -> DafnyString {
-    s.chars()
-        .map(|v| DafnyChar(v))
-        .collect::<Sequence<DafnyChar>>()
+    s.chars().map(DafnyChar).collect::<Sequence<DafnyChar>>()
 }
 
 pub fn string_utf16_of(s: &str) -> DafnyStringUTF16 {
-    Sequence::from_array_owned(s.encode_utf16().map(|v| DafnyCharUTF16(v)).collect())
+    Sequence::from_array_owned(s.encode_utf16().map(DafnyCharUTF16).collect())
 }
 
 macro_rules! impl_tuple_print {
@@ -3104,7 +2780,7 @@ pub mod array {
     }
 
     pub fn initialize<T>(n: &DafnyInt, initializer: Rc<dyn Fn(&DafnyInt) -> T>) -> Ptr<[T]> {
-        super::Ptr::from_box(initialize_box(n, initializer))
+        Ptr::from_box(initialize_box(n, initializer))
     }
 
     pub fn initialize_box<T>(n: &DafnyInt, initializer: Rc<dyn Fn(&DafnyInt) -> T>) -> Box<[T]> {
@@ -3164,7 +2840,7 @@ pub fn deallocate<T: ?Sized>(pointer: Ptr<T>) {
     unsafe {
         // Takes ownership of the reference,
         // so that it's deallocated at the end of the method
-        let _ = Box::from_raw(pointer.into_raw());
+        drop(Box::from_raw(pointer.into_raw()));
     }
 }
 
@@ -3421,7 +3097,7 @@ impl<T: ?Sized> Default for Ptr<T> {
 }
 
 impl<T: ?Sized> Debug for Ptr<T> {
-    fn fmt(&self, f: &mut Formatter) -> std::fmt::Result {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
         self.fmt_print(f, false)
     }
 }
@@ -3452,7 +3128,7 @@ impl<T: ?Sized, U: ?Sized> PartialEq<Ptr<U>> for Ptr<T> {
     }
 }
 
-impl<T: ?Sized> std::hash::Hash for Ptr<T> {
+impl<T: ?Sized> Hash for Ptr<T> {
     fn hash<H: Hasher>(&self, state: &mut H) {
         if !self.is_null() {
             (read!(self.clone()) as *const T as *const ()).hash(state);
@@ -3506,7 +3182,7 @@ pub struct Object<T: ?Sized>(pub Option<rcmut::RcMut<T>>);
 impl<T: ?Sized> Object<T> {
     // For safety, it requires the Rc to have been created with Rc::new()
     pub unsafe fn from_rc(rc: Rc<T>) -> Object<T> {
-        Object(Some(rcmut::from_rc(rc)))
+        unsafe { Object(Some(rcmut::from_rc(rc))) }
     }
     pub fn null() -> Object<T> {
         Object(None)
@@ -3543,7 +3219,7 @@ impl<T: ?Sized> Default for Object<T> {
 }
 
 impl<T: ?Sized + UpcastObject<DynAny>> Debug for Object<T> {
-    fn fmt(&self, f: &mut Formatter) -> std::fmt::Result {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
         self.fmt_print(f, false)
     }
 }
@@ -3588,7 +3264,7 @@ impl<T: ?Sized, U: ?Sized> PartialEq<Object<U>> for Object<T> {
     }
 }
 
-impl<T: ?Sized> std::hash::Hash for Object<T> {
+impl<T: ?Sized> Hash for Object<T> {
     fn hash<H: Hasher>(&self, state: &mut H) {
         if let Some(p) = &self.0 {
             (p.as_ref().get() as *const ()).hash(state);
@@ -3600,12 +3276,12 @@ impl<T: ?Sized> std::hash::Hash for Object<T> {
 
 impl<T: ?Sized> AsMut<T> for Object<T> {
     fn as_mut(&mut self) -> &mut T {
-        unsafe { &mut *(&self.0).as_ref().unwrap_unchecked().as_ref().get() }
+        unsafe { &mut *(self.0).as_ref().unwrap_unchecked().as_ref().get() }
     }
 }
 impl<T: ?Sized> AsRef<T> for Object<T> {
     fn as_ref(&self) -> &T {
-        unsafe { &*(&self.0).as_ref().unwrap_unchecked().as_ref().get() }
+        unsafe { &*(self.0).as_ref().unwrap_unchecked().as_ref().get() }
     }
 }
 
@@ -3629,7 +3305,7 @@ impl<T: ?Sized> Object<T> {
         // it will will correctly rebuilt the Rc
         let rebuilt = ::std::hint::black_box(unsafe { Rc::from_raw(pt) });
         let previous_strong_count = ::std::hint::black_box(Rc::strong_count(&rebuilt));
-        ::std::hint::black_box(crate::increment_strong_count(pt));
+        ::std::hint::black_box(increment_strong_count(pt));
         let new_strong_count = ::std::hint::black_box(Rc::strong_count(&rebuilt));
         assert_eq!(new_strong_count, previous_strong_count + 1); // Will panic if not
         Object(Some(rebuilt))
@@ -3835,23 +3511,23 @@ pub mod rcmut {
     use ::std::mem::{self, MaybeUninit};
 
     pub fn array_object_from_rc<T>(data: Rc<[T]>) -> crate::Object<[T]> {
-        crate::Object(Some(unsafe { crate::rcmut::from_rc(data) }))
+        crate::Object(Some(unsafe { from_rc(data) }))
     }
     pub fn array_object_from_box<T>(data: Box<[T]>) -> crate::Object<[T]> {
         let data: Rc<[T]> = data.into();
-        crate::Object(Some(unsafe { crate::rcmut::from_rc(data) }))
+        crate::Object(Some(unsafe { from_rc(data) }))
     }
     pub struct Array<T> {
         pub data: Box<[T]>,
     }
     impl<T> Array<T> {
         pub fn new(data: Box<[T]>) -> crate::Object<Array<T>> {
-            crate::Object(Some(crate::rcmut::new(Array { data })))
+            crate::Object(Some(new(Array { data })))
         }
 
         pub fn placebos_usize_object(length: usize) -> crate::Object<Array<MaybeUninit<T>>> {
             let x = crate::array::placebos_box_usize::<T>(length);
-            crate::rcmut::Array::<MaybeUninit<T>>::new(x)
+            Array::<MaybeUninit<T>>::new(x)
         }
     }
     /// A reference counted smart pointer with unrestricted mutability.
@@ -3863,51 +3539,51 @@ pub mod rcmut {
     }
     /// Retrieve the inner Rc as a reference.
     pub unsafe fn from<T>(value: Box<T>) -> RcMut<T> {
-        mem::transmute(Rc::new(*value))
+        unsafe { mem::transmute(Rc::new(*value)) }
     }
 
     pub unsafe fn from_rc<T: ?Sized>(value: Rc<T>) -> RcMut<T> {
-        mem::transmute(value)
+        unsafe { mem::transmute(value) }
     }
 
     pub unsafe fn as_rc<T: ?Sized>(this: &RcMut<T>) -> &Rc<T> {
-        mem::transmute(this)
+        unsafe { mem::transmute(this) }
     }
     pub unsafe fn to_rc<T: ?Sized>(this: RcMut<T>) -> Rc<T> {
-        mem::transmute(this)
+        unsafe { mem::transmute(this) }
     }
 
     /// Retrieve the inner Rc as a mutable reference.
     pub unsafe fn as_rc_mut<T: ?Sized>(this: &mut RcMut<T>) -> &mut Rc<T> {
-        mem::transmute(this)
+        unsafe { mem::transmute(this) }
     }
 
     /// Get a reference to the value.
     #[inline]
     pub unsafe fn borrow<T: ?Sized>(this: &RcMut<T>) -> &T {
-        mem::transmute(this.get())
+        unsafe { &*this.get() }
     }
 
     /// Get a mutable reference to the value.
     #[inline]
     pub unsafe fn borrow_mut<T: ?Sized>(this: &mut RcMut<T>) -> &mut T {
-        mem::transmute(this.get())
+        unsafe { &mut *this.get() }
     }
 
     #[cfg(feature = "sync")]
     pub unsafe fn downcast<T: 'static + Send + Sync>(
         this: RcMut<crate::DynAny>,
     ) -> Option<RcMut<T>> {
-        let t: Rc<crate::DynAny> = to_rc(this);
+        let t: Rc<crate::DynAny> = unsafe { to_rc(this) };
         let t: Rc<T> = Rc::downcast::<T>(t).ok()?;
-        mem::transmute(t)
+        unsafe { mem::transmute(t) }
     }
 
     #[cfg(not(feature = "sync"))]
     pub unsafe fn downcast<T: 'static>(this: RcMut<crate::DynAny>) -> Option<RcMut<T>> {
-        let t: Rc<crate::DynAny> = to_rc(this);
+        let t: Rc<crate::DynAny> = unsafe { to_rc(this) };
         let t: Rc<T> = Rc::downcast::<T>(t).ok()?;
-        mem::transmute(t)
+        unsafe { mem::transmute(t) }
     }
 }
 
@@ -3989,9 +3665,9 @@ where
 }
 pub fn upcast_box_box<A: ?Sized, B: ?Sized>() -> Rc<impl Fn(Box<A>) -> Box<B>>
 where
-    Box<A>: UpcastBox<B>,
+    A: UpcastBox<B>,
 {
-    Rc::new(|x: Box<A>| UpcastBox::upcast(&x))
+    Rc::new(|x: Box<A>| UpcastBox::upcast(x.as_ref()))
 }
 
 pub fn upcast_id<A>() -> Rc<impl Fn(A) -> A> {
@@ -4039,6 +3715,25 @@ pub trait UpcastBox<T: ?Sized> {
     fn upcast(&self) -> Box<T>;
 }
 
+impl<T: ?Sized, U> UpcastBox<T> for Rc<U>
+where
+    U: UpcastBox<T>,
+{
+    fn upcast(&self) -> Box<T> {
+        UpcastBox::upcast(AsRef::as_ref(self))
+    }
+}
+
+pub trait AnyRef {
+    fn as_any_ref(&self) -> &dyn Any;
+}
+
+impl<T: 'static> AnyRef for T {
+    fn as_any_ref(&self) -> &dyn Any {
+        self
+    }
+}
+
 #[macro_export]
 macro_rules! Extends {
     ($traitType: tt) => {
diff --git a/releases/rust/db_esdk/dafny_runtime_rust/src/small_int.rs b/releases/rust/db_esdk/dafny_runtime_rust/src/small_int.rs
new file mode 100644
index 000000000..cba1e1a60
--- /dev/null
+++ b/releases/rust/db_esdk/dafny_runtime_rust/src/small_int.rs
@@ -0,0 +1,335 @@
+#![allow(unused_imports)]
+
+use crate::DafnyPrint;
+use crate::Rc;
+use num::FromPrimitive;
+use num::ToPrimitive;
+use num::{bigint::ParseBigIntError, Integer, Num, One, Signed, Zero};
+use std::{
+    clone::Clone,
+    cmp::Ordering,
+    convert::From,
+    fmt::Formatter,
+    hash::Hash,
+    ops::{Add, Div, Mul, Neg, Rem, Sub},
+};
+
+type InternalInt = i128;
+
+#[derive(Clone, Copy)]
+pub struct DafnyInt {
+    data: InternalInt,
+}
+
+const ONE: DafnyInt = DafnyInt { data: 1 };
+const ZERO: DafnyInt = DafnyInt { data: 0 };
+
+impl DafnyInt {
+    pub fn new(data: InternalInt) -> DafnyInt {
+        DafnyInt { data }
+    }
+}
+
+impl AsRef<InternalInt> for DafnyInt {
+    fn as_ref(&self) -> &InternalInt {
+        &self.data
+    }
+}
+
+impl Default for DafnyInt {
+    fn default() -> Self {
+        ZERO
+    }
+}
+
+impl Zero for DafnyInt {
+    #[inline]
+    fn zero() -> Self {
+        ZERO
+    }
+    #[inline]
+    fn is_zero(&self) -> bool {
+        self.data == 0
+    }
+}
+impl One for DafnyInt {
+    #[inline]
+    fn one() -> Self {
+        ONE
+    }
+}
+
+impl Num for DafnyInt {
+    type FromStrRadixErr = std::num::ParseIntError;
+
+    #[inline]
+    fn from_str_radix(s: &str, radix: u32) -> Result<Self, std::num::ParseIntError> {
+        let x = InternalInt::from_str_radix(s, radix)?;
+        Ok(DafnyInt::new(x))
+    }
+}
+
+impl Ord for DafnyInt {
+    #[inline]
+    fn cmp(&self, other: &Self) -> Ordering {
+        self.data.cmp(&other.data)
+    }
+}
+impl Signed for DafnyInt {
+    #[inline]
+    fn abs(&self) -> Self {
+        DafnyInt {
+            data: self.data.abs(),
+        }
+    }
+
+    #[inline]
+    fn abs_sub(&self, other: &Self) -> Self {
+        DafnyInt {
+            data: self.data.abs_sub(&other.data),
+        }
+    }
+
+    #[inline]
+    fn signum(&self) -> Self {
+        DafnyInt {
+            data: self.data.signum(),
+        }
+    }
+
+    #[inline]
+    fn is_positive(&self) -> bool {
+        self.data.is_positive()
+    }
+
+    #[inline]
+    fn is_negative(&self) -> bool {
+        self.data.is_negative()
+    }
+}
+
+// Comparison
+impl PartialOrd<DafnyInt> for DafnyInt {
+    #[inline]
+    fn partial_cmp(&self, other: &DafnyInt) -> Option<Ordering> {
+        Some(self.cmp(other))
+    }
+}
+
+impl DafnyInt {
+    #[inline]
+    pub fn parse_bytes(number: &[u8], radix: u32) -> DafnyInt {
+        let x = InternalInt::from_str_radix(std::str::from_utf8(number).unwrap(), radix).unwrap();
+        DafnyInt::new(x)
+    }
+    pub fn from_usize(usize: usize) -> DafnyInt {
+        DafnyInt {
+            data: usize as InternalInt,
+        }
+    }
+    pub fn from_i32(i: i32) -> DafnyInt {
+        DafnyInt {
+            data: i as InternalInt,
+        }
+    }
+}
+
+// impl<const N: usize> From<&[u8; N]> for DafnyInt {
+//     fn from(number: &[u8; N]) -> Self {
+//         DafnyInt::parse_bytes(number, 10)
+//     }
+// }
+
+// impl From<&[u8]> for DafnyInt {
+//     fn from(val: &[u8]) -> DafnyInt {
+//         DafnyInt::parse_bytes(val, 10)
+//     }
+// }
+
+impl From<DafnyInt> for u8 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_u8().unwrap()
+    }
+}
+impl From<DafnyInt> for u16 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_u16().unwrap()
+    }
+}
+impl From<DafnyInt> for u32 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_u32().unwrap()
+    }
+}
+impl From<DafnyInt> for u64 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_u64().unwrap()
+    }
+}
+impl From<DafnyInt> for u128 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_u128().unwrap()
+    }
+}
+impl From<DafnyInt> for i8 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_i8().unwrap()
+    }
+}
+impl From<DafnyInt> for i16 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_i16().unwrap()
+    }
+}
+impl From<DafnyInt> for i32 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_i32().unwrap()
+    }
+}
+impl From<DafnyInt> for i64 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_i64().unwrap()
+    }
+}
+impl From<DafnyInt> for i128 {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_i128().unwrap()
+    }
+}
+impl From<DafnyInt> for usize {
+    fn from(val: DafnyInt) -> Self {
+        val.data.to_usize().unwrap()
+    }
+}
+
+impl ToPrimitive for DafnyInt {
+    fn to_i64(&self) -> Option<i64> {
+        self.data.to_i64()
+    }
+
+    fn to_u64(&self) -> Option<u64> {
+        self.data.to_u64()
+    }
+
+    // Override of functions
+    fn to_u128(&self) -> Option<u128> {
+        self.data.to_u128()
+    }
+
+    fn to_i128(&self) -> Option<i128> {
+        self.data.to_i128()
+    }
+}
+
+impl PartialEq<DafnyInt> for DafnyInt {
+    fn eq(&self, other: &DafnyInt) -> bool {
+        self.data.eq(&other.data)
+    }
+}
+impl Eq for DafnyInt {}
+impl Hash for DafnyInt {
+    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
+        self.data.hash(state);
+    }
+}
+
+impl DafnyPrint for DafnyInt {
+    fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
+        write!(f, "{}", self.data)
+    }
+}
+
+impl ::std::fmt::Debug for DafnyInt {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{}", self.data)
+    }
+}
+
+impl Add<DafnyInt> for DafnyInt {
+    type Output = DafnyInt;
+
+    fn add(self, rhs: DafnyInt) -> Self::Output {
+        DafnyInt {
+            data: self.data + rhs.data,
+        }
+    }
+}
+
+impl Mul<DafnyInt> for DafnyInt {
+    type Output = DafnyInt;
+
+    fn mul(self, rhs: DafnyInt) -> Self::Output {
+        DafnyInt {
+            data: self.data * rhs.data,
+        }
+    }
+}
+
+impl Div<DafnyInt> for DafnyInt {
+    type Output = DafnyInt;
+
+    fn div(self, rhs: DafnyInt) -> Self::Output {
+        DafnyInt {
+            data: self.data / rhs.data,
+        }
+    }
+}
+
+impl Sub<DafnyInt> for DafnyInt {
+    type Output = DafnyInt;
+
+    fn sub(self, rhs: DafnyInt) -> Self::Output {
+        DafnyInt {
+            data: self.data - rhs.data,
+        }
+    }
+}
+impl Rem<DafnyInt> for DafnyInt {
+    type Output = DafnyInt;
+
+    fn rem(self, rhs: DafnyInt) -> Self::Output {
+        DafnyInt {
+            data: self.data % rhs.data,
+        }
+    }
+}
+impl Neg for DafnyInt {
+    type Output = DafnyInt;
+
+    #[inline]
+    fn neg(self) -> Self::Output {
+        DafnyInt { data: -self.data }
+    }
+}
+
+macro_rules! impl_dafnyint_from {
+    () => {};
+    ($type:ident) => {
+        #[allow(trivial_numeric_casts)]
+        impl ::std::convert::From<$type> for $crate::DafnyInt {
+            fn from(n: $type) -> Self {
+                $crate::DafnyInt {
+                    data: n as InternalInt,
+                }
+            }
+        }
+        #[allow(trivial_numeric_casts)]
+        impl $crate::DafnyUsize for $type {
+            fn into_usize(self) -> usize {
+                self as usize
+            }
+        }
+    };
+}
+
+impl_dafnyint_from! { u8 }
+impl_dafnyint_from! { u16 }
+impl_dafnyint_from! { u32 }
+impl_dafnyint_from! { u64 }
+impl_dafnyint_from! { u128 }
+impl_dafnyint_from! { i8 }
+impl_dafnyint_from! { i16 }
+impl_dafnyint_from! { i32 }
+impl_dafnyint_from! { i64 }
+impl_dafnyint_from! { i128 }
+impl_dafnyint_from! { usize }
diff --git a/releases/rust/db_esdk/dafny_runtime_rust/src/system/mod.rs b/releases/rust/db_esdk/dafny_runtime_rust/src/system/mod.rs
index 582b3cc82..13242934e 100644
--- a/releases/rust/db_esdk/dafny_runtime_rust/src/system/mod.rs
+++ b/releases/rust/db_esdk/dafny_runtime_rust/src/system/mod.rs
@@ -12,15 +12,15 @@ pub mod _System {
     #[cfg(feature = "sync")] pub use ::std::sync::{Arc as Rc}; #[cfg(not(feature = "sync"))] pub use ::std::rc::Rc;
     pub use ::std::cmp::Eq;
     pub use ::std::hash::Hash;
+    pub use ::std::cmp::PartialEq;
     pub use ::std::hash::Hasher;
-    pub use ::std::default::Default;
     pub use ::std::convert::AsRef;
     pub use crate::SequenceIter;
     pub use crate::seq;
 
     pub type nat = DafnyInt;
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple2<T0: DafnyType, T1: DafnyType> {
         _T2 {
             _0: T0,
@@ -82,7 +82,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash> PartialEq
+        for Tuple2<T0, T1> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple2::_T2{_0, _1, }, Tuple2::_T2{_0: _2__0, _1: _2__1, }) => {
+                    _0 == _2__0 && _1 == _2__1
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash> Eq
         for Tuple2<T0, T1> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash> Hash
@@ -97,16 +114,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default> Default
-        for Tuple2<T0, T1> {
-        fn default() -> Tuple2<T0, T1> {
-            Tuple2::_T2 {
-                _0: Default::default(),
-                _1: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType> AsRef<Tuple2<T0, T1>>
         for Tuple2<T0, T1> {
         fn as_ref(&self) -> &Self {
@@ -114,7 +121,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple0 {
         _T0 {}
     }
@@ -147,6 +154,23 @@ pub mod _System {
         }
     }
 
+    impl PartialEq
+        for Tuple0 {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple0::_T0{}, Tuple0::_T0{}) => {
+                    true
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
     impl Eq
         for Tuple0 {}
 
@@ -161,13 +185,6 @@ pub mod _System {
         }
     }
 
-    impl Default
-        for Tuple0 {
-        fn default() -> Tuple0 {
-            Tuple0::_T0 {}
-        }
-    }
-
     impl AsRef<Tuple0>
         for Tuple0 {
         fn as_ref(&self) -> &Self {
@@ -175,7 +192,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple1<T0: DafnyType> {
         _T1 {
             _0: T0
@@ -227,7 +244,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash> PartialEq
+        for Tuple1<T0> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple1::_T1{_0, }, Tuple1::_T1{_0: _2__0, }) => {
+                    _0 == _2__0
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash> Eq
         for Tuple1<T0> {}
 
     impl<T0: DafnyType + Hash> Hash
@@ -241,15 +275,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default> Default
-        for Tuple1<T0> {
-        fn default() -> Tuple1<T0> {
-            Tuple1::_T1 {
-                _0: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType> AsRef<Tuple1<T0>>
         for Tuple1<T0> {
         fn as_ref(&self) -> &Self {
@@ -257,7 +282,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple3<T0: DafnyType, T1: DafnyType, T2: DafnyType> {
         _T3 {
             _0: T0,
@@ -329,7 +354,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash> PartialEq
+        for Tuple3<T0, T1, T2> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple3::_T3{_0, _1, _2, }, Tuple3::_T3{_0: _2__0, _1: _2__1, _2: _2__2, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash> Eq
         for Tuple3<T0, T1, T2> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash> Hash
@@ -345,17 +387,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default> Default
-        for Tuple3<T0, T1, T2> {
-        fn default() -> Tuple3<T0, T1, T2> {
-            Tuple3::_T3 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType> AsRef<Tuple3<T0, T1, T2>>
         for Tuple3<T0, T1, T2> {
         fn as_ref(&self) -> &Self {
@@ -363,7 +394,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple4<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType> {
         _T4 {
             _0: T0,
@@ -445,7 +476,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash> PartialEq
+        for Tuple4<T0, T1, T2, T3> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple4::_T4{_0, _1, _2, _3, }, Tuple4::_T4{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash> Eq
         for Tuple4<T0, T1, T2, T3> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash> Hash
@@ -462,18 +510,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default> Default
-        for Tuple4<T0, T1, T2, T3> {
-        fn default() -> Tuple4<T0, T1, T2, T3> {
-            Tuple4::_T4 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType> AsRef<Tuple4<T0, T1, T2, T3>>
         for Tuple4<T0, T1, T2, T3> {
         fn as_ref(&self) -> &Self {
@@ -481,7 +517,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple5<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType> {
         _T5 {
             _0: T0,
@@ -573,7 +609,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash> PartialEq
+        for Tuple5<T0, T1, T2, T3, T4> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple5::_T5{_0, _1, _2, _3, _4, }, Tuple5::_T5{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash> Eq
         for Tuple5<T0, T1, T2, T3, T4> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash> Hash
@@ -591,19 +644,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default> Default
-        for Tuple5<T0, T1, T2, T3, T4> {
-        fn default() -> Tuple5<T0, T1, T2, T3, T4> {
-            Tuple5::_T5 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType> AsRef<Tuple5<T0, T1, T2, T3, T4>>
         for Tuple5<T0, T1, T2, T3, T4> {
         fn as_ref(&self) -> &Self {
@@ -611,7 +651,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple6<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType> {
         _T6 {
             _0: T0,
@@ -713,7 +753,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash> PartialEq
+        for Tuple6<T0, T1, T2, T3, T4, T5> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple6::_T6{_0, _1, _2, _3, _4, _5, }, Tuple6::_T6{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash> Eq
         for Tuple6<T0, T1, T2, T3, T4, T5> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash> Hash
@@ -732,20 +789,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default> Default
-        for Tuple6<T0, T1, T2, T3, T4, T5> {
-        fn default() -> Tuple6<T0, T1, T2, T3, T4, T5> {
-            Tuple6::_T6 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType> AsRef<Tuple6<T0, T1, T2, T3, T4, T5>>
         for Tuple6<T0, T1, T2, T3, T4, T5> {
         fn as_ref(&self) -> &Self {
@@ -753,7 +796,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple7<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType> {
         _T7 {
             _0: T0,
@@ -865,7 +908,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash> PartialEq
+        for Tuple7<T0, T1, T2, T3, T4, T5, T6> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, }, Tuple7::_T7{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash> Eq
         for Tuple7<T0, T1, T2, T3, T4, T5, T6> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash> Hash
@@ -885,21 +945,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default> Default
-        for Tuple7<T0, T1, T2, T3, T4, T5, T6> {
-        fn default() -> Tuple7<T0, T1, T2, T3, T4, T5, T6> {
-            Tuple7::_T7 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType> AsRef<Tuple7<T0, T1, T2, T3, T4, T5, T6>>
         for Tuple7<T0, T1, T2, T3, T4, T5, T6> {
         fn as_ref(&self) -> &Self {
@@ -907,7 +952,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple8<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType> {
         _T8 {
             _0: T0,
@@ -1029,7 +1074,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash> PartialEq
+        for Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, }, Tuple8::_T8{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash> Eq
         for Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash> Hash
@@ -1050,22 +1112,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default> Default
-        for Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {
-        fn default() -> Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {
-            Tuple8::_T8 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType> AsRef<Tuple8<T0, T1, T2, T3, T4, T5, T6, T7>>
         for Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {
         fn as_ref(&self) -> &Self {
@@ -1073,7 +1119,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple9<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType> {
         _T9 {
             _0: T0,
@@ -1205,7 +1251,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq, T8: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash> PartialEq
+        for Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, }, Tuple9::_T9{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash> Eq
         for Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash> Hash
@@ -1227,23 +1290,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default, T8: DafnyType + Default> Default
-        for Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
-        fn default() -> Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
-            Tuple9::_T9 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default(),
-                _8: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType> AsRef<Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8>>
         for Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
         fn as_ref(&self) -> &Self {
@@ -1251,7 +1297,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple10<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType> {
         _T10 {
             _0: T0,
@@ -1393,7 +1439,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq, T8: DafnyType + Eq, T9: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash> PartialEq
+        for Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, }, Tuple10::_T10{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash> Eq
         for Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash> Hash
@@ -1416,24 +1479,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default, T8: DafnyType + Default, T9: DafnyType + Default> Default
-        for Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {
-        fn default() -> Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {
-            Tuple10::_T10 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default(),
-                _8: Default::default(),
-                _9: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType> AsRef<Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9>>
         for Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {
         fn as_ref(&self) -> &Self {
@@ -1441,7 +1486,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple11<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType> {
         _T11 {
             _0: T0,
@@ -1593,7 +1638,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq, T8: DafnyType + Eq, T9: DafnyType + Eq, T10: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash> PartialEq
+        for Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, }, Tuple11::_T11{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash> Eq
         for Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash> Hash
@@ -1617,25 +1679,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default, T8: DafnyType + Default, T9: DafnyType + Default, T10: DafnyType + Default> Default
-        for Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {
-        fn default() -> Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {
-            Tuple11::_T11 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default(),
-                _8: Default::default(),
-                _9: Default::default(),
-                _10: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType> AsRef<Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10>>
         for Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {
         fn as_ref(&self) -> &Self {
@@ -1643,7 +1686,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple12<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType> {
         _T12 {
             _0: T0,
@@ -1805,7 +1848,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq, T8: DafnyType + Eq, T9: DafnyType + Eq, T10: DafnyType + Eq, T11: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash> PartialEq
+        for Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, }, Tuple12::_T12{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash> Eq
         for Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash> Hash
@@ -1830,26 +1890,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default, T8: DafnyType + Default, T9: DafnyType + Default, T10: DafnyType + Default, T11: DafnyType + Default> Default
-        for Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {
-        fn default() -> Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {
-            Tuple12::_T12 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default(),
-                _8: Default::default(),
-                _9: Default::default(),
-                _10: Default::default(),
-                _11: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType> AsRef<Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11>>
         for Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {
         fn as_ref(&self) -> &Self {
@@ -1857,7 +1897,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple13<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType> {
         _T13 {
             _0: T0,
@@ -2029,7 +2069,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq, T8: DafnyType + Eq, T9: DafnyType + Eq, T10: DafnyType + Eq, T11: DafnyType + Eq, T12: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash> PartialEq
+        for Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, }, Tuple13::_T13{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash> Eq
         for Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash> Hash
@@ -2055,27 +2112,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default, T8: DafnyType + Default, T9: DafnyType + Default, T10: DafnyType + Default, T11: DafnyType + Default, T12: DafnyType + Default> Default
-        for Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {
-        fn default() -> Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {
-            Tuple13::_T13 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default(),
-                _8: Default::default(),
-                _9: Default::default(),
-                _10: Default::default(),
-                _11: Default::default(),
-                _12: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType> AsRef<Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12>>
         for Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {
         fn as_ref(&self) -> &Self {
@@ -2083,7 +2119,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple14<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType> {
         _T14 {
             _0: T0,
@@ -2265,7 +2301,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq, T8: DafnyType + Eq, T9: DafnyType + Eq, T10: DafnyType + Eq, T11: DafnyType + Eq, T12: DafnyType + Eq, T13: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash> PartialEq
+        for Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, }, Tuple14::_T14{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash> Eq
         for Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash> Hash
@@ -2292,28 +2345,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default, T8: DafnyType + Default, T9: DafnyType + Default, T10: DafnyType + Default, T11: DafnyType + Default, T12: DafnyType + Default, T13: DafnyType + Default> Default
-        for Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {
-        fn default() -> Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {
-            Tuple14::_T14 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default(),
-                _8: Default::default(),
-                _9: Default::default(),
-                _10: Default::default(),
-                _11: Default::default(),
-                _12: Default::default(),
-                _13: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType> AsRef<Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13>>
         for Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {
         fn as_ref(&self) -> &Self {
@@ -2321,7 +2352,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple15<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType> {
         _T15 {
             _0: T0,
@@ -2513,7 +2544,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq, T8: DafnyType + Eq, T9: DafnyType + Eq, T10: DafnyType + Eq, T11: DafnyType + Eq, T12: DafnyType + Eq, T13: DafnyType + Eq, T14: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash> PartialEq
+        for Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, }, Tuple15::_T15{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, _14: _2__14, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13 && _14 == _2__14
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash> Eq
         for Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash, T14: DafnyType + Hash> Hash
@@ -2541,29 +2589,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default, T8: DafnyType + Default, T9: DafnyType + Default, T10: DafnyType + Default, T11: DafnyType + Default, T12: DafnyType + Default, T13: DafnyType + Default, T14: DafnyType + Default> Default
-        for Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {
-        fn default() -> Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {
-            Tuple15::_T15 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default(),
-                _8: Default::default(),
-                _9: Default::default(),
-                _10: Default::default(),
-                _11: Default::default(),
-                _12: Default::default(),
-                _13: Default::default(),
-                _14: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType> AsRef<Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14>>
         for Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {
         fn as_ref(&self) -> &Self {
@@ -2571,7 +2596,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple16<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType> {
         _T16 {
             _0: T0,
@@ -2773,7 +2798,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq, T8: DafnyType + Eq, T9: DafnyType + Eq, T10: DafnyType + Eq, T11: DafnyType + Eq, T12: DafnyType + Eq, T13: DafnyType + Eq, T14: DafnyType + Eq, T15: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash> PartialEq
+        for Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, }, Tuple16::_T16{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, _14: _2__14, _15: _2__15, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13 && _14 == _2__14 && _15 == _2__15
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash> Eq
         for Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash, T14: DafnyType + Hash, T15: DafnyType + Hash> Hash
@@ -2802,30 +2844,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default, T8: DafnyType + Default, T9: DafnyType + Default, T10: DafnyType + Default, T11: DafnyType + Default, T12: DafnyType + Default, T13: DafnyType + Default, T14: DafnyType + Default, T15: DafnyType + Default> Default
-        for Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {
-        fn default() -> Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {
-            Tuple16::_T16 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default(),
-                _8: Default::default(),
-                _9: Default::default(),
-                _10: Default::default(),
-                _11: Default::default(),
-                _12: Default::default(),
-                _13: Default::default(),
-                _14: Default::default(),
-                _15: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType> AsRef<Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15>>
         for Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {
         fn as_ref(&self) -> &Self {
@@ -2833,7 +2851,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple17<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType> {
         _T17 {
             _0: T0,
@@ -3045,7 +3063,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq, T8: DafnyType + Eq, T9: DafnyType + Eq, T10: DafnyType + Eq, T11: DafnyType + Eq, T12: DafnyType + Eq, T13: DafnyType + Eq, T14: DafnyType + Eq, T15: DafnyType + Eq, T16: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash> PartialEq
+        for Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, }, Tuple17::_T17{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, _14: _2__14, _15: _2__15, _16: _2__16, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13 && _14 == _2__14 && _15 == _2__15 && _16 == _2__16
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash> Eq
         for Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash, T14: DafnyType + Hash, T15: DafnyType + Hash, T16: DafnyType + Hash> Hash
@@ -3075,31 +3110,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default, T8: DafnyType + Default, T9: DafnyType + Default, T10: DafnyType + Default, T11: DafnyType + Default, T12: DafnyType + Default, T13: DafnyType + Default, T14: DafnyType + Default, T15: DafnyType + Default, T16: DafnyType + Default> Default
-        for Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {
-        fn default() -> Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {
-            Tuple17::_T17 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default(),
-                _8: Default::default(),
-                _9: Default::default(),
-                _10: Default::default(),
-                _11: Default::default(),
-                _12: Default::default(),
-                _13: Default::default(),
-                _14: Default::default(),
-                _15: Default::default(),
-                _16: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType> AsRef<Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16>>
         for Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {
         fn as_ref(&self) -> &Self {
@@ -3107,7 +3117,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple18<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType> {
         _T18 {
             _0: T0,
@@ -3329,7 +3339,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq, T8: DafnyType + Eq, T9: DafnyType + Eq, T10: DafnyType + Eq, T11: DafnyType + Eq, T12: DafnyType + Eq, T13: DafnyType + Eq, T14: DafnyType + Eq, T15: DafnyType + Eq, T16: DafnyType + Eq, T17: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash, T17: DafnyType + Eq + Hash> PartialEq
+        for Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, }, Tuple18::_T18{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, _14: _2__14, _15: _2__15, _16: _2__16, _17: _2__17, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13 && _14 == _2__14 && _15 == _2__15 && _16 == _2__16 && _17 == _2__17
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash, T17: DafnyType + Eq + Hash> Eq
         for Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash, T14: DafnyType + Hash, T15: DafnyType + Hash, T16: DafnyType + Hash, T17: DafnyType + Hash> Hash
@@ -3360,32 +3387,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default, T8: DafnyType + Default, T9: DafnyType + Default, T10: DafnyType + Default, T11: DafnyType + Default, T12: DafnyType + Default, T13: DafnyType + Default, T14: DafnyType + Default, T15: DafnyType + Default, T16: DafnyType + Default, T17: DafnyType + Default> Default
-        for Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {
-        fn default() -> Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {
-            Tuple18::_T18 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default(),
-                _8: Default::default(),
-                _9: Default::default(),
-                _10: Default::default(),
-                _11: Default::default(),
-                _12: Default::default(),
-                _13: Default::default(),
-                _14: Default::default(),
-                _15: Default::default(),
-                _16: Default::default(),
-                _17: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType> AsRef<Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17>>
         for Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {
         fn as_ref(&self) -> &Self {
@@ -3393,7 +3394,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple19<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType> {
         _T19 {
             _0: T0,
@@ -3625,7 +3626,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq, T8: DafnyType + Eq, T9: DafnyType + Eq, T10: DafnyType + Eq, T11: DafnyType + Eq, T12: DafnyType + Eq, T13: DafnyType + Eq, T14: DafnyType + Eq, T15: DafnyType + Eq, T16: DafnyType + Eq, T17: DafnyType + Eq, T18: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash, T17: DafnyType + Eq + Hash, T18: DafnyType + Eq + Hash> PartialEq
+        for Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, }, Tuple19::_T19{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, _14: _2__14, _15: _2__15, _16: _2__16, _17: _2__17, _18: _2__18, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13 && _14 == _2__14 && _15 == _2__15 && _16 == _2__16 && _17 == _2__17 && _18 == _2__18
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash, T17: DafnyType + Eq + Hash, T18: DafnyType + Eq + Hash> Eq
         for Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash, T14: DafnyType + Hash, T15: DafnyType + Hash, T16: DafnyType + Hash, T17: DafnyType + Hash, T18: DafnyType + Hash> Hash
@@ -3657,33 +3675,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default, T8: DafnyType + Default, T9: DafnyType + Default, T10: DafnyType + Default, T11: DafnyType + Default, T12: DafnyType + Default, T13: DafnyType + Default, T14: DafnyType + Default, T15: DafnyType + Default, T16: DafnyType + Default, T17: DafnyType + Default, T18: DafnyType + Default> Default
-        for Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {
-        fn default() -> Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {
-            Tuple19::_T19 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default(),
-                _8: Default::default(),
-                _9: Default::default(),
-                _10: Default::default(),
-                _11: Default::default(),
-                _12: Default::default(),
-                _13: Default::default(),
-                _14: Default::default(),
-                _15: Default::default(),
-                _16: Default::default(),
-                _17: Default::default(),
-                _18: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType> AsRef<Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18>>
         for Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {
         fn as_ref(&self) -> &Self {
@@ -3691,7 +3682,7 @@ pub mod _System {
         }
     }
 
-    #[derive(PartialEq, Clone)]
+    #[derive(Clone)]
     pub enum Tuple20<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType, T19: DafnyType> {
         _T20 {
             _0: T0,
@@ -3933,7 +3924,24 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Eq, T1: DafnyType + Eq, T2: DafnyType + Eq, T3: DafnyType + Eq, T4: DafnyType + Eq, T5: DafnyType + Eq, T6: DafnyType + Eq, T7: DafnyType + Eq, T8: DafnyType + Eq, T9: DafnyType + Eq, T10: DafnyType + Eq, T11: DafnyType + Eq, T12: DafnyType + Eq, T13: DafnyType + Eq, T14: DafnyType + Eq, T15: DafnyType + Eq, T16: DafnyType + Eq, T17: DafnyType + Eq, T18: DafnyType + Eq, T19: DafnyType + Eq> Eq
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash, T17: DafnyType + Eq + Hash, T18: DafnyType + Eq + Hash, T19: DafnyType + Eq + Hash> PartialEq
+        for Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {
+        fn eq(&self, other: &Self) -> bool {
+            match (
+                    self,
+                    other
+                ) {
+                (Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, }, Tuple20::_T20{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, _14: _2__14, _15: _2__15, _16: _2__16, _17: _2__17, _18: _2__18, _19: _2__19, }) => {
+                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13 && _14 == _2__14 && _15 == _2__15 && _16 == _2__16 && _17 == _2__17 && _18 == _2__18 && _19 == _2__19
+                },
+                _ => {
+                    false
+                },
+            }
+        }
+    }
+
+    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash, T17: DafnyType + Eq + Hash, T18: DafnyType + Eq + Hash, T19: DafnyType + Eq + Hash> Eq
         for Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {}
 
     impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash, T14: DafnyType + Hash, T15: DafnyType + Hash, T16: DafnyType + Hash, T17: DafnyType + Hash, T18: DafnyType + Hash, T19: DafnyType + Hash> Hash
@@ -3966,34 +3974,6 @@ pub mod _System {
         }
     }
 
-    impl<T0: DafnyType + Default, T1: DafnyType + Default, T2: DafnyType + Default, T3: DafnyType + Default, T4: DafnyType + Default, T5: DafnyType + Default, T6: DafnyType + Default, T7: DafnyType + Default, T8: DafnyType + Default, T9: DafnyType + Default, T10: DafnyType + Default, T11: DafnyType + Default, T12: DafnyType + Default, T13: DafnyType + Default, T14: DafnyType + Default, T15: DafnyType + Default, T16: DafnyType + Default, T17: DafnyType + Default, T18: DafnyType + Default, T19: DafnyType + Default> Default
-        for Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {
-        fn default() -> Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {
-            Tuple20::_T20 {
-                _0: Default::default(),
-                _1: Default::default(),
-                _2: Default::default(),
-                _3: Default::default(),
-                _4: Default::default(),
-                _5: Default::default(),
-                _6: Default::default(),
-                _7: Default::default(),
-                _8: Default::default(),
-                _9: Default::default(),
-                _10: Default::default(),
-                _11: Default::default(),
-                _12: Default::default(),
-                _13: Default::default(),
-                _14: Default::default(),
-                _15: Default::default(),
-                _16: Default::default(),
-                _17: Default::default(),
-                _18: Default::default(),
-                _19: Default::default()
-            }
-        }
-    }
-
     impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType, T19: DafnyType> AsRef<Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19>>
         for Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {
         fn as_ref(&self) -> &Self {
diff --git a/releases/rust/db_esdk/dafny_runtime_rust/src/tests/mod.rs b/releases/rust/db_esdk/dafny_runtime_rust/src/tests/mod.rs
index 4ac2fb26b..bf75fc6e2 100644
--- a/releases/rust/db_esdk/dafny_runtime_rust/src/tests/mod.rs
+++ b/releases/rust/db_esdk/dafny_runtime_rust/src/tests/mod.rs
@@ -71,6 +71,56 @@ mod tests {
         }
     }
 
+    // This one is still the bad kind of recursive
+    #[test]
+    fn test_sequence_right() {
+        let a: Sequence<i32> = seq![1, 2];
+        let b = seq![3, 4];
+        let c = seq![5, 6];
+        let d = seq![7, 8];
+        let e = seq![9, 10];
+        let f = seq![11, 12];
+        let g = seq![13, 14];
+        let h = seq![15, 16];
+        let c1 = Sequence::<i32>::new_concat_sequence(&a, &b);
+        let c2 = Sequence::<i32>::new_concat_sequence(&c1, &c);
+        let c3 = Sequence::<i32>::new_concat_sequence(&c2, &d);
+        let c4 = Sequence::<i32>::new_concat_sequence(&c3, &e);
+        let c5 = Sequence::<i32>::new_concat_sequence(&c4, &f);
+        let c6 = Sequence::<i32>::new_concat_sequence(&c5, &g);
+        let c7 = Sequence::<i32>::new_concat_sequence(&c6, &h);
+        let arr = c7.to_array();
+        assert_eq!(
+            *arr,
+            vec![1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]
+        );
+    }
+
+    // This one is successfully tail recursive
+    #[test]
+    fn test_sequence_left() {
+        let a = seq![1, 2];
+        let b = seq![3, 4];
+        let c = seq![5, 6];
+        let d = seq![7, 8];
+        let e = seq![9, 10];
+        let f = seq![11, 12];
+        let g = seq![13, 14];
+        let h = seq![15, 16];
+        let c1 = Sequence::<i32>::new_concat_sequence(&g, &h);
+        let c2 = Sequence::<i32>::new_concat_sequence(&f, &c1);
+        let c3 = Sequence::<i32>::new_concat_sequence(&e, &c2);
+        let c4 = Sequence::<i32>::new_concat_sequence(&d, &c3);
+        let c5 = Sequence::<i32>::new_concat_sequence(&c, &c4);
+        let c6 = Sequence::<i32>::new_concat_sequence(&b, &c5);
+        let c7 = Sequence::<i32>::new_concat_sequence(&a, &c6);
+        let arr = c7.to_array();
+        assert_eq!(
+            *arr,
+            vec![1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]
+        );
+    }
+
     #[test]
     fn test_sequence() {
         let values = vec![1, 2, 3];
@@ -80,8 +130,8 @@ mod tests {
 
         // Create a concat array, wrap it into a lazy one, get the i-th element,
         // and verify that this operation flattened the array
-        let left = Sequence::<i32>::from_array_owned(vec![1, 2, 3]);
-        let right = Sequence::<i32>::from_array_owned(vec![4, 5, 6]);
+        let left = seq![1, 2, 3];
+        let right = seq![4, 5, 6];
         let concat = Sequence::<i32>::new_concat_sequence(&left, &right);
 
         assert_eq!(concat.cardinality_usize(), 6);
@@ -108,7 +158,7 @@ mod tests {
         let value = concat.get_usize(0);
         assert_eq!(value, 1);
         match &concat {
-            crate::Sequence::ConcatSequence { cache: boxed, .. } => {
+            Sequence::ConcatSequence { cache: boxed, .. } => {
                 #[cfg(not(feature = "sync"))]
                 assert_eq!(
                     *boxed.as_ref().clone().borrow().as_ref().unwrap().as_ref(),
@@ -327,7 +377,6 @@ mod tests {
         assert_eq!(map![].merge(&m_4), m_4);
         let m_5 = m_4.merge(&map![3 => 9, 6 => 12]);
         assert_eq!(m_5.cardinality_usize(), 5);
-        println!("m_4 is {:?}", m_4);
         assert_eq!(m_4.get(&3), 6);
         assert_eq!(m_5.get(&3), 9);
         assert_eq!(m_5.subtract(&set! {}), m_5);
@@ -339,8 +388,8 @@ mod tests {
     #[test]
     fn test_dafny_array() {
         let a = array![1, 2, 3];
-        assert_eq!(crate::array::length_usize(a), 3);
-        assert_eq!(crate::array::length(a), int!(3));
+        assert_eq!(array::length_usize(a), 3);
+        assert_eq!(array::length(a), int!(3));
         assert_eq!(array::get_usize(a, 0), 1);
         assert_eq!(array::get_usize(a, 1), 2);
         assert_eq!(array::get_usize(a, 2), 3);
@@ -451,12 +500,12 @@ mod tests {
 
     struct ClassWrapper<T> {
         /*var*/ t: Field<T>,
-        /*var*/ x: Field<crate::DafnyInt>,
+        /*var*/ x: Field<DafnyInt>,
         /*const*/ next: Ptr<ClassWrapper<T>>,
-        /*const*/ constant: crate::DafnyInt,
+        /*const*/ constant: DafnyInt,
     }
     impl<T: Clone> ClassWrapper<T> {
-        fn constant_plus_x(&self) -> crate::DafnyInt {
+        fn constant_plus_x(&self) -> DafnyInt {
             self.constant.clone() + read_field!(self.x)
         }
         fn increment_x(&mut self) {
@@ -466,7 +515,7 @@ mod tests {
 
     impl<T: Clone + Display> ClassWrapper<T> {
         fn constructor(t: T) -> Ptr<ClassWrapper<T>> {
-            let this = crate::allocate::<ClassWrapper<T>>();
+            let this = allocate::<ClassWrapper<T>>();
             update_field_mut_nodrop!(this, t, t);
             update_field_nodrop!(this, next, this);
             // If x is assigned twice, we need to keep track of whether it's assigned
@@ -486,7 +535,7 @@ mod tests {
         }
 
         fn constructor_object(t: T) -> Object<ClassWrapper<T>> {
-            let mut this = crate::allocate_object::<ClassWrapper<T>>();
+            let mut this = allocate_object::<ClassWrapper<T>>();
             update_field_mut_nodrop_object!(this, t, t);
             update_field_nodrop_object!(this, next, Ptr::from_raw_nonnull(this.as_mut()));
             // If x is assigned twice, we need to keep track of whether it's assigned
@@ -511,11 +560,11 @@ mod tests {
         }
     }
 
-    impl<T: DafnyType> Upcast<crate::DynAny> for ClassWrapper<T> {
-        UpcastFn!(crate::DynAny);
+    impl<T: DafnyType> Upcast<DynAny> for ClassWrapper<T> {
+        UpcastFn!(DynAny);
     }
-    impl<T: DafnyType> UpcastObject<crate::DynAny> for ClassWrapper<T> {
-        UpcastObjectFn!(crate::DynAny);
+    impl<T: DafnyType> UpcastObject<DynAny> for ClassWrapper<T> {
+        UpcastObjectFn!(DynAny);
     }
 
     #[test]
@@ -533,10 +582,14 @@ mod tests {
         assert_eq!(read!(c).constant_plus_x(), int!(82));
         modify_field!(read!(c).t, 54);
         assert_eq!(read_field!(read!(c).t), 54);
+        #[cfg(not(feature = "small-int"))]
         let x_copy = read_field!(read!(c).x);
-        assert_eq!(Rc::strong_count(&x_copy.data), 2);
+        #[cfg(not(feature = "small-int"))]
+        assert_eq!(x_copy.strong_count(), 2);
+        #[cfg(not(feature = "small-int"))]
         deallocate(c);
-        assert_eq!(Rc::strong_count(&x_copy.data), 1);
+        #[cfg(not(feature = "small-int"))]
+        assert_eq!(x_copy.strong_count(), 1);
     }
 
     #[test]
@@ -564,14 +617,11 @@ mod tests {
     fn assign_lazy_in_method(test1: bool, test2: bool) -> Rc<i32> {
         let mut t = MaybePlacebo::<Rc<i32>>::new();
         if test1 {
-            t = MaybePlacebo::from(Rc::new(5 as i32));
+            t = MaybePlacebo::from(Rc::new(5));
         }
         if test2 {
-            t = MaybePlacebo::from(Rc::new(
-                7 as i32 + if test1 { *MaybePlacebo::read(&t) } else { 0 },
-            ));
+            t = MaybePlacebo::from(Rc::new(7 + if test1 { *MaybePlacebo::read(&t) } else { 0 }));
         }
-        println!("{}", MaybePlacebo::read(&t));
         MaybePlacebo::read(&t)
     }
 
@@ -594,8 +644,6 @@ mod tests {
 
     #[test]
     fn test_placebo() {
-        override_placebo::<Rc<BigInt>>(Rc::new(BigInt::from(1)), false);
-        override_placebo::<Rc<BigInt>>(Rc::new(BigInt::from(1)), true);
         override_placebo::<DafnyInt>(int!(1), false);
         override_placebo::<DafnyInt>(int!(1), true);
         let _x: MaybePlacebo<Ptr<ClassWrapper<DafnyInt>>> =
@@ -616,30 +664,27 @@ mod tests {
     #[test]
     fn test_coercion_immutable() {
         let o = ClassWrapper::<i32>::constructor(1);
-        let a: Ptr<crate::DynAny> = Upcast::<crate::DynAny>::upcast(read!(o));
+        let a: Ptr<DynAny> = Upcast::<DynAny>::upcast(read!(o));
         assert_eq!(cast!(a, ClassWrapper<i32>), o);
         let seq_o = seq![o];
-        let seq_a = Sequence::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<
-            ClassWrapper<i32>,
-            crate::DynAny,
-        >())(seq_o);
+        let seq_a = Sequence::<Ptr<ClassWrapper<i32>>>::coerce(
+            upcast::<ClassWrapper<i32>, DynAny>(),
+        )(seq_o);
         assert_eq!(cast!(seq_a.get_usize(0), ClassWrapper<i32>), o);
         let set_o = set! {o};
-        let set_a = Set::<Ptr<ClassWrapper<i32>>>::coerce(
-            upcast::<ClassWrapper<i32>, crate::DynAny>(),
-        )(set_o);
+        let set_a =
+            Set::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, DynAny>())(set_o);
         assert_eq!(cast!(set_a.peek(), ClassWrapper<i32>), o);
         let multiset_o = multiset! {o, o};
         let multiset_a = Multiset::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<
             ClassWrapper<i32>,
-            crate::DynAny,
+            DynAny,
         >())(multiset_o);
         assert_eq!(cast!(multiset_a.peek(), ClassWrapper<i32>), o);
         let map_o = map![1 => o, 2 => o];
-        let map_a = Map::<i32, Ptr<ClassWrapper<i32>>>::coerce(upcast::<
-            ClassWrapper<i32>,
-            crate::DynAny,
-        >())(map_o);
+        let map_a = Map::<i32, Ptr<ClassWrapper<i32>>>::coerce(
+            upcast::<ClassWrapper<i32>, DynAny>(),
+        )(map_o);
         assert_eq!(cast!(map_a.get(&1), ClassWrapper<i32>), o);
         deallocate(o);
     }
@@ -673,15 +718,17 @@ mod tests {
     #[test]
     fn test_function_wrappers() {
         #[cfg(feature = "sync")]
-        let f: Rc<dyn Fn(i32) -> i32 + Send + Sync> = Rc::new(|i: i32| i + 1);
+        let f: Rc<dyn Fn(&i32) -> i32 + Send + Sync> = Rc::new(|i: &i32| *i + 1);
         #[cfg(not(feature = "sync"))]
-        let f: Rc<dyn Fn(i32) -> i32> = Rc::new(|i: i32| i + 1);
+        let f: Rc<dyn Fn(&i32) -> i32> = Rc::new(|i: &i32| *i + 1);
         let g = f.clone();
         let _h = seq![g];
     }
 
     #[test]
     fn test_forall_exists() {
+        assert!(integer_range(Zero::zero(), int!(10))
+            .all(Rc::new(|i: DafnyInt| i.clone() < int!(10)).as_ref()));
         assert!(integer_range(int!(0), int!(10))
             .all(Rc::new(|i: DafnyInt| i.clone() < int!(10)).as_ref()));
         assert!(!integer_range(int!(0), int!(11))
@@ -748,11 +795,6 @@ mod tests {
             .iter()
             .cloned()
             .any(Rc::new(|i: u32| i % 2 == 0).as_ref()));
-
-        for i in set! {1, 3, 5, 7}.iter() {
-            println!("{}", i);
-        }
-
         assert!(multiset! {1, 1, 5, 7}
             .iter()
             .all(Rc::new(|i: u32| i % 2 == 1).as_ref()));
@@ -840,11 +882,11 @@ mod tests {
         assert_eq!(sum, 55);
     }
 
-    trait SuperTrait: Upcast<crate::DynAny> + UpcastObject<crate::DynAny> {}
+    trait SuperTrait: Upcast<DynAny> + UpcastObject<DynAny> {}
 
     trait NodeRcMutTrait: SuperTrait + Upcast<dyn SuperTrait> + UpcastObject<dyn SuperTrait> {}
 
-    pub struct NodeRcMut {
+    struct NodeRcMut {
         val: DafnyInt,
         next: Object<NodeRcMut>,
     }
@@ -857,11 +899,11 @@ mod tests {
         }
     }
     impl SuperTrait for NodeRcMut {}
-    impl UpcastObject<crate::DynAny> for NodeRcMut {
-        UpcastObjectFn!(crate::DynAny);
+    impl UpcastObject<DynAny> for NodeRcMut {
+        UpcastObjectFn!(DynAny);
     }
-    impl Upcast<crate::DynAny> for NodeRcMut {
-        UpcastFn!(crate::DynAny);
+    impl Upcast<DynAny> for NodeRcMut {
+        UpcastFn!(DynAny);
     }
     impl UpcastObject<dyn NodeRcMutTrait> for NodeRcMut {
         UpcastObjectFn!(dyn NodeRcMutTrait);
@@ -888,7 +930,7 @@ mod tests {
         assert_eq!(x.as_ref().next.as_ref().val, int!(42));
         md!(rd!(x).next).next = Object(None);
         assert_eq!(refcount!(x), 1);
-        let y: Object<crate::DynAny> = upcast_object::<_, _>()(x.clone());
+        let y: Object<DynAny> = upcast_object::<_, _>()(x.clone());
         assert_eq!(refcount!(x), 2);
         let z: Object<dyn NodeRcMutTrait> = upcast_object::<_, _>()(x.clone());
         assert_eq!(refcount!(x), 3);
@@ -927,13 +969,12 @@ mod tests {
         }
         assert_eq!(refcount!(x), previous_count);
 
-        let objects: Set<Object<crate::DynAny>> =
-            crate::set! {y.clone(), cast_any_object!(x.clone())};
+        let objects: Set<Object<DynAny>> = crate::set! {y.clone(), cast_any_object!(x.clone())};
         assert_eq!(objects.cardinality_usize(), 1);
         test_dafny_type(a.clone());
     }
 
-    pub struct NodeRawMut {
+    struct NodeRawMut {
         val: DafnyInt,
         next: Ptr<NodeRawMut>,
     }
@@ -944,18 +985,8 @@ mod tests {
         }
     }
     impl NodeRcMutTrait for NodeRawMut {}
-    UpcastDefObject!(
-        NodeRawMut,
-        dyn NodeRcMutTrait,
-        dyn SuperTrait,
-        crate::DynAny
-    );
-    UpcastDef!(
-        NodeRawMut,
-        dyn NodeRcMutTrait,
-        dyn SuperTrait,
-        crate::DynAny
-    );
+    UpcastDefObject!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, DynAny);
+    UpcastDef!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, DynAny);
 
     impl SuperTrait for NodeRawMut {}
 
@@ -967,7 +998,7 @@ mod tests {
         modify!(x.clone()).next = x.clone();
         assert_eq!(read!(read!(x.clone()).next.clone()).val, int!(42));
         modify!(read!(x.clone()).next.clone()).next = Ptr::null();
-        let y: Ptr<crate::DynAny> = upcast::<_, _>()(x);
+        let y: Ptr<DynAny> = upcast::<_, _>()(x);
         assert!(y.is_instance_of::<NodeRawMut>());
         assert!(!y.is_instance_of::<NodeRcMut>());
         let z: Ptr<dyn NodeRcMutTrait> = upcast::<_, _>()(x);
@@ -1005,11 +1036,11 @@ mod tests {
     fn test_dafny_type<X: DafnyType>(_input: X) {}
 
     #[derive(Clone)]
-    pub struct InternalOpaqueError {
-        pub message: String,
+    struct InternalOpaqueError {
+        message: String,
     }
 
-    crate::UpcastDefObject!(InternalOpaqueError, crate::DynAny);
+    crate::UpcastDefObject!(InternalOpaqueError, DynAny);
 
     #[test]
     fn test_native_string_upcast() {
@@ -1017,9 +1048,9 @@ mod tests {
             message: "Hello, World!".to_string(),
         };
         let o: Object<InternalOpaqueError> = Object::new(s);
-        let n: Object<crate::DynAny> = upcast_object::<InternalOpaqueError, crate::DynAny>()(o);
+        let n: Object<DynAny> = upcast_object::<InternalOpaqueError, DynAny>()(o);
         let x = cast_object!(n, InternalOpaqueError);
-        let s2 = crate::dafny_runtime_conversions::object::dafny_class_to_struct(x);
+        let s2 = dafny_runtime_conversions::object::dafny_class_to_struct(x);
         assert_eq!(s2.message, "Hello, World!");
     }
 
@@ -1027,20 +1058,51 @@ mod tests {
     fn test_native_string_upcast_raw() {
         let message = "Hello, World!".to_string();
         let object = Object::new(message.clone());
-        let object_any: Object<crate::DynAny> =
-            UpcastObject::<crate::DynAny>::upcast(object.as_ref());
+        let object_any: Object<DynAny> = UpcastObject::<DynAny>::upcast(object.as_ref());
         let resulting_message = format!("{:?}", object_any);
         assert_eq!(resulting_message, message);
     }
 
+    /** Hierarchy implemented
+     * GeneralTraitSuper<T>
+     *  |                \____________________,
+     *  |                                     |
+     * GeneralTraitSuper<i32>                GeneralTraitSuperChild<T>
+     *  |                                     | (via i32)
+     * GeneralTrait                          CDatatype
+     *  |         |
+     * ADatatype  BDatatype
+     */
+
+    trait _Downcast_GeneralTrait {
+        fn _is(&self) -> bool;
+        fn _as(&self) -> Box<dyn GeneralTrait>; // For trait objects, Object or Ptr instead of Box
+    }
+
+    trait _Downcast_ADatatype {
+        fn _is(&self) -> bool;
+        fn _as(&self) -> ADatatype; // For trait objects, Object or Ptr instead of Box
+    }
+    trait _Downcast_CDatatype {
+        fn _is(&self) -> bool;
+        fn _as(&self) -> CDatatype; // For trait objects, Object or Ptr instead of Box
+    }
+
     // Every general trait must declare how to clone a Box<dyn .> of itself
-    trait GeneralTraitSuper<T> {
+    trait GeneralTraitSuper<T>:
+        _Downcast_GeneralTrait + AnyRef + _Downcast_GeneralTraitSuperChild<T>
+    {
         fn _clone(&self) -> Box<dyn GeneralTraitSuper<T>>;
-        fn _is_GeneralTrait(&self) -> bool;
-        fn _as_GeneralTrait(&self) -> Box<dyn GeneralTrait>;
-        fn _is_Datatype(&self) -> bool;
-        fn _as_Datatype(&self) -> ADatatype;
     }
+    trait GeneralTraitSuperChild<T>: GeneralTraitSuper<T> {
+        fn _clone(&self) -> Box<dyn GeneralTraitSuperChild<T>>;
+    }
+
+    trait _Downcast_GeneralTraitSuperChild<T> {
+        fn _is(&self) -> bool;
+        fn _as(&self) -> Box<dyn GeneralTraitSuperChild<T>>; // For trait objects, Object or Ptr instead of Box
+    }
+
     impl<T> Clone for Box<dyn GeneralTraitSuper<T>> {
         fn clone(&self) -> Self {
             GeneralTraitSuper::_clone(self.as_ref())
@@ -1055,11 +1117,6 @@ mod tests {
     trait GeneralTrait: GeneralTraitSuper<i32> + UpcastBox<dyn GeneralTraitSuper<i32>> {
         fn _clone(&self) -> Box<dyn GeneralTrait>;
     }
-    impl UpcastBox<dyn GeneralTraitSuper<i32>> for Box<dyn GeneralTrait> {
-        fn upcast(&self) -> ::std::boxed::Box<dyn crate::tests::tests::GeneralTraitSuper<i32>> {
-            crate::tests::tests::GeneralTraitSuper::<i32>::_clone(self.as_ref())
-        }
-    }
     impl Clone for Box<dyn GeneralTrait> {
         fn clone(&self) -> Self {
             GeneralTrait::_clone(self.as_ref())
@@ -1080,25 +1137,33 @@ mod tests {
             Box::new(self.clone()) as Box<dyn GeneralTrait>
         }
     }
-    impl GeneralTraitSuper<i32> for ADatatype {
-        fn _clone(&self) -> Box<dyn GeneralTraitSuper<i32>> {
-            Box::new(self.clone())
+    impl _Downcast_ADatatype for dyn Any {
+        fn _is(&self) -> bool {
+            self.downcast_ref::<ADatatype>().is_some()
         }
-
-        fn _is_GeneralTrait(&self) -> bool {
+        fn _as(&self) -> ADatatype {
+            self.downcast_ref::<ADatatype>().unwrap().clone() // Optimization: Could be unwrap_unchecked
+        }
+    }
+    impl<T: GeneralTrait> _Downcast_GeneralTrait for T {
+        fn _is(&self) -> bool {
             true
         }
-
-        fn _as_GeneralTrait(&self) -> Box<dyn GeneralTrait> {
+        fn _as(&self) -> Box<dyn GeneralTrait> {
             GeneralTrait::_clone(self)
         }
-
-        fn _is_Datatype(&self) -> bool {
-            true
+    }
+    impl GeneralTraitSuper<i32> for ADatatype {
+        fn _clone(&self) -> Box<dyn GeneralTraitSuper<i32>> {
+            Box::new(self.clone())
         }
-
-        fn _as_Datatype(&self) -> ADatatype {
-            self.clone()
+    }
+    impl _Downcast_GeneralTraitSuperChild<i32> for ADatatype {
+        fn _is(&self) -> bool {
+            false
+        }
+        fn _as(&self) -> Box<dyn GeneralTraitSuperChild<i32>> {
+            panic!("cannot")
         }
     }
     impl UpcastBox<dyn GeneralTrait> for ADatatype {
@@ -1111,26 +1176,110 @@ mod tests {
             GeneralTraitSuper::<i32>::_clone(self)
         }
     }
+
+    #[derive(Clone, PartialEq, Debug)]
+    struct CDatatype {
+        i: u32,
+    }
+    impl _Downcast_CDatatype for dyn Any {
+        fn _is(&self) -> bool {
+            self.downcast_ref::<CDatatype>().is_some()
+        }
+        fn _as(&self) -> CDatatype {
+            self.downcast_ref::<CDatatype>().unwrap().clone() // Optimization: Could be unwrap_unchecked
+        }
+    }
+    impl UpcastBox<dyn GeneralTraitSuper<i32>> for CDatatype {
+        fn upcast(&self) -> ::std::boxed::Box<dyn GeneralTraitSuper<i32>> {
+            GeneralTraitSuper::<i32>::_clone(self)
+        }
+    }
+    impl UpcastBox<dyn GeneralTraitSuperChild<i32>> for CDatatype {
+        fn upcast(&self) -> ::std::boxed::Box<dyn GeneralTraitSuperChild<i32>> {
+            GeneralTraitSuperChild::<i32>::_clone(self)
+        }
+    }
+
+    impl GeneralTraitSuper<i32> for CDatatype {
+        fn _clone(&self) -> Box<dyn GeneralTraitSuper<i32>> {
+            Box::new(self.clone())
+        }
+    }
+    impl GeneralTraitSuperChild<i32> for CDatatype {
+        fn _clone(&self) -> Box<dyn GeneralTraitSuperChild<i32>> {
+            Box::new(self.clone())
+        }
+    }
+    impl _Downcast_GeneralTraitSuperChild<i32> for CDatatype {
+        fn _is(&self) -> bool {
+            true
+        }
+        fn _as(&self) -> Box<dyn GeneralTraitSuperChild<i32>> {
+            GeneralTraitSuperChild::<i32>::_clone(self)
+        }
+    }
+    impl _Downcast_GeneralTrait for CDatatype {
+        // CDatatype does not extend general trait
+        fn _is(&self) -> bool {
+            false
+        }
+        fn _as(&self) -> Box<dyn GeneralTrait> {
+            panic!("CDatatype does not extend GeneralTrait")
+        }
+    }
     #[test]
     fn test_general_traits() {
         let x = ADatatype { i: 3 };
         let gt = upcast_box::<ADatatype, dyn GeneralTrait>()(x.clone());
         let gts = upcast_box::<ADatatype, dyn GeneralTraitSuper<i32>>()(x.clone());
         let gtgts = upcast_box_box::<dyn GeneralTrait, dyn GeneralTraitSuper<i32>>()(gt.clone());
-        assert!(gt._is_Datatype());
-        assert!(gts._is_Datatype());
-        assert!(gtgts._is_Datatype());
-        assert!(gts._is_GeneralTrait());
-        assert!(gtgts._is_GeneralTrait());
-        assert_eq!(gt._as_Datatype(), x);
-        assert_eq!(gts._as_Datatype(), x);
-        assert_eq!(gtgts._as_Datatype(), x);
-        let gtsgt = gts._as_GeneralTrait();
-        let gtgtsgt = gtgts._as_GeneralTrait();
-        assert!(gtsgt._is_Datatype());
-        assert!(gtgtsgt._is_Datatype());
-        assert_eq!(gtsgt._as_Datatype(), x);
-        assert_eq!(gtsgt._as_Datatype(), x);
+        assert!(_Downcast_ADatatype::_is(AnyRef::as_any_ref(AsRef::as_ref(
+            &gt
+        ))));
+        assert!(_Downcast_ADatatype::_is(AnyRef::as_any_ref(AsRef::as_ref(
+            &gts
+        ))));
+        assert!(_Downcast_ADatatype::_is(AnyRef::as_any_ref(AsRef::as_ref(
+            &gtgts
+        ))));
+        assert!(_Downcast_GeneralTrait::_is(AsRef::as_ref(&gts)));
+        assert!(_Downcast_GeneralTrait::_is(AsRef::as_ref(&gtgts)));
+        assert_eq!(
+            _Downcast_ADatatype::_as(AnyRef::as_any_ref(AsRef::as_ref(&gt))),
+            x
+        );
+        assert_eq!(
+            _Downcast_ADatatype::_as(AnyRef::as_any_ref(AsRef::as_ref(&gts))),
+            x
+        );
+        assert_eq!(
+            _Downcast_ADatatype::_as(AnyRef::as_any_ref(AsRef::as_ref(&gtgts))),
+            x
+        );
+        let gtsgt = _Downcast_GeneralTrait::_as(AsRef::as_ref(&gts));
+        let gtgtsgt = _Downcast_GeneralTrait::_as(AsRef::as_ref(&gtgts));
+        assert!(_Downcast_ADatatype::_is(AnyRef::as_any_ref(AsRef::as_ref(
+            &gtsgt
+        ))));
+        assert!(_Downcast_ADatatype::_is(AnyRef::as_any_ref(AsRef::as_ref(
+            &gtgtsgt
+        ))));
+        assert_eq!(
+            _Downcast_ADatatype::_as(AnyRef::as_any_ref(AsRef::as_ref(&gtsgt))),
+            x
+        );
+        assert_eq!(
+            _Downcast_ADatatype::_as(AnyRef::as_any_ref(AsRef::as_ref(&gtsgt))),
+            x
+        );
+        let xc = CDatatype { i: 3 };
+        let gtc = upcast_box::<CDatatype, dyn GeneralTraitSuper<i32>>()(xc.clone());
+        let gcsc = upcast_box::<CDatatype, dyn GeneralTraitSuperChild<i32>>()(xc.clone());
+        let gtcsc = _Downcast_GeneralTraitSuperChild::<i32>::_as(AsRef::as_ref(&gtc));
+        let xc1 = _Downcast_CDatatype::_as(AnyRef::as_any_ref(AsRef::as_ref(&gcsc)));
+        let xc2 = _Downcast_CDatatype::_as(AnyRef::as_any_ref(AsRef::as_ref(&gtcsc)));
+        assert_eq!(xc, xc1);
+        assert_eq!(xc, xc2);
     }
 
     #[test]