diff --git a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs
index 29087cbeb0..396055b185 100644
--- a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs
+++ b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs
@@ -344,7 +344,7 @@ public void AddMethod(DAST.Method item) {
     }
 
     public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
-      parent.AddUnsupported("const for datatypes - " +  item.dtor_name);
+      parent.AddUnsupported("const for datatypes - " + item.dtor_name);
     }
 
     public object Finish() {
diff --git a/Source/DafnyCore/GeneratedFromDafny/Defs.cs b/Source/DafnyCore/GeneratedFromDafny/Defs.cs
index bf93664d1e..c8d2bc4c9a 100644
--- a/Source/DafnyCore/GeneratedFromDafny/Defs.cs
+++ b/Source/DafnyCore/GeneratedFromDafny/Defs.cs
@@ -28,12 +28,12 @@ public static bool has__special(Dafny.ISequence<Dafny.Rune> i) {
         return true;
       } else if (((i).Select(BigInteger.Zero)) == (new Dafny.Rune('_'))) {
         if ((new BigInteger(2)) <= (new BigInteger((i).Count))) {
-          if (((i).Select(BigInteger.One)) != (new Dafny.Rune('_'))) {
-            return true;
-          } else {
+          if (((i).Select(BigInteger.One)) == (new Dafny.Rune('_'))) {
             Dafny.ISequence<Dafny.Rune> _in0 = (i).Drop(new BigInteger(2));
             i = _in0;
             goto TAIL_CALL_START;
+          } else {
+            return true;
           }
         } else {
           return true;
@@ -85,7 +85,7 @@ public static bool is__tuple__builder(Dafny.ISequence<Dafny.Rune> i) {
       return Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_T"), (i).Drop(new BigInteger(8)));
     }
     public static bool is__dafny__generated__id(Dafny.ISequence<Dafny.Rune> i) {
-      return ((((new BigInteger((i).Count)).Sign == 1) && (((i).Select(BigInteger.Zero)) == (new Dafny.Rune('_')))) && (!(Defs.__default.has__special((i).Drop(BigInteger.One))))) && (!((new BigInteger((i).Count)) >= (new BigInteger(2))) || (((i).Select(BigInteger.One)) != (new Dafny.Rune('T'))));
+      return (((((new BigInteger((i).Count)).Sign == 1) && (((i).Select(BigInteger.Zero)) == (new Dafny.Rune('_')))) && (!(Defs.__default.has__special((i).Drop(BigInteger.One))))) && ((!(i).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_self"))) && (!(i).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_Self"))))) && (!((new BigInteger((i).Count)) >= (new BigInteger(2))) || (((i).Select(BigInteger.One)) != (new Dafny.Rune('T'))));
     }
     public static bool is__idiomatic__rust__id(Dafny.ISequence<Dafny.Rune> i) {
       return ((((new BigInteger((i).Count)).Sign == 1) && (!(Defs.__default.has__special(i)))) && (!(Defs.__default.reserved__rust).Contains(i))) && (!(Defs.__default.reserved__rust__need__prefix).Contains(i));
@@ -99,7 +99,7 @@ public static bool is__idiomatic__rust__id(Dafny.ISequence<Dafny.Rune> i) {
       } else if (Defs.__default.is__tuple__builder(i)) {
         return Defs.__default.better__tuple__builder__name(i);
       } else if (((i).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("self"))) || ((i).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Self")))) {
-        return Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("r#_"), i);
+        return Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_"), i);
       } else if ((Defs.__default.reserved__rust).Contains(i)) {
         return Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("r#"), i);
       } else if (Defs.__default.is__idiomatic__rust__id(i)) {
@@ -108,7 +108,7 @@ public static bool is__idiomatic__rust__id(Dafny.ISequence<Dafny.Rune> i) {
         return i;
       } else {
         Dafny.ISequence<Dafny.Rune> _0_r = Defs.__default.replaceDots(i);
-        return Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("r#_"), _0_r);
+        return Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_"), _0_r);
       }
     }
     public static Dafny.ISequence<Dafny.Rune> escapeVar(Dafny.ISequence<Dafny.Rune> f) {
diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/system/mod.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/system/mod.rs
index d30d8671ec..eb25b8a8c4 100644
--- a/Source/DafnyRuntime/DafnyRuntimeRust/src/system/mod.rs
+++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/system/mod.rs
@@ -64,8 +64,8 @@ pub mod _System {
   }
 
   impl<T0: DafnyType, T1: DafnyType> Tuple2<T0, T1> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple2<T0, T1>) -> Tuple2<r#__T0, r#__T1>> {
-      Rc::new(move |this: Self| -> Tuple2<r#__T0, r#__T1>{
+    pub fn coerce<__T0: DafnyType, __T1: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple2<T0, T1>) -> Tuple2<__T0, __T1>> {
+      Rc::new(move |this: Self| -> Tuple2<__T0, __T1>{
           match this {
             Tuple2::_T2{_0, _1, } => {
               Tuple2::_T2 {
@@ -207,8 +207,8 @@ pub mod _System {
   }
 
   impl<T0: DafnyType> Tuple1<T0> {
-    pub fn coerce<r#__T0: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple1<T0>) -> Tuple1<r#__T0>> {
-      Rc::new(move |this: Self| -> Tuple1<r#__T0>{
+    pub fn coerce<__T0: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple1<T0>) -> Tuple1<__T0>> {
+      Rc::new(move |this: Self| -> Tuple1<__T0>{
           match this {
             Tuple1::_T1{_0, } => {
               Tuple1::_T1 {
@@ -303,8 +303,8 @@ pub mod _System {
   }
 
   impl<T0: DafnyType, T1: DafnyType, T2: DafnyType> Tuple3<T0, T1, T2> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple3<T0, T1, T2>) -> Tuple3<r#__T0, r#__T1, r#__T2>> {
-      Rc::new(move |this: Self| -> Tuple3<r#__T0, r#__T1, r#__T2>{
+    pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple3<T0, T1, T2>) -> Tuple3<__T0, __T1, __T2>> {
+      Rc::new(move |this: Self| -> Tuple3<__T0, __T1, __T2>{
           match this {
             Tuple3::_T3{_0, _1, _2, } => {
               Tuple3::_T3 {
@@ -413,8 +413,8 @@ pub mod _System {
   }
 
   impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType> Tuple4<T0, T1, T2, T3> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple4<T0, T1, T2, T3>) -> Tuple4<r#__T0, r#__T1, r#__T2, r#__T3>> {
-      Rc::new(move |this: Self| -> Tuple4<r#__T0, r#__T1, r#__T2, r#__T3>{
+    pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple4<T0, T1, T2, T3>) -> Tuple4<__T0, __T1, __T2, __T3>> {
+      Rc::new(move |this: Self| -> Tuple4<__T0, __T1, __T2, __T3>{
           match this {
             Tuple4::_T4{_0, _1, _2, _3, } => {
               Tuple4::_T4 {
@@ -534,8 +534,8 @@ pub mod _System {
   }
 
   impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType> Tuple5<T0, T1, T2, T3, T4> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple5<T0, T1, T2, T3, T4>) -> Tuple5<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4>> {
-      Rc::new(move |this: Self| -> Tuple5<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4>{
+    pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple5<T0, T1, T2, T3, T4>) -> Tuple5<__T0, __T1, __T2, __T3, __T4>> {
+      Rc::new(move |this: Self| -> Tuple5<__T0, __T1, __T2, __T3, __T4>{
           match this {
             Tuple5::_T5{_0, _1, _2, _3, _4, } => {
               Tuple5::_T5 {
@@ -666,8 +666,8 @@ pub mod _System {
   }
 
   impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType> Tuple6<T0, T1, T2, T3, T4, T5> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple6<T0, T1, T2, T3, T4, T5>) -> Tuple6<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5>> {
-      Rc::new(move |this: Self| -> Tuple6<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5>{
+    pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple6<T0, T1, T2, T3, T4, T5>) -> Tuple6<__T0, __T1, __T2, __T3, __T4, __T5>> {
+      Rc::new(move |this: Self| -> Tuple6<__T0, __T1, __T2, __T3, __T4, __T5>{
           match this {
             Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => {
               Tuple6::_T6 {
@@ -809,8 +809,8 @@ pub mod _System {
   }
 
   impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType> Tuple7<T0, T1, T2, T3, T4, T5, T6> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple7<T0, T1, T2, T3, T4, T5, T6>) -> Tuple7<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6>> {
-      Rc::new(move |this: Self| -> Tuple7<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6>{
+    pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple7<T0, T1, T2, T3, T4, T5, T6>) -> Tuple7<__T0, __T1, __T2, __T3, __T4, __T5, __T6>> {
+      Rc::new(move |this: Self| -> Tuple7<__T0, __T1, __T2, __T3, __T4, __T5, __T6>{
           match this {
             Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => {
               Tuple7::_T7 {
@@ -963,8 +963,8 @@ pub mod _System {
   }
 
   impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType> Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple8<T0, T1, T2, T3, T4, T5, T6, T7>) -> Tuple8<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7>> {
-      Rc::new(move |this: Self| -> Tuple8<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7>{
+    pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple8<T0, T1, T2, T3, T4, T5, T6, T7>) -> Tuple8<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7>> {
+      Rc::new(move |this: Self| -> Tuple8<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7>{
           match this {
             Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => {
               Tuple8::_T8 {
@@ -1128,8 +1128,8 @@ pub mod _System {
   }
 
   impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType> Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType, r#__T8: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> r#__T8 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8>) -> Tuple9<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8>> {
-      Rc::new(move |this: Self| -> Tuple9<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8>{
+    pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8>) -> Tuple9<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8>> {
+      Rc::new(move |this: Self| -> Tuple9<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8>{
           match this {
             Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => {
               Tuple9::_T9 {
@@ -1304,8 +1304,8 @@ pub mod _System {
   }
 
   impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType> Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType, r#__T8: DafnyType, r#__T9: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> r#__T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> r#__T9 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9>) -> Tuple10<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9>> {
-      Rc::new(move |this: Self| -> Tuple10<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9>{
+    pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9>) -> Tuple10<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9>> {
+      Rc::new(move |this: Self| -> Tuple10<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9>{
           match this {
             Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => {
               Tuple10::_T10 {
@@ -1491,8 +1491,8 @@ pub mod _System {
   }
 
   impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType> Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType, r#__T8: DafnyType, r#__T9: DafnyType, r#__T10: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> r#__T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> r#__T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> r#__T10 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10>) -> Tuple11<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10>> {
-      Rc::new(move |this: Self| -> Tuple11<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10>{
+    pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10>) -> Tuple11<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10>> {
+      Rc::new(move |this: Self| -> Tuple11<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10>{
           match this {
             Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => {
               Tuple11::_T11 {
@@ -1689,8 +1689,8 @@ pub mod _System {
   }
 
   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> Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType, r#__T8: DafnyType, r#__T9: DafnyType, r#__T10: DafnyType, r#__T11: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> r#__T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> r#__T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> r#__T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> r#__T11 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11>) -> Tuple12<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11>> {
-      Rc::new(move |this: Self| -> Tuple12<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11>{
+    pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11>) -> Tuple12<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11>> {
+      Rc::new(move |this: Self| -> Tuple12<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11>{
           match this {
             Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => {
               Tuple12::_T12 {
@@ -1898,8 +1898,8 @@ pub mod _System {
   }
 
   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> Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType, r#__T8: DafnyType, r#__T9: DafnyType, r#__T10: DafnyType, r#__T11: DafnyType, r#__T12: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> r#__T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> r#__T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> r#__T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> r#__T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> r#__T12 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12>) -> Tuple13<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12>> {
-      Rc::new(move |this: Self| -> Tuple13<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12>{
+    pub fn coerce<__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>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12>) -> Tuple13<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12>> {
+      Rc::new(move |this: Self| -> Tuple13<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12>{
           match this {
             Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => {
               Tuple13::_T13 {
@@ -2118,8 +2118,8 @@ pub mod _System {
   }
 
   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> Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType, r#__T8: DafnyType, r#__T9: DafnyType, r#__T10: DafnyType, r#__T11: DafnyType, r#__T12: DafnyType, r#__T13: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> r#__T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> r#__T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> r#__T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> r#__T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> r#__T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> r#__T13 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13>) -> Tuple14<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13>> {
-      Rc::new(move |this: Self| -> Tuple14<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13>{
+    pub fn coerce<__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>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13>) -> Tuple14<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13>> {
+      Rc::new(move |this: Self| -> Tuple14<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13>{
           match this {
             Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => {
               Tuple14::_T14 {
@@ -2349,8 +2349,8 @@ pub mod _System {
   }
 
   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> Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType, r#__T8: DafnyType, r#__T9: DafnyType, r#__T10: DafnyType, r#__T11: DafnyType, r#__T12: DafnyType, r#__T13: DafnyType, r#__T14: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> r#__T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> r#__T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> r#__T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> r#__T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> r#__T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> r#__T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> r#__T14 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14>) -> Tuple15<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13, r#__T14>> {
-      Rc::new(move |this: Self| -> Tuple15<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13, r#__T14>{
+    pub fn coerce<__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>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> __T14 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14>) -> Tuple15<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14>> {
+      Rc::new(move |this: Self| -> Tuple15<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14>{
           match this {
             Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => {
               Tuple15::_T15 {
@@ -2591,8 +2591,8 @@ pub mod _System {
   }
 
   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> Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType, r#__T8: DafnyType, r#__T9: DafnyType, r#__T10: DafnyType, r#__T11: DafnyType, r#__T12: DafnyType, r#__T13: DafnyType, r#__T14: DafnyType, r#__T15: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> r#__T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> r#__T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> r#__T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> r#__T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> r#__T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> r#__T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> r#__T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> r#__T15 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15>) -> Tuple16<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13, r#__T14, r#__T15>> {
-      Rc::new(move |this: Self| -> Tuple16<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13, r#__T14, r#__T15>{
+    pub fn coerce<__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>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> __T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> __T15 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15>) -> Tuple16<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15>> {
+      Rc::new(move |this: Self| -> Tuple16<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15>{
           match this {
             Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => {
               Tuple16::_T16 {
@@ -2844,8 +2844,8 @@ pub mod _System {
   }
 
   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> Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType, r#__T8: DafnyType, r#__T9: DafnyType, r#__T10: DafnyType, r#__T11: DafnyType, r#__T12: DafnyType, r#__T13: DafnyType, r#__T14: DafnyType, r#__T15: DafnyType, r#__T16: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> r#__T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> r#__T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> r#__T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> r#__T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> r#__T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> r#__T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> r#__T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> r#__T15 + 'static>, f_16: Rc<impl ::std::ops::Fn(T16) -> r#__T16 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16>) -> Tuple17<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13, r#__T14, r#__T15, r#__T16>> {
-      Rc::new(move |this: Self| -> Tuple17<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13, r#__T14, r#__T15, r#__T16>{
+    pub fn coerce<__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>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> __T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> __T15 + 'static>, f_16: Rc<impl ::std::ops::Fn(T16) -> __T16 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16>) -> Tuple17<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16>> {
+      Rc::new(move |this: Self| -> Tuple17<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16>{
           match this {
             Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => {
               Tuple17::_T17 {
@@ -3108,8 +3108,8 @@ pub mod _System {
   }
 
   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> Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType, r#__T8: DafnyType, r#__T9: DafnyType, r#__T10: DafnyType, r#__T11: DafnyType, r#__T12: DafnyType, r#__T13: DafnyType, r#__T14: DafnyType, r#__T15: DafnyType, r#__T16: DafnyType, r#__T17: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> r#__T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> r#__T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> r#__T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> r#__T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> r#__T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> r#__T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> r#__T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> r#__T15 + 'static>, f_16: Rc<impl ::std::ops::Fn(T16) -> r#__T16 + 'static>, f_17: Rc<impl ::std::ops::Fn(T17) -> r#__T17 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17>) -> Tuple18<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13, r#__T14, r#__T15, r#__T16, r#__T17>> {
-      Rc::new(move |this: Self| -> Tuple18<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13, r#__T14, r#__T15, r#__T16, r#__T17>{
+    pub fn coerce<__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>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> __T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> __T15 + 'static>, f_16: Rc<impl ::std::ops::Fn(T16) -> __T16 + 'static>, f_17: Rc<impl ::std::ops::Fn(T17) -> __T17 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17>) -> Tuple18<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17>> {
+      Rc::new(move |this: Self| -> Tuple18<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17>{
           match this {
             Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => {
               Tuple18::_T18 {
@@ -3383,8 +3383,8 @@ pub mod _System {
   }
 
   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> Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType, r#__T8: DafnyType, r#__T9: DafnyType, r#__T10: DafnyType, r#__T11: DafnyType, r#__T12: DafnyType, r#__T13: DafnyType, r#__T14: DafnyType, r#__T15: DafnyType, r#__T16: DafnyType, r#__T17: DafnyType, r#__T18: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> r#__T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> r#__T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> r#__T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> r#__T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> r#__T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> r#__T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> r#__T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> r#__T15 + 'static>, f_16: Rc<impl ::std::ops::Fn(T16) -> r#__T16 + 'static>, f_17: Rc<impl ::std::ops::Fn(T17) -> r#__T17 + 'static>, f_18: Rc<impl ::std::ops::Fn(T18) -> r#__T18 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18>) -> Tuple19<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13, r#__T14, r#__T15, r#__T16, r#__T17, r#__T18>> {
-      Rc::new(move |this: Self| -> Tuple19<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13, r#__T14, r#__T15, r#__T16, r#__T17, r#__T18>{
+    pub fn coerce<__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>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> __T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> __T15 + 'static>, f_16: Rc<impl ::std::ops::Fn(T16) -> __T16 + 'static>, f_17: Rc<impl ::std::ops::Fn(T17) -> __T17 + 'static>, f_18: Rc<impl ::std::ops::Fn(T18) -> __T18 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18>) -> Tuple19<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18>> {
+      Rc::new(move |this: Self| -> Tuple19<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18>{
           match this {
             Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => {
               Tuple19::_T19 {
@@ -3669,8 +3669,8 @@ pub mod _System {
   }
 
   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> Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {
-    pub fn coerce<r#__T0: DafnyType, r#__T1: DafnyType, r#__T2: DafnyType, r#__T3: DafnyType, r#__T4: DafnyType, r#__T5: DafnyType, r#__T6: DafnyType, r#__T7: DafnyType, r#__T8: DafnyType, r#__T9: DafnyType, r#__T10: DafnyType, r#__T11: DafnyType, r#__T12: DafnyType, r#__T13: DafnyType, r#__T14: DafnyType, r#__T15: DafnyType, r#__T16: DafnyType, r#__T17: DafnyType, r#__T18: DafnyType, r#__T19: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> r#__T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> r#__T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> r#__T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> r#__T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> r#__T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> r#__T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> r#__T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> r#__T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> r#__T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> r#__T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> r#__T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> r#__T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> r#__T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> r#__T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> r#__T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> r#__T15 + 'static>, f_16: Rc<impl ::std::ops::Fn(T16) -> r#__T16 + 'static>, f_17: Rc<impl ::std::ops::Fn(T17) -> r#__T17 + 'static>, f_18: Rc<impl ::std::ops::Fn(T18) -> r#__T18 + 'static>, f_19: Rc<impl ::std::ops::Fn(T19) -> r#__T19 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19>) -> Tuple20<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13, r#__T14, r#__T15, r#__T16, r#__T17, r#__T18, r#__T19>> {
-      Rc::new(move |this: Self| -> Tuple20<r#__T0, r#__T1, r#__T2, r#__T3, r#__T4, r#__T5, r#__T6, r#__T7, r#__T8, r#__T9, r#__T10, r#__T11, r#__T12, r#__T13, r#__T14, r#__T15, r#__T16, r#__T17, r#__T18, r#__T19>{
+    pub fn coerce<__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>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> __T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> __T15 + 'static>, f_16: Rc<impl ::std::ops::Fn(T16) -> __T16 + 'static>, f_17: Rc<impl ::std::ops::Fn(T17) -> __T17 + 'static>, f_18: Rc<impl ::std::ops::Fn(T18) -> __T18 + 'static>, f_19: Rc<impl ::std::ops::Fn(T19) -> __T19 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19>) -> Tuple20<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18, __T19>> {
+      Rc::new(move |this: Self| -> Tuple20<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18, __T19>{
           match this {
             Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => {
               Tuple20::_T20 {