diff --git a/Source/DafnyCore/AST/Printer.cs b/Source/DafnyCore/AST/Printer.cs
index 31920d943c6..23263fa7aee 100644
--- a/Source/DafnyCore/AST/Printer.cs
+++ b/Source/DafnyCore/AST/Printer.cs
@@ -656,8 +656,7 @@ public void PrintMembers(List<MemberDecl> members, int indent, string fileBeingP
         } else if (m is Function) {
           if (state != 0) { wr.WriteLine(); }
           PrintFunction((Function)m, indent, false);
-          var fixp = m as ExtremePredicate;
-          if (fixp != null && fixp.PrefixPredicate != null) {
+          if (m is ExtremePredicate fixp && fixp.PrefixPredicate != null) {
             Indent(indent); wr.WriteLine("/*** (note, what is printed here does not show substitutions of calls to prefix predicates)");
             PrintFunction(fixp.PrefixPredicate, indent, false);
             Indent(indent); wr.WriteLine("***/");
diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs
index f18d6efc36a..588e928d43d 100644
--- a/Source/DafnyCore/AST/TopLevelDeclarations.cs
+++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs
@@ -135,7 +135,6 @@ public override string ToString() {
   public IToken NameToken => tok;
   public virtual IEnumerable<INode> Children {
     get {
-
       return Enumerable.Empty<INode>();
     }
   }
@@ -352,6 +351,11 @@ public ModuleDecl(IToken tok, string name, ModuleDefinition parent, bool opened,
   public abstract object Dereference();
 
   public int? ResolvedHash { get; set; }
+
+  public override bool IsEssentiallyEmpty() {
+    // A module or import is considered "essentially empty" to its parents, but the module is going to be resolved by itself.
+    return true;
+  }
 }
 // Represents module X { ... }
 public class LiteralModuleDecl : ModuleDecl {
@@ -837,26 +841,37 @@ public static IEnumerable<TopLevelDeclWithMembers> AllTypesWithMembers(List<TopL
   /// declarations.
   /// Note, an iterator declaration is a type, in this sense.
   /// Note, if the given list are the top-level declarations of a module, the yield will include
-  /// greatest lemmas but not their associated prefix lemmas (which are tucked into the greatest lemma's
-  /// .PrefixLemma field).
+  /// extreme predicates/lemmas but not their associated prefix predicates/lemmas (which are tucked
+  /// into the extreme predicate/lemma's PrefixPredicate/PrefixLemma field).
   /// </summary>
   public static IEnumerable<ICallable> AllCallables(List<TopLevelDecl> declarations) {
     foreach (var d in declarations) {
-      var cl = d as TopLevelDeclWithMembers;
-      if (cl != null) {
-        foreach (var member in cl.Members) {
-          var clbl = member as ICallable;
-          if (clbl != null && !(member is ConstantField)) {
-            yield return clbl;
-            if (clbl is Function f && f.ByMethodDecl != null) {
-              yield return f.ByMethodDecl;
-            }
+      if (d is TopLevelDeclWithMembers cl) {
+        foreach (var member in cl.Members.Where(member => member is ICallable and not ConstantField)) {
+          yield return (ICallable)member;
+          if (member is Function { ByMethodDecl: { } } f) {
+            yield return f.ByMethodDecl;
           }
         }
       }
     }
   }
 
+  /// <summary>
+  /// Yields all functions and methods that are members of some type in the given list of
+  /// declarations, including prefix lemmas and prefix predicates.
+  /// </summary>
+  public static IEnumerable<ICallable> AllCallablesIncludingPrefixDeclarations(List<TopLevelDecl> declarations) {
+    foreach (var decl in AllCallables(declarations)) {
+      yield return decl;
+      if (decl is ExtremeLemma extremeLemma) {
+        yield return extremeLemma.PrefixLemma;
+      } else if (decl is ExtremePredicate extremePredicate) {
+        yield return extremePredicate.PrefixPredicate;
+      }
+    }
+  }
+
   /// <summary>
   /// Yields all functions and methods that are members of some non-iterator type in the given
   /// list of declarations, as well as any IteratorDecl's in that list.
@@ -864,17 +879,12 @@ public static IEnumerable<ICallable> AllCallables(List<TopLevelDecl> declaration
   public static IEnumerable<ICallable> AllItersAndCallables(List<TopLevelDecl> declarations) {
     foreach (var d in declarations) {
       if (d is IteratorDecl) {
-        var iter = (IteratorDecl)d;
-        yield return iter;
-      } else if (d is TopLevelDeclWithMembers) {
-        var cl = (TopLevelDeclWithMembers)d;
-        foreach (var member in cl.Members) {
-          var clbl = member as ICallable;
-          if (clbl != null) {
-            yield return clbl;
-            if (clbl is Function f && f.ByMethodDecl != null) {
-              yield return f.ByMethodDecl;
-            }
+        yield return (IteratorDecl)d;
+      } else if (d is TopLevelDeclWithMembers cl) {
+        foreach (var member in cl.Members.Where(member => member is ICallable)) {
+          yield return (ICallable)member;
+          if (member is Function { ByMethodDecl: { } } f) {
+            yield return f.ByMethodDecl;
           }
         }
       }
@@ -883,8 +893,7 @@ public static IEnumerable<ICallable> AllItersAndCallables(List<TopLevelDecl> dec
 
   public static IEnumerable<IteratorDecl> AllIteratorDecls(List<TopLevelDecl> declarations) {
     foreach (var d in declarations) {
-      var iter = d as IteratorDecl;
-      if (iter != null) {
+      if (d is IteratorDecl iter) {
         yield return iter;
       }
     }
@@ -897,8 +906,7 @@ public static IEnumerable<IteratorDecl> AllIteratorDecls(List<TopLevelDecl> decl
   public static IEnumerable<TopLevelDecl> AllDeclarationsAndNonNullTypeDecls(List<TopLevelDecl> declarations) {
     foreach (var d in declarations) {
       yield return d;
-      var cl = d as ClassDecl;
-      if (cl != null && cl.NonNullTypeDecl != null) {
+      if (d is ClassDecl { NonNullTypeDecl: { } } cl) {
         yield return cl.NonNullTypeDecl;
       }
     }
@@ -906,12 +914,10 @@ public static IEnumerable<TopLevelDecl> AllDeclarationsAndNonNullTypeDecls(List<
 
   public static IEnumerable<ExtremeLemma> AllExtremeLemmas(List<TopLevelDecl> declarations) {
     foreach (var d in declarations) {
-      var cl = d as TopLevelDeclWithMembers;
-      if (cl != null) {
+      if (d is TopLevelDeclWithMembers cl) {
         foreach (var member in cl.Members) {
-          var m = member as ExtremeLemma;
-          if (m != null) {
-            yield return m;
+          if (member is ExtremeLemma extremeLemma) {
+            yield return extremeLemma;
           }
         }
       }
@@ -919,20 +925,7 @@ public static IEnumerable<ExtremeLemma> AllExtremeLemmas(List<TopLevelDecl> decl
   }
 
   public bool IsEssentiallyEmptyModuleBody() {
-    foreach (var d in TopLevelDecls) {
-      if (d is ModuleDecl) {
-        // modules don't count
-        continue;
-      } else if (d is ClassDecl) {
-        var cl = (ClassDecl)d;
-        if (cl.Members.Count == 0) {
-          // the class is empty, so it doesn't count
-          continue;
-        }
-      }
-      return false;
-    }
-    return true;
+    return TopLevelDecls.All(decl => decl.IsEssentiallyEmpty());
   }
 
   public IToken GetFirstTopLevelToken() {
@@ -1058,6 +1051,14 @@ public virtual List<Type> ParentTypes(List<Type> typeArgs) {
 
   public bool AllowsAllocation => true;
   public override IEnumerable<INode> Children => Enumerable.Empty<INode>();
+
+  /// <summary>
+  /// A top-level declaration is considered "essentially empty" if there is no way it could generate any resolution error
+  /// other than introducing a duplicate name.
+  /// </summary>
+  public virtual bool IsEssentiallyEmpty() {
+    return Attributes == null || TypeArgs.Count != 0;
+  }
 }
 
 public abstract class TopLevelDeclWithMembers : TopLevelDecl {
@@ -1183,6 +1184,13 @@ private void AddTraitAncestors(ISet<TraitDecl> s) {
   // True if non-static members can access the underlying object "this"
   // False if all members are implicitly static (e.g. in a default class declaration)
   public abstract bool AcceptThis { get; }
+
+  public override bool IsEssentiallyEmpty() {
+    if (Members.Count != 0 || ParentTraits.Count != 0) {
+      return false;
+    }
+    return base.IsEssentiallyEmpty();
+  }
 }
 
 public class TraitDecl : ClassDecl {
@@ -1395,6 +1403,14 @@ bool ICallable.InferredDecreases {
   }
 
   public abstract DatatypeCtor GetGroundingCtor();
+
+
+  public override bool IsEssentiallyEmpty() {
+    if (Ctors.Any(ctor => ctor.Attributes != null || ctor.Formals.Count != 0)) {
+      return false;
+    }
+    return base.IsEssentiallyEmpty();
+  }
 }
 
 public class IndDatatypeDecl : DatatypeDecl {
@@ -1971,6 +1987,11 @@ bool ICallable.InferredDecreases {
   }
 
   public override bool AcceptThis => true;
+
+  public override bool IsEssentiallyEmpty() {
+    // A "newtype" is not considered "essentially empty", because it always has a parent type to be resolved.
+    return false;
+  }
 }
 
 public abstract class TypeSynonymDeclBase : TopLevelDecl, RedirectingTypeDecl {
@@ -2059,6 +2080,11 @@ bool ICallable.InferredDecreases {
   public override bool CanBeRevealed() {
     return true;
   }
+
+  public override bool IsEssentiallyEmpty() {
+    // A synonym/subset type is not considered "essentially empty", because it always has a parent type to be resolved.
+    return false;
+  }
 }
 
 public class TypeSynonymDecl : TypeSynonymDeclBase, RevealableTypeDecl {
diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs
index adc966e884b..4fcb1be2677 100644
--- a/Source/DafnyCore/Resolver/Resolver.cs
+++ b/Source/DafnyCore/Resolver/Resolver.cs
@@ -2292,50 +2292,50 @@ void RegisterMembers(ModuleDefinition moduleDef, TopLevelDeclWithMembers cl,
             reporter.Info(MessageSource.Resolver, m.tok, string.Format("_k: {0}", k.Type));
             formals.Add(k);
             if (m is ExtremePredicate) {
-              var cop = (ExtremePredicate)m;
-              formals.AddRange(cop.Formals.ConvertAll(cloner.CloneFormal));
+              var extremePredicate = (ExtremePredicate)m;
+              formals.AddRange(extremePredicate.Formals.ConvertAll(cloner.CloneFormal));
 
-              List<TypeParameter> tyvars = cop.TypeArgs.ConvertAll(cloner.CloneTypeParam);
+              List<TypeParameter> tyvars = extremePredicate.TypeArgs.ConvertAll(cloner.CloneTypeParam);
 
               // create prefix predicate
-              cop.PrefixPredicate = new PrefixPredicate(cop.tok, extraName, cop.HasStaticKeyword,
+              extremePredicate.PrefixPredicate = new PrefixPredicate(extremePredicate.tok, extraName, extremePredicate.HasStaticKeyword,
                 tyvars, k, formals,
-                cop.Req.ConvertAll(cloner.CloneAttributedExpr),
-                cop.Reads.ConvertAll(cloner.CloneFrameExpr),
-                cop.Ens.ConvertAll(cloner.CloneAttributedExpr),
-                new Specification<Expression>(new List<Expression>() { new IdentifierExpr(cop.tok, k.Name) }, null),
-                cop.Body,
+                extremePredicate.Req.ConvertAll(cloner.CloneAttributedExpr),
+                extremePredicate.Reads.ConvertAll(cloner.CloneFrameExpr),
+                extremePredicate.Ens.ConvertAll(cloner.CloneAttributedExpr),
+                new Specification<Expression>(new List<Expression>() { new IdentifierExpr(extremePredicate.tok, k.Name) }, null),
+                cloner.CloneExpr(extremePredicate.Body),
                 null,
-                cop);
-              extraMember = cop.PrefixPredicate;
+                extremePredicate);
+              extraMember = extremePredicate.PrefixPredicate;
               // In the call graph, add an edge from P# to P, since this will have the desired effect of detecting unwanted cycles.
-              moduleDef.CallGraph.AddEdge(cop.PrefixPredicate, cop);
+              moduleDef.CallGraph.AddEdge(extremePredicate.PrefixPredicate, extremePredicate);
             } else {
-              var com = (ExtremeLemma)m;
+              var extremeLemma = (ExtremeLemma)m;
               // _k has already been added to 'formals', so append the original formals
-              formals.AddRange(com.Ins.ConvertAll(cloner.CloneFormal));
+              formals.AddRange(extremeLemma.Ins.ConvertAll(cloner.CloneFormal));
               // prepend _k to the given decreases clause
               var decr = new List<Expression>();
-              decr.Add(new IdentifierExpr(com.tok, k.Name));
-              decr.AddRange(com.Decreases.Expressions.ConvertAll(cloner.CloneExpr));
+              decr.Add(new IdentifierExpr(extremeLemma.tok, k.Name));
+              decr.AddRange(extremeLemma.Decreases.Expressions.ConvertAll(cloner.CloneExpr));
               // Create prefix lemma.  Note that the body is not cloned, but simply shared.
               // For a greatest lemma, the postconditions are filled in after the greatest lemma's postconditions have been resolved.
               // For a least lemma, the preconditions are filled in after the least lemma's preconditions have been resolved.
-              var req = com is GreatestLemma
-                ? com.Req.ConvertAll(cloner.CloneAttributedExpr)
+              var req = extremeLemma is GreatestLemma
+                ? extremeLemma.Req.ConvertAll(cloner.CloneAttributedExpr)
                 : new List<AttributedExpression>();
-              var ens = com is GreatestLemma
+              var ens = extremeLemma is GreatestLemma
                 ? new List<AttributedExpression>()
-                : com.Ens.ConvertAll(cloner.CloneAttributedExpr);
-              com.PrefixLemma = new PrefixLemma(com.tok, extraName, com.HasStaticKeyword,
-                com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal),
-                req, cloner.CloneSpecFrameExpr(com.Mod), ens,
+                : extremeLemma.Ens.ConvertAll(cloner.CloneAttributedExpr);
+              extremeLemma.PrefixLemma = new PrefixLemma(extremeLemma.tok, extraName, extremeLemma.HasStaticKeyword,
+                extremeLemma.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, extremeLemma.Outs.ConvertAll(cloner.CloneFormal),
+                req, cloner.CloneSpecFrameExpr(extremeLemma.Mod), ens,
                 new Specification<Expression>(decr, null),
                 null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the greatest lemma is known
-                cloner.CloneAttributes(com.Attributes), com);
-              extraMember = com.PrefixLemma;
+                cloner.CloneAttributes(extremeLemma.Attributes), extremeLemma);
+              extraMember = extremeLemma.PrefixLemma;
               // In the call graph, add an edge from M# to M, since this will have the desired effect of detecting unwanted cycles.
-              moduleDef.CallGraph.AddEdge(com.PrefixLemma, com);
+              moduleDef.CallGraph.AddEdge(extremeLemma.PrefixLemma, extremeLemma);
             }
 
             extraMember.InheritVisibility(m, false);
@@ -3036,7 +3036,9 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl/*!*/>/*!*/ declarations,
             }
           }
           reporter.Info(MessageSource.Resolver, com.tok,
-            string.Format("{0} with focal predicate{2} {1}", com.PrefixLemma.Name, Util.Comma(focalPredicates, p => p.Name), Util.Plural(focalPredicates.Count)));
+            focalPredicates.Count == 0 ?
+              $"{com.PrefixLemma.Name} has no focal predicates" :
+              $"{com.PrefixLemma.Name} with focal predicate{Util.Plural(focalPredicates.Count)} {Util.Comma(focalPredicates, p => p.Name)}");
           // Compute the statement body of the prefix lemma
           Contract.Assume(prefixLemma.Body == null);  // this is not supposed to have been filled in before
           if (com.Body != null) {
@@ -7722,8 +7724,7 @@ void ResolveClassMemberTypes(TopLevelDeclWithMembers cl) {
           ResolveTypeParameters(m.TypeArgs, true, m);
           ResolveMethodSignature(m);
           allTypeParameters.PopMarker();
-          var com = m as ExtremeLemma;
-          if (com != null && com.PrefixLemma != null && ec == reporter.Count(ErrorLevel.Error)) {
+          if (m is ExtremeLemma com && com.PrefixLemma != null && ec == reporter.Count(ErrorLevel.Error)) {
             var mm = com.PrefixLemma;
             // resolve signature of the prefix lemma
             mm.EnclosingClass = cl;
@@ -8787,8 +8788,7 @@ void ResolveMethod(Method m) {
 
         // Resolve body
         if (m.Body != null) {
-          var com = m as ExtremeLemma;
-          if (com != null && com.PrefixLemma != null) {
+          if (m is ExtremeLemma com && com.PrefixLemma != null) {
             // The body may mentioned the implicitly declared parameter _k.  Throw it into the
             // scope before resolving the body.
             var k = com.PrefixLemma.Ins[0];
diff --git a/Source/DafnyCore/Rewriter.cs b/Source/DafnyCore/Rewriter.cs
index 04d73c63227..8ff3f086f9d 100644
--- a/Source/DafnyCore/Rewriter.cs
+++ b/Source/DafnyCore/Rewriter.cs
@@ -158,7 +158,7 @@ internal TriggerGeneratingRewriter(ErrorReporter reporter) : base(reporter) {
     internal override void PostCyclicityResolve(ModuleDefinition m) {
       var finder = new Triggers.QuantifierCollector(Reporter);
 
-      foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
+      foreach (var decl in ModuleDefinition.AllCallablesIncludingPrefixDeclarations(m.TopLevelDecls)) {
         finder.Visit(decl, null);
       }
 
@@ -191,17 +191,10 @@ public ForallStmtRewriter(ErrorReporter reporter) : base(reporter) {
     }
 
     internal override void PostResolveIntermediate(ModuleDefinition m) {
-      var forallvisiter = new ForAllStmtVisitor(Reporter);
-      foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
-        forallvisiter.Visit(decl, true);
-        if (decl is ExtremeLemma) {
-          var prefixLemma = ((ExtremeLemma)decl).PrefixLemma;
-          if (prefixLemma != null) {
-            forallvisiter.Visit(prefixLemma, true);
-          }
-        }
+      var forallVisitor = new ForAllStmtVisitor(Reporter);
+      foreach (var decl in ModuleDefinition.AllCallablesIncludingPrefixDeclarations(m.TopLevelDecls)) {
+        forallVisitor.Visit(decl, true);
       }
-
     }
 
     internal class ForAllStmtVisitor : TopDownVisitor<bool> {
diff --git a/Source/DafnyCore/Substituter.cs b/Source/DafnyCore/Substituter.cs
index e9911430924..b353994c2f3 100644
--- a/Source/DafnyCore/Substituter.cs
+++ b/Source/DafnyCore/Substituter.cs
@@ -38,13 +38,19 @@ public virtual Expression Substitute(Expression expr) {
         return new StaticReceiverExpr(e.tok, ty, e.IsImplicit) { Type = ty };
       } else if (expr is LiteralExpr literalExpr) {
         if (literalExpr.Value == null) {
-          return new LiteralExpr(literalExpr.tok) { Type = literalExpr.Type.Subst(typeMap) };
+          var ty = literalExpr.Type.Subst(typeMap);
+          if (ty != literalExpr.Type) {
+            return new LiteralExpr(literalExpr.tok) { Type = ty };
+          }
         } else {
           // nothing to substitute
         }
       } else if (expr is Translator.BoogieWrapper) {
         var e = (Translator.BoogieWrapper)expr;
-        return new Translator.BoogieWrapper(e.Expr, e.Type.Subst(typeMap));
+        var ty = e.Type.Subst(typeMap);
+        if (ty != e.Type) {
+          return new Translator.BoogieWrapper(e.Expr, ty);
+        }
       } else if (expr is WildcardExpr) {
         // nothing to substitute
       } else if (expr is ThisExpr) {
@@ -74,7 +80,7 @@ public virtual Expression Substitute(Expression expr) {
       } else if (expr is DisplayExpression) {
         DisplayExpression e = (DisplayExpression)expr;
         List<Expression> newElements = SubstituteExprList(e.Elements);
-        if (newElements != e.Elements || !e.Type.Subst(typeMap).Equals(e.Type)) {
+        if (newElements != e.Elements || e.Type.Subst(typeMap) != e.Type) {
           if (expr is SetDisplayExpr) {
             newExpr = new SetDisplayExpr(expr.tok, ((SetDisplayExpr)expr).Finite, newElements);
           } else if (expr is MultiSetDisplayExpr) {
@@ -96,18 +102,25 @@ public virtual Expression Substitute(Expression expr) {
           }
         }
         var ty = e.Type.Subst(typeMap);
-        if (anyChanges || !ty.Equals(e.Type)) {
+        if (anyChanges || ty != e.Type) {
           newExpr = new MapDisplayExpr(expr.tok, e.Finite, elmts);
         }
       } else if (expr is MemberSelectExpr) {
         var mse = (MemberSelectExpr)expr;
-        Expression substE = Substitute(mse.Obj);
-        MemberSelectExpr fseNew = new MemberSelectExpr(mse.tok, substE, mse.MemberName);
-        fseNew.Member = mse.Member;
-        fseNew.TypeApplication_AtEnclosingClass = mse.TypeApplication_AtEnclosingClass.ConvertAll(t => t.Subst(typeMap));
-        fseNew.TypeApplication_JustMember = mse.TypeApplication_JustMember.ConvertAll(t => t.Subst(typeMap));
-        fseNew.AtLabel = mse.AtLabel ?? oldHeapLabel;
-        newExpr = fseNew;
+        var newObj = Substitute(mse.Obj);
+        var newTypeApplicationAtEnclosingClass = SubstituteTypeList(mse.TypeApplication_AtEnclosingClass);
+        var newTypeApplicationJustMember = SubstituteTypeList(mse.TypeApplication_JustMember);
+        if (newObj != mse.Obj ||
+            newTypeApplicationAtEnclosingClass != mse.TypeApplication_AtEnclosingClass ||
+            newTypeApplicationJustMember != mse.TypeApplication_JustMember) {
+          var fseNew = new MemberSelectExpr(mse.tok, newObj, mse.MemberName) {
+            Member = mse.Member,
+            TypeApplication_AtEnclosingClass = newTypeApplicationAtEnclosingClass,
+            TypeApplication_JustMember = newTypeApplicationJustMember,
+            AtLabel = mse.AtLabel ?? oldHeapLabel
+          };
+          newExpr = fseNew;
+        }
       } else if (expr is SeqSelectExpr) {
         SeqSelectExpr sse = (SeqSelectExpr)expr;
         Expression seq = Substitute(sse.Seq);
@@ -159,13 +172,14 @@ public virtual Expression Substitute(Expression expr) {
         newExpr = new ApplyExpr(e.tok, fn, args, e.CloseParen);
 
       } else if (expr is DatatypeValue) {
-        DatatypeValue dtv = (DatatypeValue)expr;
+        var dtv = (DatatypeValue)expr;
         var newArguments = SubstituteExprList(dtv.Bindings.Arguments); // substitute into the expressions, but drop any binding names (since those are no longer needed)
-        if (newArguments != dtv.Bindings.Arguments) {
-          DatatypeValue newDtv = new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArguments);
-          newDtv.Ctor = dtv.Ctor;  // resolve on the fly (and set newDtv.Type below, at end)
-          newDtv.InferredTypeArgs = Util.Map(dtv.InferredTypeArgs, tt => tt.Subst(typeMap));
-          // ^ Set the correct type arguments to the constructor
+        var newTypeArgs = SubstituteTypeList(dtv.InferredTypeArgs);
+        if (newArguments != dtv.Bindings.Arguments || newTypeArgs != dtv.InferredTypeArgs) {
+          var newDtv = new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArguments) {
+            Ctor = dtv.Ctor,
+            InferredTypeArgs = newTypeArgs
+          };
           newExpr = newDtv;
         }
 
@@ -212,29 +226,39 @@ public virtual Expression Substitute(Expression expr) {
       } else if (expr is BoxingCastExpr) {
         var e = (BoxingCastExpr)expr;
         var se = Substitute(e.E);
-        if (se != e.E) {
-          newExpr = new BoxingCastExpr(se, e.FromType, e.ToType);
+        var fromType = e.FromType.Subst(typeMap);
+        var toType = e.ToType.Subst(typeMap);
+        if (se != e.E || fromType != e.FromType || toType != e.ToType) {
+          newExpr = new BoxingCastExpr(se, fromType, toType);
         }
       } else if (expr is UnaryExpr) {
         var e = (UnaryExpr)expr;
-        Expression se = Substitute(e.E);
-        if (se != e.E) {
+        var se = Substitute(e.E);
+        if (e is TypeUnaryExpr typeUnaryExpr) {
+          var toType = typeUnaryExpr.ToType.Subst(typeMap);
+          if (se != e.E || toType != typeUnaryExpr.ToType) {
+            if (e is ConversionExpr) {
+              var ee = (ConversionExpr)e;
+              newExpr = new ConversionExpr(expr.tok, se, toType);
+            } else if (e is TypeTestExpr) {
+              var ee = (TypeTestExpr)e;
+              newExpr = new TypeTestExpr(expr.tok, se, toType);
+            } else {
+              Contract.Assert(false); // unexpected UnaryExpr subtype
+            }
+          }
+        } else if (se != e.E) {
           if (e is FreshExpr) {
             var ee = (FreshExpr)e;
             newExpr = new FreshExpr(expr.tok, se, ee.At) { AtLabel = ee.AtLabel ?? oldHeapLabel };
           } else if (e is UnaryOpExpr) {
             var ee = (UnaryOpExpr)e;
             newExpr = new UnaryOpExpr(expr.tok, ee.Op, se);
-          } else if (e is ConversionExpr) {
-            var ee = (ConversionExpr)e;
-            newExpr = new ConversionExpr(expr.tok, se, ee.ToType);
-          } else if (e is TypeTestExpr) {
-            var ee = (TypeTestExpr)e;
-            newExpr = new TypeTestExpr(expr.tok, se, ee.ToType);
           } else {
             Contract.Assert(false);  // unexpected UnaryExpr subtype
           }
         }
+
       } else if (expr is BinaryExpr) {
         BinaryExpr e = (BinaryExpr)expr;
         Expression e0 = Substitute(e.E0);
diff --git a/Source/DafnyCore/Triggers/QuantifiersCollection.cs b/Source/DafnyCore/Triggers/QuantifiersCollection.cs
index cc4a231a796..998e5732b0f 100644
--- a/Source/DafnyCore/Triggers/QuantifiersCollection.cs
+++ b/Source/DafnyCore/Triggers/QuantifiersCollection.cs
@@ -339,7 +339,7 @@ void FirstLetterCapitalOnNestedToken() {
 #endif
       }
 
-      if (msg.Length > 0) {
+      if (msg.Length > 0 && !Attributes.Contains(q.quantifier.Attributes, "auto_generated")) {
         var msgStr = msg.ToString().TrimEnd("\r\n ".ToCharArray());
         reporter.Message(MessageSource.Rewriter, errorLevel, reportingToken, msgStr);
       }
diff --git a/Test/dafny0/ErrorsInRelatedModules.dfy b/Test/dafny0/ErrorsInRelatedModules.dfy
index a424daecf97..cdd094ad950 100644
--- a/Test/dafny0/ErrorsInRelatedModules.dfy
+++ b/Test/dafny0/ErrorsInRelatedModules.dfy
@@ -58,3 +58,104 @@ module BadImportNames {
   }
   import MI = Middle.I  // error: there's no module called Middle.I
 }
+
+// --------------------------------------------------------------------------------
+
+module ModuleWithErrors {
+  datatype Packet = Packet(UndeclaredType)  // error: UndeclaredType
+}
+
+module ClientOfErroneousModule0 {
+  import ModuleWithErrors // error: not resolving this module, because of error in imported module
+  method M() {
+    var u: int := true; // no error is reported here
+  }
+}
+
+module ClientOfErroneousModule1 {
+  import ModuleWithErrors // no additional error reported here, because this module proper is empty
+}
+
+module ClientOfErroneousModule2 {
+  import ModuleWithErrors // error: not resolving this module, because of error in imported module
+  class C {
+    method M() {
+      var u: int := true; // no error is reported here
+    }
+  }
+}
+
+module ClientOfErroneousModule2' {
+  import ModuleWithErrors // no additional error reported here, because this module proper is empty
+  trait T { }
+  class C { }
+}
+
+module ClientOfErroneousModule2'' {
+  import ModuleWithErrors // error: not resolving this module, because of error in imported module
+  trait T { }
+  class C extends T { }
+}
+
+module ClientOfErroneousModule2'3 {
+  import ModuleWithErrors // error: not resolving this module, because of error in imported module
+  class C extends TraitThatDoesNotExist { }
+}
+
+module ClientOfErroneousModule3 {
+  import ModuleWithErrors // error: not resolving this module, because of error in imported module
+  datatype Color = Artic | Mint | Lilac
+  {
+    method M() {
+      var u: int := true; // no error is reported here
+    }
+  }
+}
+
+module ClientOfErroneousModule3' {
+  import ModuleWithErrors // no additional error reported here, because this module proper is empty
+  datatype Color = Artic | Mint | Lilac
+}
+
+module ClientOfErroneousModule3'' {
+  import ModuleWithErrors // error: not resolving this module, because of error in imported module
+  datatype Color = Artic | Mint(u: TypeDoesNotExist) | Lilac // no error reported here
+}
+
+module ClientOfErroneousModule4 {
+  import ModuleWithErrors // no additional error reported here, because this module proper is empty
+  module InnerModule {
+    method M() {
+      var u: int := true; // error: cannot assign bool to int
+    }
+  }
+}
+
+module ClientOfErroneousModule5 {
+  import ModuleWithErrors // error: not resolving this module, because of error in imported module
+  module InnerModule {
+    method M() {
+      var u: int := true; // error: cannot assign bool to int
+    }
+  }
+  newtype MyInt = int {
+    method M() {
+      var u: int := true; // no error is reported here
+    }
+  }
+}
+
+module ClientOfErroneousModule6 {
+  import ModuleWithErrors
+  trait EverythingHasTheSameName<X> { }
+  class EverythingHasTheSameName<X> { } // error: duplicate name
+  datatype EverythingHasTheSameName<X> = Y // error: duplicate name
+}
+
+module ClientOfErroneousModule7 {
+  import ModuleWithErrors // error: not resolving this module, because of error in imported module
+  trait A<X, X> { } // no error reported here
+  class B<Y, Y> { } // no error reported here
+  datatype C<Z, Z> = R // no error reported here
+}
+
diff --git a/Test/dafny0/ErrorsInRelatedModules.dfy.expect b/Test/dafny0/ErrorsInRelatedModules.dfy.expect
index 874bd47df06..86d2245eb63 100644
--- a/Test/dafny0/ErrorsInRelatedModules.dfy.expect
+++ b/Test/dafny0/ErrorsInRelatedModules.dfy.expect
@@ -6,4 +6,17 @@ ErrorsInRelatedModules.dfy(34,29): Error: Undeclared top-level type or type para
 ErrorsInRelatedModules.dfy(34,29): Error: Undeclared top-level type or type parameter: UndeclaredType (did you forget to qualify a name or declare a module import 'opened'?)
 ErrorsInRelatedModules.dfy(38,11): Error: not resolving module 'ClientModule' because there were errors in resolving its import 'T'
 ErrorsInRelatedModules.dfy(59,21): Error: module I does not exist (position 1 in path Middle.I)
-8 resolution/type errors detected in ErrorsInRelatedModules.dfy
+ErrorsInRelatedModules.dfy(65,27): Error: Undeclared top-level type or type parameter: UndeclaredType (did you forget to qualify a name or declare a module import 'opened'?)
+ErrorsInRelatedModules.dfy(69,9): Error: not resolving module 'ClientOfErroneousModule0' because there were errors in resolving its import 'ModuleWithErrors'
+ErrorsInRelatedModules.dfy(80,9): Error: not resolving module 'ClientOfErroneousModule2' because there were errors in resolving its import 'ModuleWithErrors'
+ErrorsInRelatedModules.dfy(95,9): Error: not resolving module 'ClientOfErroneousModule2''' because there were errors in resolving its import 'ModuleWithErrors'
+ErrorsInRelatedModules.dfy(101,9): Error: not resolving module 'ClientOfErroneousModule2'3' because there were errors in resolving its import 'ModuleWithErrors'
+ErrorsInRelatedModules.dfy(106,9): Error: not resolving module 'ClientOfErroneousModule3' because there were errors in resolving its import 'ModuleWithErrors'
+ErrorsInRelatedModules.dfy(121,9): Error: not resolving module 'ClientOfErroneousModule3''' because there were errors in resolving its import 'ModuleWithErrors'
+ErrorsInRelatedModules.dfy(129,17): Error: RHS (of type bool) not assignable to LHS (of type int)
+ErrorsInRelatedModules.dfy(138,17): Error: RHS (of type bool) not assignable to LHS (of type int)
+ErrorsInRelatedModules.dfy(135,9): Error: not resolving module 'ClientOfErroneousModule5' because there were errors in resolving its import 'ModuleWithErrors'
+ErrorsInRelatedModules.dfy(151,8): Error: duplicate name of top-level declaration: EverythingHasTheSameName
+ErrorsInRelatedModules.dfy(152,11): Error: duplicate name of top-level declaration: EverythingHasTheSameName
+ErrorsInRelatedModules.dfy(151,8): Error: a module that already contains a top-level declaration 'EverythingHasTheSameName?' is not allowed to declare a class 'EverythingHasTheSameName'
+21 resolution/type errors detected in ErrorsInRelatedModules.dfy
diff --git a/Test/dafny0/PrefixTypeSubst.dfy.expect b/Test/dafny0/PrefixTypeSubst.dfy.expect
index b06d54ed025..5466854f015 100644
--- a/Test/dafny0/PrefixTypeSubst.dfy.expect
+++ b/Test/dafny0/PrefixTypeSubst.dfy.expect
@@ -287,7 +287,7 @@ class MyClass<A, B> {
     if 0 < _k.Offset {
       L#[_k - 1](u, v);
     } else {
-      forall _k': ORDINAL, u: U, v: V /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} | _k' < _k
+      forall _k': ORDINAL, u: U, v: V /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} {:trigger this.P#[_k'](u, v)} | _k' < _k
         ensures this.P#[_k'](u, v)
       {
         L#[_k'](u, v)
@@ -311,7 +311,7 @@ class MyClass<A, B> {
       M#<W>[_k - 1]();
       assert R#<char>[_k - 1]();
     } else {
-      forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} | _k' < _k
+      forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} {:trigger this.R#[_k']()} {:trigger _k' < _k} | _k' < _k
         ensures this.R#[_k']()
       {
         M#[_k']()
@@ -337,7 +337,7 @@ lemma /*{:_induction _k}*/ N#<D0, D1, D2>[_k: ORDINAL](o: MyClass<D0, D1>)
   if 0 < _k.Offset {
     N#<D0, D1, D2>[_k - 1](o);
   } else {
-    forall _k': ORDINAL, o: MyClass<D0, D1> /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} | _k' < _k
+    forall _k': ORDINAL, o: MyClass<D0, D1> /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} {:trigger o.R#[_k']()} | _k' < _k
       ensures o.R#[_k']()
     {
       N#[_k'](o)
@@ -359,7 +359,7 @@ lemma /*{:_induction _k}*/ O#<D0, D1, D2>[_k: ORDINAL]()
   if 0 < _k.Offset {
     O#<D0, D1, D2>[_k - 1]();
   } else {
-    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} | _k' < _k
+    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} {:trigger MyClass<D0, D1>.S#[_k']()} {:trigger _k' < _k} | _k' < _k
       ensures MyClass<D0, D1>.S#[_k']()
     {
       O#[_k']()
@@ -381,7 +381,7 @@ lemma {:induction false} RstRst0#<alpha, gamma>[_k: ORDINAL]()
   if 0 < _k.Offset {
     RstRst0#<int, gamma>[_k - 1]();
   } else {
-    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} | _k' < _k
+    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} {:trigger MyClass<alpha, char>.RST#[_k']()} {:trigger _k' < _k} | _k' < _k
       ensures MyClass<alpha, char>.RST#[_k']()
     {
       RstRst0#[_k']()
@@ -403,7 +403,7 @@ lemma {:induction false} RstRst1#<alpha, gamma>[_k: ORDINAL]()
   if 0 < _k.Offset {
     RstRst1#<int, int>[_k - 1]();
   } else {
-    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} | _k' < _k
+    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} {:trigger MyClass<alpha, char>.RST#[_k']()} {:trigger _k' < _k} | _k' < _k
       ensures MyClass<alpha, char>.RST#[_k']()
     {
       RstRst1#[_k']()
@@ -425,7 +425,7 @@ lemma {:induction false} RstRst2#<alpha, gamma>[_k: ORDINAL]()
   if 0 < _k.Offset {
     RstRst2#<alpha, gamma>[_k - 1]();
   } else {
-    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} | _k' < _k
+    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} {:trigger MyClass<alpha, char>.RST#[_k']()} {:trigger _k' < _k} | _k' < _k
       ensures MyClass<alpha, char>.RST#[_k']()
     {
       RstRst2#[_k']()
@@ -447,7 +447,7 @@ lemma {:induction false} RstRst3#<alpha, beta, gamma>[_k: ORDINAL]()
   if 0 < _k.Offset {
     RstRst3#<alpha, beta, gamma>[_k - 1]();
   } else {
-    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} | _k' < _k
+    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} {:trigger MyClass<alpha, beta>.RST#[_k']()} {:trigger _k' < _k} | _k' < _k
       ensures MyClass<alpha, beta>.RST#[_k']()
     {
       RstRst3#[_k']()
@@ -469,7 +469,7 @@ lemma {:induction false} RstRst4#<alpha, beta, gamma>[_k: ORDINAL]()
   if 0 < _k.Offset {
     RstRst4#<beta, alpha, gamma>[_k - 1]();
   } else {
-    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} | _k' < _k
+    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} {:trigger MyClass<alpha, beta>.RST#[_k']()} {:trigger _k' < _k} | _k' < _k
       ensures MyClass<alpha, beta>.RST#[_k']()
     {
       RstRst4#[_k']()
@@ -499,7 +499,7 @@ lemma {:induction false} RstRst5#<alpha, gamma>[_k: ORDINAL]()
       assert _k.Offset == 1;
     }
   } else {
-    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} | _k' < _k
+    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} {:trigger MyClass<alpha, char>.RST#[_k']()} {:trigger _k' < _k} | _k' < _k
       ensures MyClass<alpha, char>.RST#[_k']()
     {
       RstRst5#[_k']()
@@ -529,7 +529,7 @@ lemma {:induction false} RstRst6#<alpha, beta, gamma>[_k: ORDINAL]()
     case 2 <= _k.Offset =>
       RstRst6#<alpha, beta, gamma>[_k - 2]();
   } else {
-    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} | _k' < _k
+    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} {:trigger MyClass<alpha, beta>.RST#[_k']()} {:trigger _k' < _k} | _k' < _k
       ensures MyClass<alpha, beta>.RST#[_k']()
     {
       RstRst6#[_k']()
@@ -557,7 +557,7 @@ lemma /*{:_induction _k}*/ RstRst7#<alpha, beta, gamma>[_k: ORDINAL]()
     } else {
     }
   } else {
-    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} | _k' < _k
+    forall _k': ORDINAL /*{:_autorequires}*/ /*{:_trustWellformed}*/ {:auto_generated} {:trigger MyClass<alpha, beta>.RST#[_k']()} {:trigger _k' < _k} | _k' < _k
       ensures MyClass<alpha, beta>.RST#[_k']()
     {
       RstRst7#[_k']()
diff --git a/Test/git-issues/git-issue-2947.dfy b/Test/git-issues/git-issue-2947.dfy
new file mode 100644
index 00000000000..1e62b6fe907
--- /dev/null
+++ b/Test/git-issues/git-issue-2947.dfy
@@ -0,0 +1,49 @@
+// RUN: %dafny_0 /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+codatatype Stream<X> = Nil | Cons(head: X, tail: Stream<X>)
+
+least predicate Finite<Y>(s: Stream<Y>) {
+  // The following once generated malformed Boogie, because of a missing
+  // type substitution in the datatype value Nil
+  s == Nil || Finite(s.tail)
+}
+
+least predicate F0<Y>(s: Stream<Y>) {
+  var nil := Nil;
+  s == nil || F0(s.tail)
+}
+
+least predicate F1<Y>(s: Stream<Y>) {
+  s.Nil? || F1(s.tail)
+}
+
+least predicate G0<Y>(s: Stream<Y>) {
+  s is Stream<Y>
+}
+
+least predicate G1<Y>(s: Stream<Y>) {
+  s == Identity(s)
+}
+
+least predicate G2<Y>(s: Stream<Y>) {
+  s == Identity<Stream<Y>>(s)
+}
+
+function Identity<W>(w: W): W { w }
+
+least lemma About<Z>(s: Stream<Z>)
+  requires s == Nil
+  requires s.Nil?
+  requires var nil := Nil; s == nil
+  requires s is Stream<Z>
+  requires s == Identity(s)
+  requires s == Identity<Stream<Z>>(s)
+  requires Finite(s)
+  requires F0(s)
+  requires F1(s)
+  requires G0(s)
+  requires G1(s)
+  requires G2(s)
+{
+}
diff --git a/Test/git-issues/git-issue-2947.dfy.expect b/Test/git-issues/git-issue-2947.dfy.expect
new file mode 100644
index 00000000000..00a51f822da
--- /dev/null
+++ b/Test/git-issues/git-issue-2947.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/docs/dev/news/2984.fix b/docs/dev/news/2984.fix
new file mode 100644
index 00000000000..1d2675716ce
--- /dev/null
+++ b/docs/dev/news/2984.fix
@@ -0,0 +1 @@
+Fix malformed Boogie generated for extreme predicates