diff --git a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs
index aa6e8068dba..396055b1853 100644
--- a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs
+++ b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs
@@ -188,7 +188,7 @@ public void AddMethod(DAST.Method item) {
     }
 
     public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
-      throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
+      parent.AddUnsupported("var/const for trait - " + item.dtor_name);
     }
 
     public object Finish() {
@@ -240,11 +240,11 @@ public NewtypeBuilder(NewtypeContainer parent, string name, List<TypeArgDecl> ty
     }
 
     public void AddMethod(DAST.Method item) {
-      throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
+      parent.AddUnsupported("method for newtypes - " + item.dtor_name);
     }
 
     public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
-      throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
+      parent.AddUnsupported("const for newtypes - " + item.dtor_name);
     }
 
     public object Finish() {
@@ -344,7 +344,7 @@ public void AddMethod(DAST.Method item) {
     }
 
     public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
-      throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
+      parent.AddUnsupported("const for datatypes - " + item.dtor_name);
     }
 
     public object Finish() {
diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
index 45a3bda471a..79f7a064ae9 100644
--- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
@@ -1578,12 +1578,13 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) {
     }
 
     protected override void EmitStringLiteral(string str, bool isVerbatim, ConcreteSyntaxTree wr) {
-      throw new UnsupportedInvalidOperationException("<i>EmitStringLiteral</i>");
+      AddUnsupported("EmitStringLiteral");
     }
 
     protected override ConcreteSyntaxTree EmitBitvectorTruncation(BitvectorType bvType, [CanBeNull] NativeType nativeType,
       bool surroundByUnchecked, ConcreteSyntaxTree wr) {
-      throw new UnsupportedInvalidOperationException("<i>EmitBitvectorTruncation</i>");
+      AddUnsupported("EmitBitvectorTruncation");
+      return wr;
     }
 
     protected override void EmitRotate(Expression e0, Expression e1, bool isRotateLeft, ConcreteSyntaxTree wr,
diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy
index 1ba1e84e853..7f2623cca51 100644
--- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy
+++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy
@@ -37,14 +37,16 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
      (|i| == 3 && i[2] in "0123456789"))
   }
 
+  // Given a Dafny-expanded fully qualified name with # or ., where ' has been replaced by _k, ? by _q and _ by __
+  // detect if there are of the strings above
   predicate has_special(i: string) {
     if |i| == 0 then false
     else if i[0] == '.' then true
     else if i[0] == '#' then true // otherwise "escapeName("r#") becomes "r#""
     else if i[0] == '_' then
       if 2 <= |i| then
-        if i[1] != '_' then true
-        else has_special(i[2..])
+        if i[1] == '_' then has_special(i[2..])
+        else true
       else
         true
     else
@@ -88,6 +90,7 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
 
   predicate is_dafny_generated_id(i: string) {
     && |i| > 0 && i[0] == '_' && !has_special(i[1..])
+    && (i != "_self" && i != "_Self")
     && (|i| >= 2 ==> i[1] != 'T') // To avoid conflict with tuple builders _T<digits>
   }
 
@@ -101,21 +104,21 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
   }
 
   function escapeIdent(i: string): string {
-    if is_tuple_numeric(i) then
+    if is_tuple_numeric(i) then // _42 remains the same
       i
-    else if is_tuple_builder(i) then
+    else if is_tuple_builder(i) then // ___hMake42 becomes _T42
       better_tuple_builder_name(i)
-    else if i == "self" || i == "Self" then
-      "r#_" + i
+    else if i == "self" || i == "Self" then // self becomes _self
+      "_" + i
     else if i in reserved_rust then
       "r#" + i
-    else if is_idiomatic_rust_id(i) then
+    else if is_idiomatic_rust_id(i) then // some__id becomes some_id
       idiomatic_rust(i)
-    else if is_dafny_generated_id(i) then
+    else if is_dafny_generated_id(i) then // _module remains _module
       i // Dafny-generated identifiers like "_module", cannot be written in Dafny itself
-    else
+    else // u16 becomes _u16, namespace.IsSomething_q becomes _namespace_dIsSomething_q
       var r := replaceDots(i);
-      "r#_" + r
+      "_" + r
   }
 
   // To be used when escaping variables
diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy
index 611bb413f02..71b556ccb7c 100644
--- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy
+++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy
@@ -88,15 +88,25 @@ module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs {
     else
     if i[0] == '_' then
       |i| >= 2 &&
-      i[1] in "_qkh" && IsDafnyEncodedIdTail(i[2..])
+      i[1] in ESCAPING && IsDafnyEncodedIdTail(i[2..])
     else
-      i[0] in "aqkhd." &&
+      (i[0] in SAMPLE_LETTERS || i[0] == '.') &&
       IsDafnyEncodedIdTail(i[1..])
   }
 
-  predicate IsDafnyEncodedId(i: string) {
-    if |i| == 0 then true
-    else i[0] in "aqkhd" && IsDafnyEncodedIdTail(i[1..])
+  // Subset of characters supported in Dafny identifiers, for proof purposes
+  const SAMPLE_LETTERS := "aqkhd"
+
+  // Letters that can come after a "_" in Dafny identifiers
+  // __ => _
+  // _q => ?
+  // _k => '
+  // _h => #
+  const ESCAPING := "_qkh"
+
+  ghost predicate IsDafnyEncodedId(i: string) {
+    if |i| == 0 then false
+    else i[0] in SAMPLE_LETTERS && IsDafnyEncodedIdTail(i[1..])
   }
 
   lemma DafnyEscapeCorrect(s: string)
@@ -194,7 +204,7 @@ module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs {
     ensures escapeIdent("_m") == "_m" // any hidden variable
     ensures escapeIdent("___hMake1") == "_T1" // tuple deconstructor
     ensures escapeIdent("h__w") == "h_w" // only letters and underscore
-    ensures escapeIdent("h_kw") == "r#_h_kw" //contains special char
+    ensures escapeIdent("h_kw") == "_h_kw" //contains special char
     ensures escapeIdent("fn") == "r#fn" // Keyword
   {
     assert has_special("h_kw");
@@ -225,26 +235,26 @@ module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs {
   }
 
   function UnescapeIdent(s: string): string {
-    if |s| >= 2 && s[0..2] == "r#" then
-      if |s| >= 3 && s[2] == '_' then
-        ReverseReplaceDots(s[3..]) // General escape
-      else
-        s[2..] // Keyword
-    else if |s| >= 1 && s[0] == '_' then
-      if |s| >= 2 && s[1] == 'T' then
-        "___hMake" + s[2..] // Tuple builder
-      else if is_tuple_numeric(s) then
+    if |s| >= 1 && s[0] == '_' then
+      if is_tuple_numeric(s) then
         s
+      else if |s| >= 2 && s[1] == 'T' then
+        "___hMake" + s[2..] // Tuple builder
+      else if s == "_self" || s == "_Self" then
+        s[1..]
       else
-        s
+        ReverseReplaceDots(s[1..]) // We remove the extra "_" prefix and place dots again
+    else if |s| >= 2 && s[0..2] == "r#" then
+      s[2..] // Reserved identifier
     else // Idiomatic rust
       ReverseIdiomaticRust(s)
   }
 
-  lemma TupleIdentInvertible(s: string)
-    requires is_tuple_numeric(s)
-    ensures UnescapeIdent(escapeIdent(s)) == s
-  {}
+  lemma TupleIdentInvertible(i: string)
+    requires is_tuple_numeric(i)
+    ensures UnescapeIdent(escapeIdent(i)) == i
+  {
+  }
 
   lemma {:rlimit 500} TupleBuilderInvertible(i: string)
     requires !is_tuple_numeric(i)
@@ -302,14 +312,24 @@ module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs {
     }
   }
 
-  lemma {:rlimit 800} EscapeIdentInvertibleForDafnyGeneratedId(s: string)
-    requires !is_tuple_numeric(s)
-    requires !is_tuple_builder(s)
-    requires s !in reserved_rust
-    requires !is_idiomatic_rust_id(s)
-    requires is_dafny_generated_id(s)
-    ensures UnescapeIdent(escapeIdent(s)) == s
+  lemma {:rlimit 800} EscapeIdentInvertibleForDafnyGeneratedId(i: string)
+    requires IsDafnyEncodedId(i)
+    requires !is_tuple_numeric(i)
+    requires !is_tuple_builder(i)
+    requires i !in reserved_rust
+    requires !is_idiomatic_rust_id(i)
+    requires is_dafny_generated_id(i)
+    ensures UnescapeIdent(escapeIdent(i)) == i
   {
+    assert escapeIdent(i) == i;
+    var s := i;
+    assert |s| >= 1 && s[0] == '_';
+    assert !(|s| >= 2 && s[1] == 'T');
+    assert !(s == "_self" || s == "_Self");
+    calc {
+      UnescapeIdent(s);
+      s;
+    }
   }
 
   lemma {:rlimit 800} EverythingElseInvertible(i: string)
@@ -322,16 +342,24 @@ module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs {
     ensures UnescapeIdent(escapeIdent(i)) == i
   {
     var r := replaceDots(i);
-    var s := "r#_" + r;
-    assert |s| >= 2 && s[0..2] == "r#";
-    assert |s| >= 3 && s[2] == '_';
-    assert s[3..] == r;
-    calc {
-      UnescapeIdent(escapeIdent(i));
-      UnescapeIdent(s);
-      ReverseReplaceDots(replaceDots(i));
-      { ReplaceDotsInvertible(i); }
-      i;
+    var s := "_" + r;
+    assert escapeIdent(i) == s;
+    assert |s| >= 1 && s[0] == '_';
+    assert !(|s| >= 2 && s[1] == 'T');
+    assert !(s == "_self" || s == "_Self");
+    assert |i| > 0;
+    if i[0] == '_' {
+      assert i[0] == '_'; // So if i[0] is not '_'
+      assert UnescapeIdent(escapeIdent(i)) == i;
+    } else {
+      calc {
+        UnescapeIdent(s);
+        ReverseReplaceDots(s[1..]);
+        ReverseReplaceDots(r);
+        ReverseReplaceDots(replaceDots(i));
+        { ReplaceDotsInvertible(i); }
+        i;
+      }
     }
   }
 
diff --git a/Source/DafnyCore/GeneratedFromDafny/Defs.cs b/Source/DafnyCore/GeneratedFromDafny/Defs.cs
index bf93664d1ef..c8d2bc4c9ac 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 d30d8671ec0..eb25b8a8c4b 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 {