diff --git a/src/col/vct/col/print/Namer.scala b/src/col/vct/col/print/Namer.scala
index 8feae24bde..2d43790e85 100644
--- a/src/col/vct/col/print/Namer.scala
+++ b/src/col/vct/col/print/Namer.scala
@@ -10,8 +10,8 @@ case class Namer[G](syntax: Ctx.Syntax) {
   private val stack = ScopedStack[Node[G]]()
   private val names = mutable.Map[(scala.Any, String, Int), Declaration[G]]()
 
-  def nearest(f: PartialFunction[Node[G], Unit]): Option[Node[G]] =
-    stack.toSeq.find(n => f.isDefinedAt(n))
+  def nearest(f: PartialFunction[Node[G], Unit]): Seq[Node[G]] =
+    stack.toSeq.filter(n => f.isDefinedAt(n))
 
   private def nearestClass = nearest {
     case _: Class[G] | _: JavaClass[G] | _: VeyMontSeqProg[G] | _: JavaInterface[G] | _: JavaAnnotationInterface[G] => ()
@@ -73,14 +73,19 @@ case class Namer[G](syntax: Ctx.Syntax) {
     if (index == 0) name
     else s"$name$index"
 
-  def nameKeyed(key: scala.Any, decl: Declaration[G]): Unit = {
+  def nameKeyed(keys: Seq[scala.Any], decl: Declaration[G]): Unit = {
+    if(keys.isEmpty) {
+      // Refuse to name this declaration, it is unclear how to distinguish them.
+      return
+    }
+
     var (baseName, index) = unpackName(decl.o.preferredName)
 
-    while(names.contains((key, baseName, index))) {
+    while(keys.exists(key => names.contains((key, baseName, index)))) {
       index += 1
     }
 
-    names((key, baseName, index)) = decl
+    names((keys.head, baseName, index)) = decl
   }
 
   def name(node: Node[G]): Unit = {
@@ -89,7 +94,7 @@ case class Namer[G](syntax: Ctx.Syntax) {
     node match {
       case decl: GlobalDeclaration[G] => nameKeyed(nearest { case _: Program[G] => () }, decl)
       case decl: ClassDeclaration[G] => nameKeyed(nearestClass, decl)
-      case decl: ADTDeclaration[G] => nameKeyed(if(syntax == Ctx.Silver) 3 else nearest { case _: AxiomaticDataType[G] => () }, decl)
+      case decl: ADTDeclaration[G] => nameKeyed(if(syntax == Ctx.Silver) Seq(3) else nearest { case _: AxiomaticDataType[G] => () }, decl)
       case decl: ModelDeclaration[G] => nameKeyed(nearest { case _: Model[G] => () }, decl)
       case decl: EnumConstant[G] => nameKeyed(nearest { case _: Enum[G] => () }, decl)
       case decl: Variable[G] => nameKeyed(nearestVariableScope, decl)
diff --git a/src/rewrite/vct/rewrite/InlineApplicables.scala b/src/rewrite/vct/rewrite/InlineApplicables.scala
index 4f84961a5d..1cdfb9a67d 100644
--- a/src/rewrite/vct/rewrite/InlineApplicables.scala
+++ b/src/rewrite/vct/rewrite/InlineApplicables.scala
@@ -76,6 +76,13 @@ case object InlineApplicables extends RewriterBuilder {
     override def inlineContext: String = s"${definition.inlineContext} [inlined from] ${usages.head.o.inlineContext}"
   }
 
+  case object InlineLetThisOrigin extends Origin {
+    override def preferredName: String = "self"
+    override def context: String = "[At let binding for `this`]"
+    override def inlineContext: String = "[Let binding for `this`]"
+    override def shortPosition: String = "generated"
+  }
+
   case class InlineFoldAssertFailed(fold: Fold[_]) extends Blame[AssertFailed] {
     override def blame(error: AssertFailed): Unit =
       fold.blame.blame(FoldFailed(error.failure, fold))
@@ -191,26 +198,26 @@ case class InlineApplicables[Pre <: Generation]() extends Rewriter[Pre] with Laz
         lazy val obj = {
           val instanceApply = apply.asInstanceOf[InstanceApply[Pre]]
           val cls = classOwner(instanceApply.ref.decl)
-          Replacement(ThisObject[Pre](cls.ref), instanceApply.obj)
+          Replacement(ThisObject[Pre](cls.ref), instanceApply.obj)(InlineLetThisOrigin)
         }
 
         lazy val args =
           Replacements(for((arg, v) <- apply.args.zip(apply.ref.decl.args))
-            yield Replacement(v.get, arg))
+            yield Replacement(v.get, arg)(v.o))
 
         lazy val givenArgs =
           Replacements(for((Ref(v), arg) <- apply.asInstanceOf[InvokingNode[Pre]].givenMap)
-            yield Replacement(v.get, arg))
+            yield Replacement(v.get, arg)(v.o))
 
         lazy val outArgs = {
           val inv = apply.asInstanceOf[AnyMethodInvocation[Pre]]
           Replacements(for((out, v) <- inv.outArgs.zip(inv.ref.decl.outArgs))
-            yield Replacement(v.get, out))
+            yield Replacement(v.get, out)(v.o))
         }
 
         lazy val yields =
           Replacements(for((out, Ref(v)) <- apply.asInstanceOf[InvokingNode[Pre]].yields)
-            yield Replacement(v.get, out))
+            yield Replacement(v.get, out)(v.o))
 
         val replacements = apply.ref.decl.args.map(_.get).zip(apply.args).toMap[Expr[Pre], Expr[Pre]]
         // TODO: consider type arguments and out-arguments and given and yields (oof)