diff --git a/.unreleased/features/unsafe.md b/.unreleased/features/unsafe.md
new file mode 100644
index 0000000000..99205f081a
--- /dev/null
+++ b/.unreleased/features/unsafe.md
@@ -0,0 +1 @@
+Added scope-unsafe builder.
\ No newline at end of file
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala
index e50e21db89..b4d09c0825 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala
@@ -8,8 +8,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._
 import at.forsyte.apalache.tla.bmcmt.rules.aux.{ProtoSeqOps, RecordAndVariantOps}
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 import scalaz.unused
 
 import scala.collection.immutable.SortedMap
@@ -41,7 +40,7 @@ class LazyEquality(rewriter: SymbStateRewriter)
    * @return
    *   tla.eql(left, right), provided that left and right can be compared
    */
-  def safeEq(left: ArenaCell, right: ArenaCell): TBuilderInstruction = {
+  def safeEq(left: ArenaCell, right: ArenaCell): BuilderT = {
     if (left == right) {
       tla.bool(true) // this is just true
     } else {
@@ -319,14 +318,14 @@ class LazyEquality(rewriter: SymbStateRewriter)
         // inAndEq checks if lelem is in right
         val inAndEqList = rightElems.map(inAndEq(rewriter, _, lelem, right, lazyEq = true))
         // There are plenty of valid subformulas. Simplify!
-        tla.or(inAndEqList: _*).map(simplifier.simplifyShallow)
+        simplifier.applySimplifyShallowToBuilderEx(tla.or(inAndEqList: _*))
       }
 
       def notInOrExists(lelem: ArenaCell) = {
         val notInOrExists =
-          tla
-            .or(tla.not(tla.selectInSet(lelem.toBuilder, left.toBuilder)), exists(lelem))
-            .map(simplifier.simplifyShallow)
+          simplifier.applySimplifyShallowToBuilderEx(
+              tla.or(tla.not(tla.selectInSet(lelem.toBuilder, left.toBuilder)), exists(lelem))
+          )
 
         if (simplifier.isBoolConst(notInOrExists)) {
           notInOrExists // just return the constant
@@ -340,7 +339,8 @@ class LazyEquality(rewriter: SymbStateRewriter)
         }
       }
 
-      val forEachNotInOrExists = tla.and(leftElems.map(notInOrExists): _*).map(simplifier.simplifyShallow)
+      val forEachNotInOrExists =
+        simplifier.applySimplifyShallowToBuilderEx(tla.and(leftElems.map(notInOrExists): _*))
       newState = newState.updateArena(_.appendCell(BoolT1))
       val pred = newState.arena.topCell
       rewriter.solverContext.assertGroundExpr(tla.eql(pred.toBuilder, forEachNotInOrExists))
@@ -471,7 +471,7 @@ class LazyEquality(rewriter: SymbStateRewriter)
     val commonKeys = leftType.fieldTypes.keySet.intersect(rightType.fieldTypes.keySet)
     var newState = state
 
-    def keyEq(key: String): TBuilderInstruction = {
+    def keyEq(key: String): BuilderT = {
       val leftIndex = leftType.fieldTypes.keySet.toList.indexOf(key)
       val rightIndex = rightType.fieldTypes.keySet.toList.indexOf(key)
 
@@ -522,7 +522,7 @@ class LazyEquality(rewriter: SymbStateRewriter)
       leftRec: ArenaCell,
       rightRec: ArenaCell): SymbState = {
     var nextState = state
-    def fieldsEq(name: String): TBuilderInstruction = {
+    def fieldsEq(name: String): BuilderT = {
       val leftField = recordOps.getField(nextState.arena, leftRec, name)
       val rightField = recordOps.getField(nextState.arena, rightRec, name)
       // The field values may be non-basic expressions. Use lazy equality over them too.
@@ -545,7 +545,7 @@ class LazyEquality(rewriter: SymbStateRewriter)
     val leftTag = recordOps.getVariantTag(nextState.arena, leftVar)
     val rightTag = recordOps.getVariantTag(nextState.arena, rightVar)
 
-    def valuesEq(tagName: String): TBuilderInstruction = {
+    def valuesEq(tagName: String): BuilderT = {
       val leftValue = recordOps.getUnsafeVariantValue(nextState.arena, leftVar, tagName)
       val rightValue = recordOps.getUnsafeVariantValue(nextState.arena, rightVar, tagName)
       // The field values may be non-basic expressions. Use lazy equality over them too.
@@ -569,7 +569,7 @@ class LazyEquality(rewriter: SymbStateRewriter)
   private def mkTupleEq(state: SymbState, left: ArenaCell, right: ArenaCell): SymbState = {
     var newState = state
 
-    def elemEq(lelem: ArenaCell, relem: ArenaCell): TBuilderInstruction = {
+    def elemEq(lelem: ArenaCell, relem: ArenaCell): BuilderT = {
       newState = cacheOneEqConstraint(newState, lelem, relem)
       safeEq(lelem, relem)
     }
@@ -602,7 +602,7 @@ class LazyEquality(rewriter: SymbStateRewriter)
     val len1Ex = len1.toBuilder
     val len2Ex = len2.toBuilder
 
-    def eqPairwise(indexBase1: Int, cells: (ArenaCell, ArenaCell)): TBuilderInstruction = {
+    def eqPairwise(indexBase1: Int, cells: (ArenaCell, ArenaCell)): BuilderT = {
       nextState = cacheOneEqConstraint(nextState, cells._1, cells._2)
       // Either (1) one of the lengths is below the index, or (2) the elements are equal.
       // The case (1) is compensated with the constraint sizesEq below.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala
index da36921b93..1d96cdf622 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala
@@ -10,8 +10,8 @@ import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.{TlaBoolOper, TlaOper}
 import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker
 import at.forsyte.apalache.tla.lir.transformations.standard.ReplaceFixed
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.typecomp._
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 import com.typesafe.scalalogging.LazyLogging
 
 import scala.util.Random
@@ -442,7 +442,7 @@ class SeqModelChecker[ExecutorContextT](
     val stateType = RecT1(checkerInput.rootModule.varDeclarations.map(d => d.name -> d.typeTag.asTlaType1()): _*)
 
     // convert a variable binding to a record
-    def mkRecord(b: Binding): TBuilderInstruction = {
+    def mkRecord(b: Binding): BuilderT = {
       val ctorArgs = b.toMap.map { case (key, value) =>
         (key, tla.name(value.toString, stateType.fieldTypes(key)))
       }
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala
index 974aab97e7..ca4f5ba709 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala
@@ -8,8 +8,8 @@ import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaSetOper
 import at.forsyte.apalache.tla.lir.values._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 import com.typesafe.scalalogging.LazyLogging
 
 import scala.collection.immutable.SortedMap
@@ -24,16 +24,21 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
   private val protoSeqOps = new ProtoSeqOps(rewriter)
   private val recordOps = new RecordAndVariantOps(rewriter)
 
+  def evalGroundExprForBuilderEx(ex: TBuilderInstruction): TBuilderInstruction =
+    ex.map(solverContext.evalGroundExpr) // when using TBuilderInstruction
+  def evalGroundExprForBuilderEx(ex: TlaEx): TlaEx =
+    solverContext.evalGroundExpr(ex) // when using TlaEx
+
   def decodeStateVariables(state: SymbState): Map[String, TlaEx] = {
     state.binding.toMap.map(p => (p._1, reverseMapVar(decodeCellToTlaEx(state.arena, p._2), p._1, p._2)))
   }
 
-  def decodeCellToTlaEx(arena: PureArenaAdapter, cell: ArenaCell): TBuilderInstruction = cell.cellType match {
+  def decodeCellToTlaEx(arena: PureArenaAdapter, cell: ArenaCell): BuilderT = cell.cellType match {
     case CellTFrom(BoolT1) =>
-      cell.toBuilder.map(solverContext.evalGroundExpr)
+      evalGroundExprForBuilderEx(cell.toBuilder)
 
     case CellTFrom(IntT1) =>
-      cell.toBuilder.map(solverContext.evalGroundExpr)
+      evalGroundExprForBuilderEx(cell.toBuilder)
 
     case ct @ CellTFrom(StrT1 | ConstT1(_)) =>
       // First, attempt to check the cache
@@ -128,7 +133,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
       throw new RewriterException("Don't know how to decode the cell %s of type %s".format(cell, cell.cellType), NullEx)
   }
 
-  private def decodeOldRecordToTlaEx(arena: PureArenaAdapter, cell: ArenaCell, recordT: RecT1): TBuilderInstruction = {
+  private def decodeOldRecordToTlaEx(arena: PureArenaAdapter, cell: ArenaCell, recordT: RecT1): BuilderT = {
     def exToStr(ex: TlaEx): TlaStr = ex match {
       case ValEx(s @ TlaStr(_)) => s
       case _                    => throw new RewriterException("Expected a string, found: " + ex, ex)
@@ -141,7 +146,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
     val fieldValues = arena.getHas(cell)
     val keyList = recordT.fieldTypes.keySet.toList
 
-    def eachField(es: List[TBuilderInstruction], key: String): List[TBuilderInstruction] = {
+    def eachField(es: List[BuilderT], key: String): List[BuilderT] = {
       if (!dom.contains(TlaStr(key))) {
         es // skip
       } else {
@@ -151,7 +156,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
       }
     }
 
-    val keysAndValues = keyList.reverse.foldLeft(List.empty[TBuilderInstruction])(eachField)
+    val keysAndValues = keyList.reverse.foldLeft(List.empty[BuilderT])(eachField)
     if (keysAndValues.nonEmpty) {
       tla.recMixed(keysAndValues: _*)
     } else {
@@ -165,7 +170,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
   private def decodeRecordToTlaEx(
       arena: PureArenaAdapter,
       cell: ArenaCell,
-      fieldTypes: SortedMap[String, TlaType1]): TBuilderInstruction =
+      fieldTypes: SortedMap[String, TlaType1]): BuilderT =
     tla.rowRec(None,
         fieldTypes.keySet.toList.map { k =>
           k -> decodeCellToTlaEx(arena, recordOps.getField(arena, cell, k))
@@ -174,7 +179,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
   private def decodeVariantToTlaEx(
       arena: PureArenaAdapter,
       cell: ArenaCell,
-      options: SortedMap[String, TlaType1]): TBuilderInstruction = {
+      options: SortedMap[String, TlaType1]): BuilderT = {
     val tagName = decodeCellToTlaEx(arena, recordOps.getVariantTag(arena, cell)).build match {
       case ValEx(TlaStr(name)) => name
 
@@ -184,7 +189,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
     tla.variant(tagName, value, VariantT1(RowT1(options, None)))
   }
 
-  private def decodeFunToTlaEx(arena: PureArenaAdapter, cell: ArenaCell): TBuilderInstruction = {
+  private def decodeFunToTlaEx(arena: PureArenaAdapter, cell: ArenaCell): BuilderT = {
     // a function is represented with the relation {(x, f[x]) : x \in S}
     val relation = arena.getCdm(cell)
 
@@ -195,7 +200,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
           // given this, we query the solver about the function's domain instead
           val domain = arena.getDom(cell)
 
-          def inDom(elem: ArenaCell): TBuilderInstruction = {
+          def inDom(elem: ArenaCell): BuilderT = {
             val elemEx = elem.toBuilder
             val domEx = domain.toBuilder
             tla.selectInSet(elemEx, domEx)
@@ -257,7 +262,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
     }
   }
 
-  private def findCellInSet(cells: Seq[ArenaCell], ex: TBuilderInstruction): Option[ArenaCell] = {
+  private def findCellInSet(cells: Seq[ArenaCell], ex: BuilderT): Option[ArenaCell] = {
     def isEq(c: ArenaCell): Boolean = {
       val query = tla.and(tla.eql(c.toBuilder, ex))
       tla.bool(true).build == solverContext.evalGroundExpr(query)
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PtrUtil.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PtrUtil.scala
index c81c24f6ab..28f570c42b 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PtrUtil.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PtrUtil.scala
@@ -1,7 +1,7 @@
 package at.forsyte.apalache.tla.bmcmt.arena
 
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, ElemPtr, FixedElemPtr, SmtExprElemPtr}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Contains miscellaneous methods related to [[ElemPtr]]s.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PureArenaAdapter.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PureArenaAdapter.scala
index 72f43e98f8..01b7357a5e 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PureArenaAdapter.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PureArenaAdapter.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, ElemPtr, FixedElemPtr, PureAren
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Declares the same interface as [[Arena]]s (with the exception of [[ElemPtr]] usage).
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/EqCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/EqCache.scala
index 21646402d3..984baef229 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/EqCache.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/EqCache.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.caches.EqCache._
 import at.forsyte.apalache.tla.bmcmt.rewriter.Recoverable
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, StackableContext}
 import at.forsyte.apalache.tla.lir.TlaEx
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 import scala.collection.mutable
 
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntRangeCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntRangeCache.scala
index 47ec20a096..5f92925f81 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntRangeCache.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntRangeCache.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, ElemPtr, FixedElemPtr}
 import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.lir.{IntT1, SetT1}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Cache tuple domains as well as ranges a..b.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntValueCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntValueCache.scala
index 2bce3fcba9..284bf02d02 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntValueCache.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntValueCache.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.ArenaCell
 import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.lir.IntT1
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * A cache for integer constants that maps an integer to an integer constant in SMT.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala
index 3318cc1d6e..fe25ac55d0 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala
@@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.bmcmt.types.CellTFrom
 import at.forsyte.apalache.tla.lir.{ConstT1, StrT1}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * A cache for model values that are translated as uninterpreted constants, with a unique sort per uniterpreted type.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/RecordDomainCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/RecordDomainCache.scala
index 606c429769..fc68488903 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/RecordDomainCache.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/RecordDomainCache.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, ElemPtr, SmtExprElemPtr}
 import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.lir.{SetT1, StrT1}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 import scala.collection.immutable.SortedSet
 
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/CardinalityConstRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/CardinalityConstRule.scala
index d424032ab2..5a083fdf83 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/CardinalityConstRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/CardinalityConstRule.scala
@@ -6,7 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.CherryPick
 import at.forsyte.apalache.tla.lir.oper.{ApalacheOper, TlaArithOper, TlaFiniteSetOper}
 import at.forsyte.apalache.tla.lir.values.TlaInt
 import at.forsyte.apalache.tla.lir.{BoolT1, OperEx, ValEx}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Optimization for Cardinality(S) >= k, where k is constant. See [docs/smt/Cardinality.md].
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala
index 7cf90cc6f9..02c19a730f 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala
@@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.{ProtoSeqOps, RecordAndVariantOps
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaFunOper
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Rewriting DOMAIN f, that is, translating the domain of a function, record, tuple, or sequence.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FoldSetRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FoldSetRule.scala
index f1a895676b..f3e87a8484 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FoldSetRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FoldSetRule.scala
@@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.lir.oper.ApalacheOper
 import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker
 import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming
 import at.forsyte.apalache.tla.pp.Inliner
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Rewriting rule for FoldSet. Similar to Cardinality, we need to consider element set presence and multiplicity.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRule.scala
index c46e087842..3505ecee11 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRule.scala
@@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, ProtoSeqOps, RecordAndVariantOps}
 import at.forsyte.apalache.tla.bmcmt.types._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 import at.forsyte.apalache.tla.lir.oper.TlaFunOper
 import at.forsyte.apalache.tla.lir.values.{TlaInt, TlaStr}
 import at.forsyte.apalache.tla.lir._
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRuleWithArrays.scala
index 0f1e5531e6..6690fc4784 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRuleWithArrays.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRuleWithArrays.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._
 import at.forsyte.apalache.tla.bmcmt.types._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 import at.forsyte.apalache.tla.lir.{BoolT1, FunT1, RecT1, SetT1, TlaEx}
 
 /**
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRule.scala
index c823cfb84b..767a4b2ee7 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRule.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaFunOper
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * The new implementation of a function constructor that encodes a function f = [x \in S |-> e] the classical way: f =
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRuleWithArrays.scala
index 73b9c06aa9..e0393c441f 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRuleWithArrays.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRuleWithArrays.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Encodes the construction of a function f = [x \in S |-> e]. We carry the domain set in a separate set cell. The
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRule.scala
index 36ff58c28a..a29232d67a 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRule.scala
@@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.{ProtoSeqOps, RecordAndVariantOps
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaFunOper
 import at.forsyte.apalache.tla.lir.values.{TlaInt, TlaStr}
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 import scalaz.unused
 
 /**
@@ -66,7 +65,7 @@ class FunExceptRule(rewriter: SymbStateRewriter) extends RewritingRule {
       indexCell: ArenaCell,
       valueCell: ArenaCell): SymbState = {
     // rewrite tuples <<j_i, e_i>> to cells
-    def mkPair(indexCell: ArenaCell, resCell: ArenaCell): TBuilderInstruction =
+    def mkPair(indexCell: ArenaCell, resCell: ArenaCell): BuilderT =
       tla.tuple(indexCell.toBuilder, resCell.toBuilder)
 
     var nextState = rewriter.rewriteUntilDone(state.setRex(mkPair(indexCell, valueCell)))
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRuleWithArrays.scala
index 86c2b6174a..8bb0385770 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRuleWithArrays.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRuleWithArrays.scala
@@ -3,8 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.arena.PtrUtil
 import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps.constrainRelationArgs
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * Rewriting EXCEPT for functions, tuples, and records.
@@ -31,7 +30,7 @@ class FunExceptRuleWithArrays(rewriter: SymbStateRewriter) extends FunExceptRule
     nextState = nextState.updateArena(_.setDom(resultFunCell, domainCell))
 
     // Make pair <arg,res> to propagate metadata
-    def mkPair(indexCell: ArenaCell, resCell: ArenaCell): TBuilderInstruction =
+    def mkPair(indexCell: ArenaCell, resCell: ArenaCell): BuilderT =
       tla.tuple(indexCell.toBuilder, resCell.toBuilder)
 
     nextState = rewriter.rewriteUntilDone(nextState.setRex(mkPair(indexCell, valueCell)))
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IfThenElseRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IfThenElseRule.scala
index 5753c1bc55..c27230be1d 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IfThenElseRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IfThenElseRule.scala
@@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.CherryPick
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir.oper.TlaControlOper
 import at.forsyte.apalache.tla.lir.{BoolT1, ConstT1, IntT1, OperEx}
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * Rewriting rule for IF A THEN B ELSE C.
@@ -63,7 +62,7 @@ class IfThenElseRule(rewriter: SymbStateRewriter) extends RewritingRule {
   private def iteBasic(
       state: SymbState,
       commonType: CellT,
-      pred: TBuilderInstruction,
+      pred: BuilderT,
       thenCell: ArenaCell,
       elseCell: ArenaCell) = {
     val newArena = state.arena.appendCellOld(commonType)
@@ -78,7 +77,7 @@ class IfThenElseRule(rewriter: SymbStateRewriter) extends RewritingRule {
   // The cool thing is that we do not have to compare the results anymore. It is all defined by the oracle.
   private def iteGeneral(
       state: SymbState,
-      pred: TBuilderInstruction,
+      pred: BuilderT,
       thenCell: ArenaCell,
       elseCell: ArenaCell) = {
     def solverAssert = rewriter.solverContext.assertGroundExpr _
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/QuantRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/QuantRule.scala
index d203be5da0..717325582e 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/QuantRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/QuantRule.scala
@@ -4,10 +4,10 @@ import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, OracleHelper}
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 import at.forsyte.apalache.tla.lir.oper._
 import at.forsyte.apalache.tla.lir.values.{TlaIntSet, TlaNatSet}
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
 import com.typesafe.scalalogging.LazyLogging
 
 /**
@@ -139,16 +139,16 @@ class QuantRule(rewriter: SymbStateRewriter) extends RewritingRule with LazyLogg
       val (predState: SymbState, predEsRaw: Seq[TlaEx]) =
         rewriter.rewriteBoundSeqUntilDone(setState, setCells.map(mkPair))
 
-      val predEs: Seq[TBuilderInstruction] = predEsRaw.map(tla.unchecked)
+      val predEs: Seq[BuilderT] = predEsRaw.map(tla.unchecked)
 
       val nonEmpty = tla.or(setCells.map(c => tla.selectInSet(c.toBuilder, set.toBuilder)): _*)
       val empty = tla.and(setCells.map(c => tla.not(tla.selectInSet(c.toBuilder, set.toBuilder))): _*)
 
-      def elemWitnesses(elemAndPred: (ArenaCell, TBuilderInstruction)): TBuilderInstruction = {
+      def elemWitnesses(elemAndPred: (ArenaCell, BuilderT)): BuilderT = {
         tla.and(tla.selectInSet(elemAndPred._1.toBuilder, set.toBuilder), elemAndPred._2)
       }
 
-      def elemSatisfies(elemAndPred: (ArenaCell, TBuilderInstruction)): TBuilderInstruction = {
+      def elemSatisfies(elemAndPred: (ArenaCell, BuilderT)): BuilderT = {
         tla.or(tla.not(tla.selectInSet(elemAndPred._1.toBuilder, set.toBuilder)), elemAndPred._2)
       }
 
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RecCtorRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RecCtorRule.scala
index 327ceaf69a..a8b1835a96 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RecCtorRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RecCtorRule.scala
@@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.RecordAndVariantOps
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaFunOper
 import at.forsyte.apalache.tla.lir.values.TlaStr
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 import scala.collection.immutable.{SortedMap, SortedSet}
 
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala
index 7bec841e0a..7dff798d78 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala
@@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker
 import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming
 import at.forsyte.apalache.tla.lir.values.TlaInt
 import at.forsyte.apalache.tla.pp.Inliner
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Rewriting rule for Repeat. This rule is similar to [[FoldSeqRule]].
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SeqOpsRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SeqOpsRule.scala
index affd54df27..c089426668 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SeqOpsRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SeqOpsRule.scala
@@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, ProtoSeqOps}
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 import at.forsyte.apalache.tla.lir.oper.{ApalacheInternalOper, TlaSeqOper}
 
 /**
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetAsFunRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetAsFunRule.scala
index a796dbbfdf..4f6396dd7b 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetAsFunRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetAsFunRule.scala
@@ -3,9 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.rules
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 import at.forsyte.apalache.tla.lir.oper.ApalacheOper
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
 
 /**
  * Implements a rule for Apalache!SetAsFun.
@@ -118,7 +117,7 @@ class SetAsFunRule(rewriter: SymbStateRewriter) extends RewritingRule {
       val key1 = nextState.arena.getHas(pair1).head
 
       // ensure that a pair with the same key has not been included in the relation yet
-      def keysDifferOrNotIncluded(pair2Ptr: ElemPtr): TBuilderInstruction = {
+      def keysDifferOrNotIncluded(pair2Ptr: ElemPtr): BuilderT = {
         val pair2 = pair2Ptr.elem
         val key2 = nextState.arena.getHas(pair2).head
         // pair2 \notin funRel
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCtorRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCtorRule.scala
index 765734621c..8ee6c25656 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCtorRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCtorRule.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.types.{CellT, CellTFrom}
 import at.forsyte.apalache.tla.lir.oper.TlaSetOper
 import at.forsyte.apalache.tla.lir.{OperEx, SetT1, TlaEx, TypingException}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Rewrites the set constructor {e_1, ..., e_k}.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala
index fad08ced10..4ee1c5f480 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala
@@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.arena.PtrUtil
 import at.forsyte.apalache.tla.lir.oper.{TlaBoolOper, TlaSetOper}
 import at.forsyte.apalache.tla.lir.{OperEx, TlaType1}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Rewrites X \cup Y, that is, a union of two sets (not UNION). In the first encoding, we used a linear number of `in`
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetFilterRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetFilterRule.scala
index d50920dd70..514dfad4e4 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetFilterRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetFilterRule.scala
@@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir.oper.{TlaBoolOper, TlaSetOper}
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Rewrites a set comprehension { x \in S: P }.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala
index ea88a6558e..edb0153941 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala
@@ -5,8 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir.oper.{ApalacheInternalOper, TlaSetOper}
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * Rewrites set membership tests: x \in S, x \in SUBSET S, and x \in [S -> T].
@@ -114,7 +113,7 @@ class SetInRule(rewriter: SymbStateRewriter) extends RewritingRule {
     // In the new implementation, a function is a relation { <<x, f[x]>> : x \in U }.
     // Check that \A t \in f: t[1] \in S /\ t[2] \in T, and
     // `DOMAIN f = S`, since the above only implies `DOMAIN f \subseteq S`
-    def onPair(pair: ArenaCell): TBuilderInstruction = {
+    def onPair(pair: ArenaCell): BuilderT = {
       val tupleElems = nextState.arena.getHas(pair)
       val (arg, res) = (tupleElems.head, tupleElems.tail.head)
       nextState = rewriter.rewriteUntilDone(nextState.setRex(tla.selectInSet(arg.toBuilder, funsetDom.toBuilder)))
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala
index 3f0901d625..684b814e86 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala
@@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, RewriterException, SymbState, SymbStateRewriter}
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * Rewrites set membership tests: x \in S, x \in SUBSET S, and x \in [S -> T].
@@ -33,16 +32,18 @@ class SetInRuleWithArrays(rewriter: SymbStateRewriter) extends SetInRule(rewrite
     // TODO: Inlining this method is pointless. We should consider handling tuples and other structures natively in SMT.
     var newState = rewriter.lazyEq.cacheEqConstraints(state, setElems.cross(powsetDomainElems))
 
-    def isInPowset(setElem: ArenaCell): TBuilderInstruction = {
+    def isInPowset(setElem: ArenaCell): BuilderT = {
       newState = newState.updateArena(_.appendCell(BoolT1))
       val pred = newState.arena.topCell
 
-      def isInAndEqSetElem(powsetDomainElem: ArenaCell): TBuilderInstruction = {
+      def isInAndEqSetElem(powsetDomainElem: ArenaCell): BuilderT = {
         // powsetDomainElem \in powsetDomain /\ powsetDomainElem = setElem
-        tla
-          .and(tla.selectInSet(powsetDomainElem.toBuilder, powsetDomain.toBuilder),
-              tla.eql(powsetDomainElem.toBuilder, setElem.toBuilder))
-          .map(simplifier.simplifyShallow)
+        simplifier.applySimplifyShallowToBuilderEx(
+            tla.and(
+                tla.selectInSet(powsetDomainElem.toBuilder, powsetDomain.toBuilder),
+                tla.eql(powsetDomainElem.toBuilder, setElem.toBuilder),
+            )
+        )
       }
 
       val elemsInAndEqSetElem = powsetDomainElems.map(isInAndEqSetElem)
@@ -53,7 +54,8 @@ class SetInRuleWithArrays(rewriter: SymbStateRewriter) extends SetInRule(rewrite
       pred.toBuilder
     }
 
-    val isSubset = tla.and(setElems.map(isInPowset): _*).map(simplifier.simplifyShallow)
+    val isSubset =
+      simplifier.applySimplifyShallowToBuilderEx(tla.and(setElems.map(isInPowset): _*))
     newState = newState.updateArena(_.appendCell(BoolT1))
     val pred = newState.arena.topCell.toBuilder
     rewriter.solverContext.assertGroundExpr(tla.eql(pred, isSubset))
@@ -88,7 +90,7 @@ class SetInRuleWithArrays(rewriter: SymbStateRewriter) extends SetInRule(rewrite
 
     // This method checks if f(x) \in T, for a given x
     // The goal is to ensure that \forall x \in DOMAIN f : f(x) \in T, by applying it to every arg \in DOMAIN f
-    def onFun(funsetDomElem: ArenaCell): TBuilderInstruction = {
+    def onFun(funsetDomElem: ArenaCell): BuilderT = {
       funsetCdm.cellType match {
         case _: PowSetT =>
           nextState = rewriter
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithFunArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithFunArrays.scala
index 0b2aa208a7..0000d6f9f0 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithFunArrays.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithFunArrays.scala
@@ -4,8 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, RewriterException, SymbState, SymbStateRewriter}
 import at.forsyte.apalache.tla.lir.{BoolT1, FunT1}
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * Rewrites set membership tests: x \in S, x \in SUBSET S, and x \in [S -> T].
@@ -38,7 +37,7 @@ class SetInRuleWithFunArrays(rewriter: SymbStateRewriter) extends SetInRule(rewr
 
     // This method checks if there is a pair (x,y) \in RELATION f s.t. x = arg \land arg \in DOMAIN f
     // The goal is to ensure that f's range is a subset of T, by applying it to every arg \in DOMAIN f
-    def onPair(arg: ArenaCell): TBuilderInstruction = {
+    def onPair(arg: ArenaCell): BuilderT = {
       val funApp = tla.app(funCell.toBuilder, arg.toBuilder)
       nextState = rewriter.rewriteUntilDone(nextState.setRex(funApp))
       val funAppRes = nextState.asCell
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala
index cbb3c19ae7..417e61b650 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala
@@ -3,10 +3,9 @@ package at.forsyte.apalache.tla.bmcmt.rules
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.arena.PtrUtil
 import at.forsyte.apalache.tla.bmcmt.types.CellTFrom
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 import at.forsyte.apalache.tla.lir.oper.TlaSetOper
 import at.forsyte.apalache.tla.lir.{OperEx, SetT1, TypingException}
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
 
 /**
  * Implements the rule for a union of all set elements, that is, UNION S for a set S that contains sets as elements.
@@ -62,7 +61,7 @@ class SetUnionRule(rewriter: SymbStateRewriter) extends RewritingRule {
           // add all the elements to the arena
           nextState = nextState.updateArena(_.appendHas(newSetCell, unionElemPtrs: _*))
 
-          def inPointingSet(elemCell: ArenaCell, set: ArenaCell): TBuilderInstruction = {
+          def inPointingSet(elemCell: ArenaCell, set: ArenaCell): BuilderT = {
             // this is sound, because we have generated element equalities
             // and thus can use congruence of in(...) for free
             tla.and(tla.selectInSet(set.toBuilder, topSetCell.toBuilder),
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/AuxOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/AuxOps.scala
index 0e197f5ccc..e2aa2639ea 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/AuxOps.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/AuxOps.scala
@@ -3,8 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt.rewriter.ConstSimplifierForSmt
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter}
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * Auxiliary methods for handling rewriting rules.
@@ -46,13 +45,13 @@ object AuxOps {
         val domainElems = nextState.arena.getHas(domain)
         val relationElems = nextState.arena.getHas(relation)
 
-        def eqAndInDomain(domainElem: ArenaCell, checkedElem: ArenaCell): TBuilderInstruction = {
+        def eqAndInDomain(domainElem: ArenaCell, checkedElem: ArenaCell): BuilderT = {
           val eq = tla.unchecked(rewriter.lazyEq.safeEq(domainElem, checkedElem))
           val selectInSet = tla.selectInSet(domainElem.toBuilder, domain.toBuilder)
           tla.and(eq, selectInSet)
         }
 
-        def isInDomain(elem: ArenaCell): TBuilderInstruction = {
+        def isInDomain(elem: ArenaCell): BuilderT = {
           if (domainElems.isEmpty) {
             tla.bool(false)
           } else {
@@ -99,7 +98,7 @@ object AuxOps {
       checkedElem: ArenaCell,
       setElem: ArenaCell,
       setCell: ArenaCell,
-      lazyEq: Boolean): TBuilderInstruction = {
+      lazyEq: Boolean): BuilderT = {
 
     val conjunction = if (lazyEq) {
       tla.and(
@@ -112,6 +111,6 @@ object AuxOps {
           tla.eql(checkedElem.toBuilder, setElem.toBuilder),
       )
     }
-    conjunction.map(simplifier.simplifyShallow)
+    simplifier.applySimplifyShallowToBuilderEx(conjunction)
   }
 }
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala
index abf076190b..14076b0089 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala
@@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.arena.PtrUtil
 import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types._
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT, _}
 
 import scala.collection.immutable.SortedMap
 
@@ -39,7 +38,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
    * @return
    *   a new symbolic state whose expression stores a fresh cell that corresponds to the picked element.
    */
-  def pick(set: ArenaCell, state: SymbState, elseAssert: TBuilderInstruction): SymbState = {
+  def pick(set: ArenaCell, state: SymbState, elseAssert: BuilderT): SymbState = {
     set.cellType match {
       // all kinds of sets that should be kept unexpanded
       case PowSetT(t @ SetT1(_)) =>
@@ -110,7 +109,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
       state: SymbState,
       oracle: Oracle,
       elems: Seq[ArenaCell],
-      elseAssert: TBuilderInstruction): SymbState = {
+      elseAssert: BuilderT): SymbState = {
     assert(elems.nonEmpty) // this is an advanced operator -- you should know what you are doing
     val targetType = elems.head.cellType
 
@@ -181,7 +180,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
       state: SymbState,
       oracle: Oracle,
       elems: Seq[ArenaCell],
-      elseAssert: TBuilderInstruction): SymbState = {
+      elseAssert: BuilderT): SymbState = {
     rewriter.solverContext.log("; CHERRY-PICK %s FROM [%s] {".format(cellType, elems.map(_.toString).mkString(", ")))
     val arena = state.arena.appendCell(cellType)
     val resultCell = arena.topCell
@@ -214,7 +213,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
       state: SymbState,
       oracle: Oracle,
       tuples: Seq[ArenaCell],
-      elseAssert: TBuilderInstruction): SymbState = {
+      elseAssert: BuilderT): SymbState = {
     rewriter.solverContext.log("; CHERRY-PICK %s FROM [%s] {".format(cellType, tuples.map(_.toString).mkString(", ")))
     var newState = state
 
@@ -262,7 +261,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
       state: SymbState,
       oracle: Oracle,
       records: Seq[ArenaCell],
-      elseAssert: TBuilderInstruction): SymbState = {
+      elseAssert: BuilderT): SymbState = {
     // the records do not always have the same type, but they do have compatible types
     val commonRecordT = findCommonRecordType(records)
     rewriter.solverContext
@@ -353,7 +352,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
       state: SymbState,
       oracle: Oracle,
       records: Seq[ArenaCell],
-      elseAssert: TBuilderInstruction): SymbState = {
+      elseAssert: BuilderT): SymbState = {
     // new row records always have the same type
     val (fieldTypes, recordT) = records.head.cellType match {
       case CellTFrom(rt @ RecRowT1(RowT1(fieldTypes, None))) => (fieldTypes, rt)
@@ -400,7 +399,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
       state: SymbState,
       oracle: Oracle,
       variants: Seq[ArenaCell],
-      elseAssert: TBuilderInstruction): SymbState = {
+      elseAssert: BuilderT): SymbState = {
     // variants should always have the same type
     val (optionTypes, variantT) = variants.head.cellType match {
       case CellTFrom(rt @ VariantT1(RowT1(opts, None))) => (opts, rt)
@@ -580,7 +579,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
       state: SymbState,
       oracle: Oracle,
       memberSets: Seq[ArenaCell],
-      elseAssert: TBuilderInstruction,
+      elseAssert: BuilderT,
       noSmt: Boolean = false): SymbState = {
     if (memberSets.isEmpty) {
       throw new RuntimeException("Picking from a statically empty set")
@@ -602,7 +601,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
       state: SymbState,
       oracle: Oracle,
       memberSets: Seq[ArenaCell],
-      elseAssert: TBuilderInstruction,
+      elseAssert: BuilderT,
       noSMT: Boolean): SymbState = {
     def solverAssert(e: TlaEx): Unit = rewriter.solverContext.assertGroundExpr(e)
 
@@ -658,7 +657,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
       // The awesome property of the oracle is that we do not have to compare the sets directly!
       // Instead, we compare the oracle values.
       // (chosen = 1 /\ in(z_i, R) <=> in(c_i, S_1)) \/ (chosen = 2 /\ in(z_i, R) <=> in(d_i, S_2)) \/ (chosen = N <=> elseAssert)
-      def nthIn(elemAndSet: (ArenaCell, ArenaCell), no: Int): (TBuilderInstruction, TBuilderInstruction) = {
+      def nthIn(elemAndSet: (ArenaCell, ArenaCell), no: Int): (BuilderT, BuilderT) = {
         if (elemsOfMemberSets(no).nonEmpty) {
           val inSet = tla.ite(tla.selectInSet(elemAndSet._1.toBuilder, elemAndSet._2.toBuilder), membershipEx,
               tla.storeNotInSet(picked.toBuilder, resultCell.toBuilder))
@@ -715,7 +714,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
       state: SymbState,
       oracle: Oracle,
       memberSeqs: Seq[ArenaCell],
-      elseAssert: TBuilderInstruction): SymbState = {
+      elseAssert: BuilderT): SymbState = {
     if (memberSeqs.isEmpty) {
       throw new RuntimeException("Picking a sequence from a statically empty set")
     } else if (memberSeqs.length == 1) {
@@ -738,7 +737,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
       state: SymbState,
       oracle: Oracle,
       memberSeqs: Seq[ArenaCell],
-      elseAssert: TBuilderInstruction): SymbState = {
+      elseAssert: BuilderT): SymbState = {
     rewriter.solverContext
       .log("; CHERRY-PICK %s FROM [%s] {".format(seqType, memberSeqs.map(_.toString).mkString(", ")))
 
@@ -829,7 +828,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
       state: SymbState,
       oracle: Oracle,
       funs: Seq[ArenaCell],
-      elseAssert: TBuilderInstruction): SymbState = {
+      elseAssert: BuilderT): SymbState = {
     rewriter.solverContext.log("; CHERRY-PICK %s FROM [%s] {".format(funType, funs.map(_.toString).mkString(", ")))
     var nextState = state
     rewriter.solverContext.config.smtEncoding match {
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/IntOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/IntOracle.scala
index 6e0e31ecb4..46bfd4dce0 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/IntOracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/IntOracle.scala
@@ -4,8 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState}
 import at.forsyte.apalache.tla.lir.{IntT1, ValEx}
 import at.forsyte.apalache.tla.lir.values.TlaInt
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * An oracle that uses an integer variable. Although using integers as an oracle is the most straightforward decision,
@@ -23,13 +22,13 @@ class IntOracle(val intCell: ArenaCell, nvalues: Int) extends Oracle {
 
   override def size: Int = nvalues
 
-  override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction =
+  override def whenEqualTo(state: SymbState, position: Int): BuilderT =
     tla.eql(intCell.toBuilder, tla.int(position))
 
   override def caseAssertions(
       state: SymbState,
-      assertions: Seq[TBuilderInstruction],
-      elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = {
+      assertions: Seq[BuilderT],
+      elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = {
     if (elseAssertions.nonEmpty && assertions.size != elseAssertions.size) {
       throw new IllegalStateException(s"Invalid call to Oracle, malformed elseAssertions")
     }
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MockOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MockOracle.scala
index c36e6ffa24..1c10c3c6d6 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MockOracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MockOracle.scala
@@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
 
 import at.forsyte.apalache.tla.bmcmt.SymbState
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * An oracle that always has the same value. This class specializes all methods to the case oracle == fixedValue.
@@ -16,14 +15,14 @@ class MockOracle(fixedValue: Int) extends Oracle {
 
   override def size: Int = fixedValue + 1
 
-  override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = {
+  override def whenEqualTo(state: SymbState, position: Int): BuilderT = {
     tla.bool(position == fixedValue)
   }
 
   override def caseAssertions(
       state: SymbState,
-      assertions: Seq[TBuilderInstruction],
-      elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction =
+      assertions: Seq[BuilderT],
+      elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT =
     assertions(fixedValue)
 
   override def evalPosition(solverContext: SolverContext, state: SymbState): Int =
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala
index 8762c1f364..78a746876f 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala
@@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
 
 import at.forsyte.apalache.tla.bmcmt.SymbState
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * An abstract version of an oracle that is used e.g. in CherryPick.
@@ -30,7 +29,7 @@ trait Oracle extends Serializable {
    * @param position
    *   a position the oracle should be equal to
    */
-  def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction
+  def whenEqualTo(state: SymbState, position: Int): BuilderT
 
   /**
    * Produce a ground expression that contains assertions for the possible oracle values.
@@ -46,8 +45,8 @@ trait Oracle extends Serializable {
    */
   def caseAssertions(
       state: SymbState,
-      assertions: Seq[TBuilderInstruction],
-      elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = {
+      assertions: Seq[BuilderT],
+      elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = {
     size match {
       // If the oracle has no candidate values, then caseAssertions should return a no-op for SMT, i.e. TRUE.
       case 0 => state.arena.cellTrue().toBuilder
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/OracleHelper.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/OracleHelper.scala
index 0a619b9c13..35b63d5777 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/OracleHelper.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/OracleHelper.scala
@@ -1,7 +1,7 @@
 package at.forsyte.apalache.tla.bmcmt.rules.aux
 
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * A helper class to create oracle values and compare them. In two previous solutions, we were using integers, then
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala
index 270bccea4c..5d67003924 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala
@@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
 
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.lir.SetT1
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * This class constructs the power set of S, that is, SUBSET S. Sometimes, this is just unavoidable, e.g., consider { Q
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PropositionalOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PropositionalOracle.scala
index f1f7dde250..025869aed5 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PropositionalOracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PropositionalOracle.scala
@@ -4,15 +4,15 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.bmcmt.types.CellTFrom
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter}
 import at.forsyte.apalache.tla.lir.BoolT1
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 
 class PropositionalOracle(bitCells: Seq[ArenaCell], nvalues: Int) extends Oracle {
 
   override def size: Int = nvalues
 
-  override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = {
-    def mkLits(n: Int, cells: Seq[ArenaCell]): Seq[TBuilderInstruction] = {
+  override def whenEqualTo(state: SymbState, position: Int): BuilderT = {
+    def mkLits(n: Int, cells: Seq[ArenaCell]): Seq[BuilderT] = {
       cells match {
         case Nil => Nil
 
@@ -35,8 +35,8 @@ class PropositionalOracle(bitCells: Seq[ArenaCell], nvalues: Int) extends Oracle
 
   override def caseAssertions(
       state: SymbState,
-      assertions: Seq[TBuilderInstruction],
-      elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = {
+      assertions: Seq[BuilderT],
+      elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = {
     if (elseAssertions.nonEmpty & assertions.size != elseAssertions.size) {
       throw new IllegalStateException(s"Invalid call to Oracle, malformed elseAssertions")
     }
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala
index dbcabd98e7..a776fea7e9 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter
 import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, UnknownT}
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, FixedElemPtr, SymbState, SymbStateRewriter}
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 import scala.collection.immutable.ArraySeq
 
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/RecordAndVariantOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/RecordAndVariantOps.scala
index 2032574ae1..8e4dd60f82 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/RecordAndVariantOps.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/RecordAndVariantOps.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.arena.{PtrUtil, PureArenaAdapter}
 import at.forsyte.apalache.tla.bmcmt.types.CellTFrom
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 import scala.collection.immutable.SortedMap
 
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SetOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SetOps.scala
index 1911df2866..d347a62d66 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SetOps.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SetOps.scala
@@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
 
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter}
 import at.forsyte.apalache.tla.lir.BoolT1
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * <p>A small collection of operations on sets that can be reused by rewriting rules.</p>
@@ -57,7 +56,7 @@ class SetOps(rewriter: SymbStateRewriter) {
       //   /\ c[i] \in S
       //   /\ \A j \in 0..(i - 1):
       //      ~b[j] \/ c[j] /= c[i]
-      def notSeen(j: Int): TBuilderInstruction = {
+      def notSeen(j: Int): BuilderT = {
         tla.or(tla.not(predicates(j).toBuilder), tla.not(tla.eql(c_i.toBuilder, elems(j).toBuilder)))
       }
 
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala
index 4112ea8563..b95064232b 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala
@@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
 
 import at.forsyte.apalache.tla.bmcmt.SymbState
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
+import at.forsyte.apalache.tla.types.{BuilderUT => BuilderT}
 
 /**
  * The oracle for sparse values, that is, a set S of naturals. This oracle is mapped on a smaller contiguous range
@@ -23,15 +23,15 @@ class SparseOracle(oracle: Oracle, val values: Set[Int]) extends Oracle {
 
   override def size: Int = values.size
 
-  override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = {
+  override def whenEqualTo(state: SymbState, position: Int): BuilderT = {
     assert(indexMap.contains(position))
     oracle.whenEqualTo(state, indexMap(position))
   }
 
   override def caseAssertions(
       state: SymbState,
-      assertions: Seq[TBuilderInstruction],
-      elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction =
+      assertions: Seq[BuilderT],
+      elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT =
     oracle.caseAssertions(state, assertions, elseAssertions)
 
   override def evalPosition(solverContext: SolverContext, state: SymbState): Int = {
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/UninterpretedConstOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/UninterpretedConstOracle.scala
index 4a01eb73ef..1fac909c43 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/UninterpretedConstOracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/UninterpretedConstOracle.scala
@@ -3,20 +3,20 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.lir.ConstT1
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 
 class UninterpretedConstOracle(valueCells: Seq[ArenaCell], oracleCell: ArenaCell, nvalues: Int) extends Oracle {
 
   override def size: Int = nvalues
 
-  override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction =
+  override def whenEqualTo(state: SymbState, position: Int): BuilderT =
     tla.eql(oracleCell.toBuilder, valueCells(position).toBuilder)
 
   override def caseAssertions(
       state: SymbState,
-      assertions: Seq[TBuilderInstruction],
-      elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = {
+      assertions: Seq[BuilderT],
+      elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = {
     if (elseAssertions.nonEmpty && assertions.size != elseAssertions.size) {
       throw new IllegalStateException(s"Invalid call to Oracle, malformed elseAssertions")
     }
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ValueGenerator.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ValueGenerator.scala
index 23784c3d16..66bd88d113 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ValueGenerator.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ValueGenerator.scala
@@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.bmcmt.types.{CellT, CellTFrom}
 import at.forsyte.apalache.tla.lir.TypedPredefs._
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.convenience.{tla => tlaLegacy}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 import scalaz.unused
 
 import scala.collection.immutable.{SortedMap, SortedSet}
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala
index edba7f30dc..88b674f175 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala
@@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
 
 import at.forsyte.apalache.tla.bmcmt.SymbState
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * [[ZipOracle]] is an optimization of [[Oracle]]. It groups several values of the background oracle together, in order
@@ -21,7 +20,7 @@ import at.forsyte.apalache.tla.types.tla
 class ZipOracle(backOracle: Oracle, groups: Seq[Seq[Int]]) extends Oracle {
   override def size: Int = groups.size
 
-  override def whenEqualTo(state: SymbState, index: Int): TBuilderInstruction = {
+  override def whenEqualTo(state: SymbState, index: Int): BuilderT = {
     assert(index < groups.size)
     val conds = groups(index).map(i => backOracle.whenEqualTo(state, i))
     tla.or(conds: _*)
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
index 883ec6bc89..0303ab7091 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
@@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter
 import at.forsyte.apalache.tla.bmcmt.profiler.{IdleSmtListener, SmtListener}
 import at.forsyte.apalache.tla.bmcmt.rewriter.ConstSimplifierForSmt
 import at.forsyte.apalache.tla.bmcmt.types._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.io.UTFPrinter
 import at.forsyte.apalache.tla.lir.oper._
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntRangeCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntRangeCache.scala
index db962c93a1..2f3cb6662c 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntRangeCache.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntRangeCache.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.bmcmt.types.CellT
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, FixedElemPtr, PureArena}
 import at.forsyte.apalache.tla.lir.{IntT1, SetT1}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Cache ranges a..b and, as a special case, tuple domains.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntValueCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntValueCache.scala
index 76e96e78fe..9002f4d476 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntValueCache.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntValueCache.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.bmcmt.types.CellT
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, PureArena}
 import at.forsyte.apalache.tla.lir.IntT1
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * A cache for integer constants that maps an integer to an integer constant in SMT.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/RecordDomainCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/RecordDomainCache.scala
index 23bef5c036..0eb8efa5c6 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/RecordDomainCache.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/RecordDomainCache.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.bmcmt.types.CellT
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, FixedElemPtr, PureArena}
 import at.forsyte.apalache.tla.lir.{SetT1, StrT1}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 import scala.collection.immutable.SortedSet
 
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala
index 2d1a7b9dac..6a62339b86 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.bmcmt.types.{CellT, CellTFrom}
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, PureArena}
 import at.forsyte.apalache.tla.lir.{ConstT1, StrT1, TlaType1}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * A cache for uninterpreted literals, that are translated to uninterpreted SMT constants, with a unique sort per
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/IntOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/IntOracle.scala
index fee661f0bb..38ad298eec 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/IntOracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/IntOracle.scala
@@ -5,8 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope
 import at.forsyte.apalache.tla.bmcmt.types.CellT
 import at.forsyte.apalache.tla.lir.{IntT1, ValEx}
 import at.forsyte.apalache.tla.lir.values.TlaInt
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * An oracle that uses an integer variable. Although using integers as an oracle is the most straightforward decision,
@@ -27,7 +26,7 @@ class IntOracle(val intCell: ArenaCell, nvalues: Int) extends Oracle {
    * Produce an expression that states that the chosen value equals to the value `v_{index}`. The actual implementation
    * may be different from an integer comparison.
    */
-  override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction =
+  override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT =
     tla.eql(intCell.toBuilder, tla.int(index))
 
   override def getIndexOfChosenValueFromModel(solverContext: SolverContext): BigInt =
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/MockOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/MockOracle.scala
index 53b288b0ce..09bb698e29 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/MockOracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/MockOracle.scala
@@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.oracles
 
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * An oracle that always has the same value. This class specializes all methods to the case oracle == fixedValue.
@@ -17,13 +16,13 @@ class MockOracle(fixedValue: Int) extends Oracle {
 
   override def size: Int = fixedValue + 1
 
-  override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction =
+  override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT =
     tla.bool(index == fixedValue)
 
   override def caseAssertions(
       scope: RewriterScope,
-      assertions: Seq[TBuilderInstruction],
-      elseAssertionsOpt: Option[Seq[TBuilderInstruction]] = None): TBuilderInstruction = {
+      assertions: Seq[BuilderT],
+      elseAssertionsOpt: Option[Seq[BuilderT]] = None): BuilderT = {
     require(assertions.size == this.size && elseAssertionsOpt.forall { _.size == this.size },
         s"Invalid call to Oracle, assertion sequences must have length $size.")
     assertions(fixedValue)
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala
index 26efc705ed..74238f4c78 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala
@@ -3,8 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.oracles
 import at.forsyte.apalache.tla.bmcmt.PureArena
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * An oracle provides a means of choosing a single value, out of a finite collection of candidate values. It can
@@ -29,7 +28,7 @@ trait Oracle {
    * Produce an expression that states that the chosen value equals to the value `v_{index}`. The actual implementation
    * may be different from an integer comparison.
    */
-  def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction
+  def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT
 
   /**
    * Produce a ground expression that contains assertions for the possible oracle values.
@@ -45,8 +44,8 @@ trait Oracle {
    */
   def caseAssertions(
       scope: RewriterScope,
-      assertions: Seq[TBuilderInstruction],
-      elseAssertionsOpt: Option[Seq[TBuilderInstruction]] = None): TBuilderInstruction = {
+      assertions: Seq[BuilderT],
+      elseAssertionsOpt: Option[Seq[BuilderT]] = None): BuilderT = {
     require(assertions.size == this.size && elseAssertionsOpt.forall { _.size == this.size },
         s"Invalid call to Oracle, assertion sequences must have length $size.")
     size match {
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/SparseOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/SparseOracle.scala
index 55c9255f41..e02c0ba337 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/SparseOracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/SparseOracle.scala
@@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.oracles
 
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * Given a set `indices` of size `N`, sparse oracle is able to answer {{{chosenValueIsEqualToIndexedValue(_, i),}}} for
@@ -30,7 +29,7 @@ class SparseOracle(mkOracle: Int => Oracle, val values: Set[Int]) extends Oracle
 
   override def size: Int = values.size
 
-  def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction =
+  def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT =
     indexMap
       .get(index.toInt)
       .map {
@@ -40,8 +39,8 @@ class SparseOracle(mkOracle: Int => Oracle, val values: Set[Int]) extends Oracle
 
   override def caseAssertions(
       scope: RewriterScope,
-      assertions: Seq[TBuilderInstruction],
-      elseAssertionsOpt: Option[Seq[TBuilderInstruction]] = None): TBuilderInstruction =
+      assertions: Seq[BuilderT],
+      elseAssertionsOpt: Option[Seq[BuilderT]] = None): BuilderT =
     oracle.caseAssertions(scope, assertions, elseAssertionsOpt)
 
   override def getIndexOfChosenValueFromModel(solverContext: SolverContext): BigInt = {
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/UninterpretedConstOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/UninterpretedConstOracle.scala
index 92e5549c93..bf1016cd91 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/UninterpretedConstOracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/UninterpretedConstOracle.scala
@@ -6,8 +6,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.UninterpretedLit
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope}
 import at.forsyte.apalache.tla.bmcmt.types.CellT
 import at.forsyte.apalache.tla.lir.ConstT1
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 
 /**
  * An oracle that uses a fixed collection of potential cells.
@@ -24,7 +24,7 @@ class UninterpretedConstOracle(val valueCells: Seq[ArenaCell], val oracleCell: A
    */
   override def size: Int = valueCells.size
 
-  override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction =
+  override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT =
     if (valueCells.indices.contains(index)) tla.eql(oracleCell.toBuilder, valueCells(index.toInt).toBuilder)
     else tla.bool(false)
 
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/ZipOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/ZipOracle.scala
index 054dac080a..240251b916 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/ZipOracle.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/ZipOracle.scala
@@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.oracles
 
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * [[ZipOracle]] is an optimization of [[Oracle]]. It groups several values of the background oracle together, in order
@@ -21,7 +20,7 @@ import at.forsyte.apalache.tla.types.tla
 class ZipOracle(backOracle: Oracle, groups: Seq[Seq[Int]]) extends Oracle {
   override def size: Int = groups.size
 
-  override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction =
+  override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT =
     if (groups.indices.contains(index)) {
       val conds = groups(index.toInt).map(i => backOracle.chosenValueIsEqualToIndexedValue(scope, i))
       tla.or(conds: _*)
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/IntConstStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/IntConstStratifiedRule.scala
index f82de7f822..3737632188 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/IntConstStratifiedRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/IntConstStratifiedRule.scala
@@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.IntValueCache
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope, StratifiedRule}
 import at.forsyte.apalache.tla.lir.values.TlaInt
 import at.forsyte.apalache.tla.lir.{TlaEx, ValEx}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Rewrites integer constants.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/AndStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/AndStratifiedRule.scala
index 26ffcdf960..76bee4f8fc 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/AndStratifiedRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/AndStratifiedRule.scala
@@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope}
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{addCell, StratifiedRule}
 import at.forsyte.apalache.tla.lir.oper.TlaBoolOper
 import at.forsyte.apalache.tla.lir.{BoolT1, OperEx, TlaEx}
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * Implements the rule for conjunction.
@@ -20,8 +19,7 @@ import at.forsyte.apalache.tla.types.tla
  * @author
  *   Jure Kukovec
  */
-class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false)
-    extends StratifiedRule[Option[TBuilderInstruction]] {
+class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) extends StratifiedRule[Option[BuilderT]] {
   private val simplifier = new ConstSimplifierForSmt()
 
   override def isApplicable(ex: TlaEx, scope: RewriterScope): Boolean = ex match {
@@ -32,7 +30,7 @@ class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false)
   override def buildArena(ex: TlaEx)(startingScope: RewriterScope): (
       RewriterScope,
       ArenaCell,
-      Option[TBuilderInstruction]) = simplifier.simplifyShallow(ex) match {
+      Option[BuilderT]) = simplifier.simplifyShallow(ex) match {
     case OperEx(TlaBoolOper.and, args @ _*) =>
       if (args.isEmpty) {
         // empty conjunction is always true
@@ -40,9 +38,9 @@ class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false)
       } else {
         // use short-circuiting on state-level expressions (like in TLC)
 
-        def toIte(es: Seq[TlaEx]): TBuilderInstruction = {
+        def toIte(es: Seq[TlaEx]): BuilderT = {
           // assume es is nonempty
-          es.map(tla.unchecked).reduceRight[TBuilderInstruction] { case (elem, partial) =>
+          es.map(tla.unchecked).reduceRight[BuilderT] { case (elem, partial) =>
             tla.ite(elem, partial, PureArena.cellFalse(startingScope.arena).toBuilder)
           }
         }
@@ -58,7 +56,7 @@ class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false)
 
           val (newScope, rewrittenArgCells) =
             // With AND all blocks belong to the same scope, so we have to propagate it
-            args.foldLeft((startingScope.copy(arena = arenaWithAndCell), Seq.empty[TBuilderInstruction])) {
+            args.foldLeft((startingScope.copy(arena = arenaWithAndCell), Seq.empty[BuilderT])) {
               case ((scope, cellSeq), term) =>
                 val (newScope, termCell) = rewriter.rewrite(term)(scope)
                 (newScope, cellSeq :+ termCell.toBuilder)
@@ -74,7 +72,7 @@ class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false)
       (scope, cell, None)
   }
 
-  override def addConstraints(scope: RewriterScope, cell: ArenaCell, auxData: Option[TBuilderInstruction]): Unit = {
+  override def addConstraints(scope: RewriterScope, cell: ArenaCell, auxData: Option[BuilderT]): Unit = {
     // Only add constraints, if ITE rewriting didn't fire (in that case, the ITE rule does it for us)
     auxData.foreach { conjunction =>
       rewriter.assert(tla.eql(cell.toBuilder, conjunction))
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/OrStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/OrStratifiedRule.scala
index 187803e49c..93233c86fa 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/OrStratifiedRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/OrStratifiedRule.scala
@@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{addCell, StratifiedRule}
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope}
 import at.forsyte.apalache.tla.lir.{BoolT1, OperEx, TlaEx}
 import at.forsyte.apalache.tla.lir.oper.TlaBoolOper
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * Implements the rule for disjunction.
@@ -20,8 +19,7 @@ import at.forsyte.apalache.tla.types.tla
  * @author
  *   Jure Kukovec
  */
-class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false)
-    extends StratifiedRule[Option[TBuilderInstruction]] {
+class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) extends StratifiedRule[Option[BuilderT]] {
   private val simplifier = new ConstSimplifierForSmt()
 
   override def isApplicable(ex: TlaEx, scope: RewriterScope): Boolean = ex match {
@@ -32,7 +30,7 @@ class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false)
   override def buildArena(ex: TlaEx)(startingScope: RewriterScope): (
       RewriterScope,
       ArenaCell,
-      Option[TBuilderInstruction]) = simplifier.simplifyShallow(ex) match {
+      Option[BuilderT]) = simplifier.simplifyShallow(ex) match {
     case OperEx(TlaBoolOper.or, args @ _*) =>
       if (args.isEmpty) {
         // empty disjunction is always false
@@ -40,9 +38,9 @@ class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false)
       } else {
         // use short-circuiting on state-level expressions (like in TLC)
 
-        def toIte(es: Seq[TlaEx]): TBuilderInstruction = {
+        def toIte(es: Seq[TlaEx]): BuilderT = {
           // assume es is nonempty
-          es.map(tla.unchecked).reduceRight[TBuilderInstruction] { case (elem, partial) =>
+          es.map(tla.unchecked).reduceRight[BuilderT] { case (elem, partial) =>
             tla.ite(elem, PureArena.cellTrue(startingScope.arena).toBuilder, partial)
           }
         }
@@ -71,7 +69,7 @@ class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false)
       (scope, cell, None)
   }
 
-  override def addConstraints(scope: RewriterScope, cell: ArenaCell, auxData: Option[TBuilderInstruction]): Unit = {
+  override def addConstraints(scope: RewriterScope, cell: ArenaCell, auxData: Option[BuilderT]): Unit = {
     // Only add constraints, if ITE rewriting didn't fire (in that case, the ITE rule does it for us)
     auxData.foreach { disjunction =>
       rewriter.assert(tla.eql(cell.toBuilder, disjunction))
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCtorStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCtorStratifiedRule.scala
index f0fb928416..88572fa324 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCtorStratifiedRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCtorStratifiedRule.scala
@@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope}
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{addCell, StratifiedRule}
 import at.forsyte.apalache.tla.lir.oper.TlaSetOper
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Rewrites the set constructor {e_1, ..., e_k}.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCupStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCupStratifiedRule.scala
index ad4d437819..73d284806a 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCupStratifiedRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCupStratifiedRule.scala
@@ -6,6 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope, S
 import at.forsyte.apalache.tla.bmcmt.types.CellT
 import at.forsyte.apalache.tla.lir.oper.TlaSetOper
 import at.forsyte.apalache.tla.lir.{OperEx, TlaEx}
+import at.forsyte.apalache.tla.typecomp._
 
 /**
  * Rewrites X \cup Y, that is, a union of two sets (not UNION).
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetFilterStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetFilterStratifiedRule.scala
index 78156496c8..63b3520b1e 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetFilterStratifiedRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetFilterStratifiedRule.scala
@@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{addCell, Rewriter, Rewrite
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaSetOper
 import at.forsyte.apalache.tla.lir.values.{TlaIntSet, TlaNatSet}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Rewrites a set comprehension { x \in S: P }.
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala
index 911ede25ce..c540f12e9d 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala
@@ -3,10 +3,10 @@ package at.forsyte.apalache.tla.bmcmt
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker
 import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
 import org.scalatest.funsuite.FixtureAnyFunSuite
 
 import java.io.StringWriter
@@ -19,7 +19,7 @@ trait RewriterBase extends FixtureAnyFunSuite {
 
   protected val renaming = new IncrementalRenaming(new IdleTracker)
 
-  protected def assertBuildEqual(a: TBuilderInstruction, b: TBuilderInstruction): Unit =
+  protected def assertBuildEqual(a: BuilderT, b: BuilderT): Unit =
     assert(a.build == b.build)
 
   protected def create(rewriterType: SMTEncoding): SymbStateRewriter = {
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCherryPick.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCherryPick.scala
index cacf67134a..bef6f6dabc 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCherryPick.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCherryPick.scala
@@ -3,10 +3,9 @@ package at.forsyte.apalache.tla.bmcmt
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, Oracle, OracleFactory}
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla._
 import at.forsyte.apalache.tla.types.parser.DefaultType1Parser
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.types.tlaU._
 
 trait TestCherryPick extends RewriterBase {
   private val parser = DefaultType1Parser
@@ -171,7 +170,7 @@ trait TestCherryPick extends RewriterBase {
     state = oracleState
 
     def mkRecord(i: Int, j: Int): ArenaCell = {
-      val rec = tla.rec("a" -> int(i), "b" -> int(j)).map(_.withTag(Typed(recordT)))
+      val rec = tla.rec("a" -> int(i), "b" -> int(j)).withTag(Typed(recordT))
       state = rewriter.rewriteUntilDone(state.setRex(rec))
       state.asCell
     }
@@ -351,7 +350,7 @@ trait TestCherryPick extends RewriterBase {
     val (oracleState, oracle) = new OracleFactory(rewriter).newConstOracle(state, 2)
     state = oracleState
 
-    def mkFun(dom: TBuilderInstruction, map: TBuilderInstruction): ArenaCell = {
+    def mkFun(dom: BuilderT, map: BuilderT): ArenaCell = {
       val fun = funDef(map, name("x", IntT1) -> dom)
       state = rewriter.rewriteUntilDone(state.setRex(fun))
       state.asCell
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateDecoder.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateDecoder.scala
index b3de34187d..a83152a9d7 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateDecoder.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateDecoder.scala
@@ -3,19 +3,19 @@ package at.forsyte.apalache.tla.bmcmt
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaSetOper
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
 import at.forsyte.apalache.tla.types.parser.DefaultType1Parser
-import at.forsyte.apalache.tla.types.tla
-import at.forsyte.apalache.tla.types.tla._
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
+import at.forsyte.apalache.tla.types.tlaU._
 
 trait TestSymbStateDecoder extends RewriterBase {
   private val parser = DefaultType1Parser
   private val int2 = parser("<<Int, Int>>")
 
-  private def pair(i: Int, j: Int): TBuilderInstruction = tuple(int(i), int(j))
+  private def pair(i: Int, j: Int): BuilderT = tuple(int(i), int(j))
 
   test("decode bool") { rewriterType: SMTEncoding =>
-    val originalEx: TBuilderInstruction = bool(true)
+    val originalEx: BuilderT = bool(true)
     val state = new SymbState(originalEx, arena, Binding())
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
@@ -45,7 +45,7 @@ trait TestSymbStateDecoder extends RewriterBase {
   }
 
   test("decode str") { rewriterType: SMTEncoding =>
-    val originalEx: TBuilderInstruction = str("hello")
+    val originalEx: BuilderT = str("hello")
     val state = new SymbState(originalEx, arena, Binding())
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
@@ -141,7 +141,7 @@ trait TestSymbStateDecoder extends RewriterBase {
     val decoder = new SymbStateDecoder(solverContext, rewriter)
     val decodedEx = decoder.decodeCellToTlaEx(nextState.arena, cell)
 
-    val expectedOutcome: TBuilderInstruction = setAsFun(enumSet(pair(1, 2), pair(2, 3)))
+    val expectedOutcome: BuilderT = setAsFun(enumSet(pair(1, 2), pair(2, 3)))
     assertBuildEqual(expectedOutcome, decodedEx)
   }
 
@@ -180,7 +180,7 @@ trait TestSymbStateDecoder extends RewriterBase {
 
   test("decode dynamically empty fun") { rewriterType: SMTEncoding =>
     // this domain is not empty at the arena level, but it is in every SMT model
-    def dynEmpty(left: TBuilderInstruction): TBuilderInstruction =
+    def dynEmpty(left: BuilderT): BuilderT =
       filter(name("t", IntT1), left, bool(false))
 
     val domEx = dynEmpty(enumSet(int(1)))
@@ -246,7 +246,7 @@ trait TestSymbStateDecoder extends RewriterBase {
     val recEx = rec(
         "a" -> int(1),
         "b" -> bool(true),
-    ).map(_.withTag(Typed(parser("{ a: Int, b: Bool }"))))
+    ).withTag(Typed(parser("{ a: Int, b: Bool }")))
     val state = new SymbState(recEx, arena, Binding())
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala
index b741f7255f..cbd771fabb 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala
@@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt.SymbStateRewriter.Continue
 import at.forsyte.apalache.tla.lir.IntT1
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
+import at.forsyte.apalache.tla.typecomp._
 
 trait TestSymbStateRewriterAction extends RewriterBase {
   test("""x' is rewritten to the binding of x'""") { rewriterType: SMTEncoding =>
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterApalacheGen.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterApalacheGen.scala
index 063e46ec2e..5d64a3a6be 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterApalacheGen.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterApalacheGen.scala
@@ -6,7 +6,8 @@ import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.convenience.{tla => tlaLegacy}
 import at.forsyte.apalache.tla.lir.oper.ApalacheOper
 import at.forsyte.apalache.tla.types.parser.DefaultType1Parser
-import at.forsyte.apalache.tla.types.tla._
+import at.forsyte.apalache.tla.types.tlaU._
+import at.forsyte.apalache.tla.typecomp._
 
 trait TestSymbStateRewriterApalacheGen extends RewriterBase {
   private val parser = DefaultType1Parser
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala
index 09dac17186..ede1eb8a8b 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala
@@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt
 
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla._
+import at.forsyte.apalache.tla.types.{BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.types.tlaU._
 
 /**
  * Tests for assignments. The assignments were at the core of Apalache 0.5.x. In Apalache 0.6.x, they are preprocessed
@@ -12,19 +12,19 @@ import at.forsyte.apalache.tla.types.tla._
 trait TestSymbStateRewriterAssignment extends RewriterBase {
   val ibI: TlaType1 = TupT1(IntT1, BoolT1, SetT1(IntT1))
 
-  private val set12: TBuilderInstruction = enumSet(int(1), int(2))
-  private val x_prime: TBuilderInstruction = prime(name("x", IntT1))
-  private val x_primeS: TBuilderInstruction = prime(name("x", SetT1(IntT1)))
-  private val x_primeFbi: TBuilderInstruction = prime(name("x", FunT1(BoolT1, IntT1)))
-  private val x_primeFii: TBuilderInstruction = prime(name("x", FunT1(IntT1, IntT1)))
-  private val x_primeFib: TBuilderInstruction = prime(name("x", FunT1(IntT1, BoolT1)))
-  private val y_prime: TBuilderInstruction = prime(name("y", IntT1))
-  private val boundName: TBuilderInstruction = name("t", IntT1)
-  private val boundNameS: TBuilderInstruction = name("t", SetT1(IntT1))
-  private val boundNameFbi: TBuilderInstruction = name("t", FunT1(BoolT1, IntT1))
-  private val boundNameFii: TBuilderInstruction = name("t", FunT1(IntT1, IntT1))
-  private val boundNameFib: TBuilderInstruction = name("t", FunT1(IntT1, BoolT1))
-  private val boolset: TBuilderInstruction = enumSet(bool(false), bool(true))
+  private val set12: BuilderT = enumSet(int(1), int(2))
+  private val x_prime: BuilderT = prime(name("x", IntT1))
+  private val x_primeS: BuilderT = prime(name("x", SetT1(IntT1)))
+  private val x_primeFbi: BuilderT = prime(name("x", FunT1(BoolT1, IntT1)))
+  private val x_primeFii: BuilderT = prime(name("x", FunT1(IntT1, IntT1)))
+  private val x_primeFib: BuilderT = prime(name("x", FunT1(IntT1, BoolT1)))
+  private val y_prime: BuilderT = prime(name("y", IntT1))
+  private val boundName: BuilderT = name("t", IntT1)
+  private val boundNameS: BuilderT = name("t", SetT1(IntT1))
+  private val boundNameFbi: BuilderT = name("t", FunT1(BoolT1, IntT1))
+  private val boundNameFii: BuilderT = name("t", FunT1(IntT1, IntT1))
+  private val boundNameFib: BuilderT = name("t", FunT1(IntT1, BoolT1))
+  private val boolset: BuilderT = enumSet(bool(false), bool(true))
 
   test("""\E t \in {1, 2}: x' \in {t} ~~> TRUE and [x -> $C$k]""") { rewriterType: SMTEncoding =>
     val asgn = skolem(exists(boundName, set12, assign(x_prime, boundName)))
@@ -98,7 +98,7 @@ trait TestSymbStateRewriterAssignment extends RewriterBase {
 
   test("""\E t \in \in {t_2 \in {1}: FALSE}: x' \in {t} ~~> FALSE""") { rewriterType: SMTEncoding =>
     // a regression test
-    def empty(set: TBuilderInstruction): TBuilderInstruction = {
+    def empty(set: BuilderT): BuilderT = {
       filter(name("t_2", IntT1), set, bool(false))
     }
 
@@ -181,7 +181,7 @@ trait TestSymbStateRewriterAssignment extends RewriterBase {
   test("""\E t \in {{1, 2}, {1+1, 2, 3}} \ {{2, 3}}: x' \in {t} ~~> TRUE and [x -> $C$k]""") {
     rewriterType: SMTEncoding =>
       // equal elements in different sets mess up picking from a set
-      def setminus(left: TBuilderInstruction, right: TBuilderInstruction): TBuilderInstruction = {
+      def setminus(left: BuilderT, right: BuilderT): BuilderT = {
         // this is how Keramelizer translates setminus
         filter(name("t_2", SetT1(IntT1)), left, not(eql(name("t_2", SetT1(IntT1)), right)))
 
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala
index 8d60b6fdca..0181f58083 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala
@@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt
 
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.lir.IntT1
-import at.forsyte.apalache.tla.types.tla._
+import at.forsyte.apalache.tla.types.tlaU._
 
 trait TestSymbStateRewriterChooseOrGuess extends RewriterBase {
   test("""CHOOSE x \in { 1, 2, 3 }: x > 1""") { rewriterType: SMTEncoding =>
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala
index 6a712f5161..57699ff2e0 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala
@@ -3,8 +3,8 @@ package at.forsyte.apalache.tla.bmcmt
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla._
+import at.forsyte.apalache.tla.types.{BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.types.tlaU._
 
 trait TestSymbStateRewriterFunSet extends RewriterBase {
   val i_to_B: TlaType1 = FunT1(IntT1, SetT1(BoolT1))
@@ -172,7 +172,7 @@ trait TestSymbStateRewriterFunSet extends RewriterBase {
   // this should be redundant in the presence of #91
   test("""[x \in {0, 1, 2} \ {0} |-> 3] \in [{1, 2} -> {3, 4}]""") { rewriterType: SMTEncoding =>
     // although 0 is in the function domain at the arena level, it does not belong to the set difference
-    def setminus(set: TBuilderInstruction, intVal: BigInt): TBuilderInstruction = {
+    def setminus(set: BuilderT, intVal: BigInt): BuilderT = {
       filter(name("t", IntT1), set, not(eql(name("t", IntT1), int(intVal))))
 
     }
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRecord.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRecord.scala
index fbe0d667d2..16e37f9ded 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRecord.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRecord.scala
@@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.bmcmt
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla._
+import at.forsyte.apalache.tla.types.tlaU._
 
 import scala.collection.immutable.{SortedMap, SortedSet, TreeMap}
 
@@ -82,7 +82,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase {
     val record = rec(
         "a" -> int(1),
         "b" -> bool(false),
-    ).map { _.withTag(Typed(ribs)) }
+    ).withTag(Typed(ribs))
     // We assume that record has the type RecT1("a" -> IntT1, "b" -> BoolT1, "c" -> StrT1).
     // This can happen due to type unification. The record access should still work,
     // though the access is expected to produce an arbitrary value (of proper type).
@@ -130,7 +130,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase {
     val record1 = rec(
         "a" -> int(1),
         "b" -> bool(false),
-    ).map { _.withTag(Typed(ribs)) }
+    ).withTag(Typed(ribs))
     val record2 = rec(
         "a" -> int(2),
         "b" -> bool(true),
@@ -165,7 +165,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase {
       // and then -- when knowing the type of the filtered records -- map them somewhere.
       // Although, it is not easy to do in a symbolic encoding, we support this idiom.
       // We require though that all the records have type-compatible fields.
-      val record1 = rec("a" -> int(1)).map { _.withTag(Typed(rii)) }
+      val record1 = rec("a" -> int(1)).withTag(Typed(rii))
       val record2 = rec("a" -> int(2), "c" -> int(3))
       // Records in a set can have different sets of keys. This requires a type annotation.
       val setEx = enumSet(record1, record2)
@@ -207,7 +207,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase {
         "b" -> bool(false),
         "c" -> str("d"),
     )
-    val record2 = rec("a" -> int(1)).map { _.withTag(Typed(ribs)) }
+    val record2 = rec("a" -> int(1)).withTag(Typed(ribs))
     val eq = not(eql(record1, record2))
     val state = new SymbState(eq, arena, Binding())
     val rewriter = create(rewriterType)
@@ -229,7 +229,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase {
   }
 
   test("""DOMAIN [a |-> 1] = {"a"} under type annotations!""") { rewriterType: SMTEncoding =>
-    val record = rec("a" -> int(1)).map(_.withTag(Typed(ribs)))
+    val record = rec("a" -> int(1)).withTag(Typed(ribs))
     val domain = dom(record)
     val eq = eql(domain, enumSet(str("a")))
     val state = new SymbState(eq, arena, Binding())
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala
index aea018c7dd..29c525816b 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala
@@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt
 
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 trait TestSymbStateRewriterRepeat extends RewriterBase {
   test("""Repeat(LET Op(a,i) == a + 1 IN Op, 5, 0) = 5""") { rewriterType: SMTEncoding =>
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestPropositionalOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestPropositionalOracle.scala
index 04a8b1f0f7..1302906eac 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestPropositionalOracle.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestPropositionalOracle.scala
@@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt.{Binding, RewriterBase, SymbState}
 import at.forsyte.apalache.tla.lir.{BoolT1, TestingPredefs}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
+import at.forsyte.apalache.tla.typecomp._
 
 trait TestPropositionalOracle extends RewriterBase with TestingPredefs {
   test("""Propositional Oracle.create""") { rewriterType: SMTEncoding =>
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala
index 23715cdc85..2bfbe1256e 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala
@@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt.{Binding, RewriterBase, SymbState}
 import at.forsyte.apalache.tla.lir.{BoolT1, TestingPredefs}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
+import at.forsyte.apalache.tla.typecomp._
 
 trait TestSparseOracle extends RewriterBase with TestingPredefs {
   test("""Sparse Oracle.create""") { rewriterType: SMTEncoding =>
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestUninterpretedConstOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestUninterpretedConstOracle.scala
index 9c25fbee6c..8533863012 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestUninterpretedConstOracle.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestUninterpretedConstOracle.scala
@@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt.{Binding, RewriterBase, SymbState}
 import at.forsyte.apalache.tla.lir.{BoolT1, TestingPredefs}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
+import at.forsyte.apalache.tla.typecomp._
 
 trait TestUninterpretedConstOracle extends RewriterBase with TestingPredefs {
   test("""UninterpretedConst Oracle.create""") { rewriterType: SMTEncoding =>
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala
index 56052ad099..4149cd7fa7 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala
@@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.smt
 
 import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter
 import at.forsyte.apalache.tla.lir.IntT1
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 import org.scalatest.funsuite.AnyFunSuite
 
 /**
@@ -13,7 +13,7 @@ import org.scalatest.funsuite.AnyFunSuite
 trait TestRecordingSolverContext extends AnyFunSuite {
   protected var solverConfig: SolverConfig = _
 
-  private val int42: TBuilderInstruction = tla.int(42)
+  private val int42: BuilderT = tla.int(42)
 
   test("operations proxied") {
     val solver = RecordingSolverContext.createZ3(None, solverConfig)
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/ApalacheRewriterTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/ApalacheRewriterTest.scala
index b7868f2683..dfeb025d37 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/ApalacheRewriterTest.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/ApalacheRewriterTest.scala
@@ -3,8 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.apalache.AssignmentStratifiedRule
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, Binding, PureArena}
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 import org.junit.runner.RunWith
 import org.scalatest.BeforeAndAfterEach
 import org.scalatest.funsuite.AnyFunSuite
@@ -27,7 +26,7 @@ class ApalacheRewriterTest extends AnyFunSuite with BeforeAndAfterEach {
 
     val rule = new AssignmentStratifiedRule(rewriter)
 
-    def assignTo(lhs: TBuilderInstruction, rhs: TBuilderInstruction = tla.int(1)): TBuilderInstruction =
+    def assignTo(lhs: BuilderT, rhs: BuilderT = tla.int(1)): BuilderT =
       tla.assign(tla.prime(lhs), rhs)
 
     val startScope = RewriterScope.initial()
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/BoolRewriterTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/BoolRewriterTest.scala
index 9736d3d815..04a12f6a2b 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/BoolRewriterTest.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/BoolRewriterTest.scala
@@ -2,7 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules
 
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, Binding, PureArena}
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
+import at.forsyte.apalache.tla.typecomp._
 import org.junit.runner.RunWith
 import org.scalatest.BeforeAndAfterEach
 import org.scalatest.funsuite.AnyFunSuite
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/IntRewriterTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/IntRewriterTest.scala
index 21e75e24cd..916f15299c 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/IntRewriterTest.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/IntRewriterTest.scala
@@ -1,7 +1,8 @@
 package at.forsyte.apalache.tla.bmcmt.stratifiedRules
 
 import at.forsyte.apalache.tla.lir.{IntT1, NameEx, SetT1, Typed}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
+import at.forsyte.apalache.tla.typecomp._
 import org.junit.runner.RunWith
 import org.scalatest.BeforeAndAfterEach
 import org.scalatest.funsuite.AnyFunSuite
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/SetRewriterTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/SetRewriterTest.scala
index 562a148bf3..7332b32b19 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/SetRewriterTest.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/SetRewriterTest.scala
@@ -4,7 +4,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.set.SetFilterStratifiedRule
 import at.forsyte.apalache.tla.bmcmt.types.CellT
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
+import at.forsyte.apalache.tla.typecomp._
 import org.junit.runner.RunWith
 import org.scalatest.BeforeAndAfterEach
 import org.scalatest.funsuite.AnyFunSuite
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntRangeCacheTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntRangeCacheTest.scala
index 4b83e8acb8..6494248f02 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntRangeCacheTest.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntRangeCacheTest.scala
@@ -2,7 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux
 
 import at.forsyte.apalache.tla.bmcmt.PureArena
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.{IntRangeCache, IntValueCache}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
+import at.forsyte.apalache.tla.typecomp._
 import org.junit.runner.RunWith
 import org.scalatest.BeforeAndAfterEach
 import org.scalatest.funsuite.AnyFunSuite
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntValueCacheTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntValueCacheTest.scala
index 7895f465c8..2193bb49cb 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntValueCacheTest.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntValueCacheTest.scala
@@ -2,7 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux
 
 import at.forsyte.apalache.tla.bmcmt.PureArena
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.IntValueCache
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
+import at.forsyte.apalache.tla.typecomp._
 import org.junit.runner.RunWith
 import org.scalatest.BeforeAndAfterEach
 import org.scalatest.funsuite.AnyFunSuite
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/RecordDomainCacheTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/RecordDomainCacheTest.scala
index 004243cf2a..f99923ad5b 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/RecordDomainCacheTest.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/RecordDomainCacheTest.scala
@@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux
 import at.forsyte.apalache.tla.bmcmt.PureArena
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.{RecordDomainCache, UninterpretedLiteralCache}
 import at.forsyte.apalache.tla.lir.{StrT1, TlaType1}
-import at.forsyte.apalache.tla.types.{tla, ModelValueHandler}
+import at.forsyte.apalache.tla.types.{tlaU => tla, ModelValueHandler}
+import at.forsyte.apalache.tla.typecomp._
 import org.junit.runner.RunWith
 import org.scalatest.BeforeAndAfterEach
 import org.scalatest.funsuite.AnyFunSuite
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala
index 868cfa9e87..a9083a80d5 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala
@@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux
 import at.forsyte.apalache.tla.bmcmt.PureArena
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.UninterpretedLiteralCache
 import at.forsyte.apalache.tla.lir.{StrT1, TlaType1}
-import at.forsyte.apalache.tla.types.{tla, ModelValueHandler}
+import at.forsyte.apalache.tla.types.{tlaU => tla, ModelValueHandler}
+import at.forsyte.apalache.tla.typecomp._
 import org.junit.runner.RunWith
 import org.scalatest.BeforeAndAfterEach
 import org.scalatest.funsuite.AnyFunSuite
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestIntOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestIntOracle.scala
index 8485c3f3e4..d24d073693 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestIntOracle.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestIntOracle.scala
@@ -7,8 +7,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope
 import at.forsyte.apalache.tla.lir.{BoolT1, NameEx, OperEx, TlaEx, ValEx}
 import at.forsyte.apalache.tla.lir.oper.TlaOper
 import at.forsyte.apalache.tla.lir.values.TlaInt
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 import org.junit.runner.RunWith
 import org.scalacheck.{Gen, Prop}
 import org.scalacheck.Prop.forAll
@@ -62,7 +62,7 @@ class TestIntOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers {
 
   }
 
-  val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0
+  val (assertionsA, assertionsB): (Seq[BuilderT], Seq[BuilderT]) = 0
     .to(10)
     .map { i =>
       (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1))
@@ -70,7 +70,7 @@ class TestIntOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers {
     .unzip
 
   test("caseAssertions requires assertion sequences of equal length") {
-    val assertionsGen: Gen[(Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for {
+    val assertionsGen: Gen[(Seq[BuilderT], Option[Seq[BuilderT]])] = for {
       i <- Gen.choose(0, assertionsA.size)
       j <- Gen.choose(0, assertionsB.size)
       opt <- Gen.option(Gen.const(assertionsB.take(j)))
@@ -91,7 +91,7 @@ class TestIntOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers {
   }
 
   test("caseAssertions constructs a collection of ITEs, or shorthands") {
-    val gen: Gen[(Int, Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for {
+    val gen: Gen[(Int, Seq[BuilderT], Option[Seq[BuilderT]])] = for {
       size <- nonNegIntGen
       opt <- Gen.option(Gen.const(assertionsB.take(size)))
     } yield (size, assertionsA.take(size), opt)
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestMockOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestMockOracle.scala
index 74afa816a8..a1c065d805 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestMockOracle.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestMockOracle.scala
@@ -4,8 +4,8 @@ import at.forsyte.apalache.tla.bmcmt.smt.{SolverConfig, Z3SolverContext}
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.values.TlaBool
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 import org.junit.runner.RunWith
 import org.scalacheck.Prop.forAll
 import org.scalacheck.{Gen, Prop}
@@ -58,7 +58,7 @@ class TestMockOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers {
     check(prop, minSuccessful(1000), sizeRange(4))
   }
 
-  val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0
+  val (assertionsA, assertionsB): (Seq[BuilderT], Seq[BuilderT]) = 0
     .to(10)
     .map { i =>
       (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1))
@@ -66,7 +66,7 @@ class TestMockOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers {
     .unzip
 
   test("caseAssertions requires assertion sequences of equal length") {
-    val assertionsGen: Gen[(Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for {
+    val assertionsGen: Gen[(Seq[BuilderT], Option[Seq[BuilderT]])] = for {
       i <- Gen.choose(0, assertionsA.size)
       j <- Gen.choose(0, assertionsB.size)
       opt <- Gen.option(Gen.const(assertionsB.take(j)))
@@ -86,7 +86,7 @@ class TestMockOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers {
   }
 
   test("caseAssertions always shorthands") {
-    val gen: Gen[(Int, Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for {
+    val gen: Gen[(Int, Seq[BuilderT], Option[Seq[BuilderT]])] = for {
       fixed <- nonNegIntGen
       opt <- Gen.option(Gen.const(assertionsB.take(fixed + 1)))
     } yield (fixed, assertionsA.take(fixed + 1), opt)
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestSparseOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestSparseOracle.scala
index c2c40e1007..a7b09be08c 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestSparseOracle.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestSparseOracle.scala
@@ -6,8 +6,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope
 import at.forsyte.apalache.tla.bmcmt.types.CellT
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, PureArena}
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 import org.junit.runner.RunWith
 import org.scalacheck.Gen
 import org.scalacheck.Prop.forAll
@@ -59,7 +59,7 @@ class TestSparseOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers
     check(prop, minSuccessful(1000), sizeRange(4))
   }
 
-  val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0
+  val (assertionsA, assertionsB): (Seq[BuilderT], Seq[BuilderT]) = 0
     .to(10)
     .map { i =>
       (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1))
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala
index 6688fbc3df..4b047c464c 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala
@@ -7,8 +7,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.UninterpretedLit
 import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope, TestingRewriter}
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaOper
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 import org.junit.runner.RunWith
 import org.scalacheck.Prop.forAll
 import org.scalacheck.{Gen, Prop}
@@ -69,7 +69,7 @@ class TestUninterpretedConstOracle extends AnyFunSuite with BeforeAndAfterEach w
     check(prop, minSuccessful(200), sizeRange(4))
   }
 
-  val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0
+  val (assertionsA, assertionsB): (Seq[BuilderT], Seq[BuilderT]) = 0
     .to(10)
     .map { i =>
       (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1))
@@ -77,7 +77,7 @@ class TestUninterpretedConstOracle extends AnyFunSuite with BeforeAndAfterEach w
     .unzip
 
   test("caseAssertions requires assertion sequences of equal length") {
-    val assertionsGen: Gen[(Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for {
+    val assertionsGen: Gen[(Seq[BuilderT], Option[Seq[BuilderT]])] = for {
       i <- Gen.choose(0, assertionsA.size)
       j <- Gen.choose(0, assertionsB.size)
       opt <- Gen.option(Gen.const(assertionsB.take(j)))
@@ -97,7 +97,7 @@ class TestUninterpretedConstOracle extends AnyFunSuite with BeforeAndAfterEach w
   }
 
   test("caseAssertions constructs a collection of ITEs, or shorthands") {
-    val gen: Gen[(Int, Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for {
+    val gen: Gen[(Int, Seq[BuilderT], Option[Seq[BuilderT]])] = for {
       size <- nonNegIntGen
       opt <- Gen.option(Gen.const(assertionsB.take(size)))
     } yield (size, assertionsA.take(size), opt)
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala
index 0b544e080a..ed9044555b 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala
@@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.trex
 
 import at.forsyte.apalache.tla.bmcmt.{Binding, StateInvariant}
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 
 /**
  * An abstract test suite that is parameterized by the snapshot type.
@@ -16,8 +16,8 @@ import at.forsyte.apalache.tla.types.tla
  */
 trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
 
-  def nX: TBuilderInstruction = tla.name("x", IntT1)
-  def nY: TBuilderInstruction = tla.name("y", IntT1)
+  def nX: BuilderT = tla.name("x", IntT1)
+  def nY: BuilderT = tla.name("y", IntT1)
 
   test("constant initialization") { exeCtx: ExecutorContextT =>
     // N' <- 1
@@ -129,7 +129,7 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
     // state 1 is produced by transition 1
     assert(1 == decPath(1)._2)
 
-    def mapWithBuild(pairs: (String, TBuilderInstruction)*): Map[String, TlaEx] =
+    def mapWithBuild(pairs: (String, BuilderT)*): Map[String, TlaEx] =
       pairs.map { case (a, b) => a -> b.build }.toMap
 
     assert(mapWithBuild("x" -> tla.int(1), "y" -> tla.int(1)) == decPath(1)._1)
@@ -225,9 +225,9 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
     assert(!mayChange2)
   }
 
-  private def mkAssign(name: String, value: Int): TBuilderInstruction =
+  private def mkAssign(name: String, value: Int): BuilderT =
     tla.assign(tla.prime(tla.name(name, IntT1)), tla.int(value))
 
-  private def mkAssignInt(name: String, rhs: TBuilderInstruction) =
+  private def mkAssignInt(name: String, rhs: BuilderT) =
     tla.assign(tla.prime(tla.name(name, IntT1)), rhs)
 }
diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala
index ad8a5209c2..23cbe6f36b 100644
--- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala
+++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala
@@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.pp
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper._
 import at.forsyte.apalache.tla.lir.values.{TlaBool, TlaInt, TlaStr}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderT, BuilderUT}
 
 /**
  * <p>A base class for constant simplification that is shared by more specialized simplifiers.</p>
@@ -239,4 +239,9 @@ abstract class ConstSimplifierBase {
     case ex =>
       ex
   }
+
+  def applySimplifyShallowToBuilderEx(ex: BuilderUT): BuilderUT =
+    simplifyShallow(ex) // when using TlaEx
+  def applySimplifyShallowToBuilderEx(ex: BuilderT): BuilderT =
+    ex.map(simplifyShallow) // when using TBuilderInstruction
 }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ArenaCell.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ArenaCell.scala
index 44f917e358..6e9e9a9d47 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ArenaCell.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ArenaCell.scala
@@ -2,9 +2,9 @@ package at.forsyte.apalache.tla.bmcmt
 
 import at.forsyte.apalache.tla.bmcmt.PureArena.namePrefix
 import at.forsyte.apalache.tla.lir.{NameEx, TlaEx}
-import at.forsyte.apalache.tla.typecomp
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 import at.forsyte.apalache.tla.bmcmt.types.CellT
+import at.forsyte.apalache.tla.typecomp._
 
 object ArenaCell {
   def isValidName(name: String): Boolean = {
@@ -44,7 +44,7 @@ class ArenaCell(val id: Int, val cellType: CellT, val isUnconstrained: Boolean =
    * @return
    *   a builder instruction that can be used with the typed builder
    */
-  def toBuilder: typecomp.TBuilderInstruction = tla.name(toString, cellType.toTlaType1)
+  def toBuilder: BuilderT = tla.name(toString, cellType.toTlaType1)
 
   def mkTlaEq(rhs: ArenaCell): TlaEx = tla.eql(this.toBuilder, rhs.toBuilder)
 
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ElemPtr.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ElemPtr.scala
index c35692625e..6e97dce712 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ElemPtr.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ElemPtr.scala
@@ -1,7 +1,6 @@
 package at.forsyte.apalache.tla.bmcmt
 
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * An abstract membership pointer.
@@ -18,7 +17,7 @@ sealed trait ElemPtr {
   /**
    * Translate the membership test into an expression that can be understood by Z3SolverContext.
    */
-  def toSmt: TBuilderInstruction
+  def toSmt: BuilderT
 
   /**
    * After certain set operations, every pointer must become a SmtExprElemPtr, because the operation invalidates the
@@ -31,7 +30,7 @@ sealed trait ElemPtr {
    * filter). `ptr.restrict(x)` returns `ptr2`, such that `ptr2.toSmt` is logically equivalent (but not necessarily
    * syntactically equal) to `tla.and(ptr.toSmt, x)`, while `ptr.elem = ptr2.elem`.
    */
-  def restrict(cond: TBuilderInstruction): SmtExprElemPtr
+  def restrict(cond: BuilderT): SmtExprElemPtr
 }
 
 /**
@@ -42,9 +41,9 @@ sealed trait ElemPtr {
  *   the element this pointer is pointing to.
  */
 case class FixedElemPtr(elem: ArenaCell) extends ElemPtr {
-  override def toSmt: TBuilderInstruction = tla.bool(true)
+  override def toSmt: BuilderT = tla.bool(true)
 
-  override def restrict(cond: TBuilderInstruction): SmtExprElemPtr = SmtExprElemPtr(elem, cond)
+  override def restrict(cond: BuilderT): SmtExprElemPtr = SmtExprElemPtr(elem, cond)
 }
 
 /**
@@ -56,7 +55,7 @@ case class FixedElemPtr(elem: ArenaCell) extends ElemPtr {
  * @param smtEx
  *   the corresponding SMT expression.
  */
-case class SmtExprElemPtr(elem: ArenaCell, smtEx: TBuilderInstruction) extends ElemPtr {
-  override def toSmt: TBuilderInstruction = smtEx
-  def restrict(cond: TBuilderInstruction): SmtExprElemPtr = this.copy(smtEx = tla.and(smtEx, cond))
+case class SmtExprElemPtr(elem: ArenaCell, smtEx: BuilderT) extends ElemPtr {
+  override def toSmt: BuilderT = smtEx
+  def restrict(cond: BuilderT): SmtExprElemPtr = this.copy(smtEx = tla.and(smtEx, cond))
 }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ParamUtil.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ParamUtil.scala
new file mode 100644
index 0000000000..a3dadd3420
--- /dev/null
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ParamUtil.scala
@@ -0,0 +1,75 @@
+package at.forsyte.apalache.tla.typecomp
+
+import at.forsyte.apalache.tla.lir.{
+  BoolT1, ConstT1, FunT1, IntT1, OperParam, OperT1, RealT1, RecRowT1, RecT1, RowT1, SeqT1, SetT1, SparseTupT1, StrT1,
+  TlaType1, TupT1, VarT1, VariantT1,
+}
+
+object ParamUtil {
+
+  type TypedParam = (OperParam, TlaType1)
+
+  /**
+   * Evaluates whether a parameter type satisfies the type restrictions on operator parameters in TLA+.
+   *
+   * Parameters of TLA+ operators must:
+   *   - have a non-operator type, unless they are (syntactically) marked higher-order (HO)
+   *   - have a top-level operator type (OperT1) if they are marked HO
+   *   - not contain `OperT1` in the type's syntax-tree in either case, except possibly at the root (if HO). In
+   *     particular, a parameter to a HO operator with an `OperT1` type may not be HO itself.
+   */
+  def isAcceptableParamType(canContainOper: Boolean): TlaType1 => Boolean = {
+    case FunT1(arg, res)         => isAcceptableParamType(false)(arg) && isAcceptableParamType(false)(res)
+    case SetT1(elem)             => isAcceptableParamType(false)(elem)
+    case SeqT1(elem)             => isAcceptableParamType(false)(elem)
+    case TupT1(elems @ _*)       => elems.forall(isAcceptableParamType(false))
+    case SparseTupT1(fieldTypes) => fieldTypes.values.forall(isAcceptableParamType(false))
+    case RecT1(fieldTypes)       => fieldTypes.values.forall(isAcceptableParamType(false))
+    case OperT1(args, res) =>
+      if (canContainOper)
+        args.nonEmpty &&
+        args.forall(isAcceptableParamType(false)) &&
+        isAcceptableParamType(false)(res)
+      else false
+    case RowT1(fieldTypes, _) => fieldTypes.values.forall(isAcceptableParamType(false))
+    case RecRowT1(row)        => isAcceptableParamType(false)(row)
+    case VariantT1(row)       => isAcceptableParamType(false)(row)
+    case IntT1 | StrT1 | BoolT1 | RealT1 | VarT1(_) | ConstT1(_) => true
+  }
+
+  /**
+   * Throws if parameters don't satisfy [[isAcceptableParamType]]. Permits operator types iff the parameter arity is
+   * positive.
+   */
+  def validateParamType(tp: TypedParam): Unit = {
+    val (OperParam(name, arity), tt) = tp
+    if (!isAcceptableParamType(canContainOper = arity > 0)(tt))
+      throw new TBuilderTypeException(
+          s"Parameter $name type $tt and arity $arity are inconsistent. Parameters have operator types iff their arity is positive."
+      )
+  }
+
+  /**
+   * Determines the parameter arity, if the type is an operator type. We distinguish nullary operators from
+   * non-operators in this method.
+   */
+  def typeAsOperArity(tt: TlaType1): Option[Int] = tt match {
+    case OperT1(args, _) => Some(args.size)
+    case _               => None
+  }
+
+  /**
+   * Operator parameter with type information. Checks that parameters have permissible types.
+   */
+  def param(name: String, tt: TlaType1): TypedParam = {
+    val arityOpt = typeAsOperArity(tt)
+    // operator parameters may not be nullary operators
+    if (arityOpt.contains(0))
+      throw new TBuilderTypeException(s"Parameter $name may not have a nullary operator type $tt.")
+    val arity = arityOpt.getOrElse(0) // 0 here means not-an-operator
+    val ret = (OperParam(name, arity), tt)
+    validateParamType(ret)
+    ret
+  }
+
+}
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopeUnsafeBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopeUnsafeBuilder.scala
new file mode 100644
index 0000000000..81438d1217
--- /dev/null
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopeUnsafeBuilder.scala
@@ -0,0 +1,128 @@
+package at.forsyte.apalache.tla.typecomp
+
+import at.forsyte.apalache.tla.lir.TypedPredefs.TypeTagAsTlaType1
+import at.forsyte.apalache.tla.lir._
+import at.forsyte.apalache.tla.typecomp.unsafe.{
+  UnsafeActionBuilder, UnsafeApalacheBuilder, UnsafeApalacheInternalBuilder, UnsafeArithmeticBuilder, UnsafeBaseBuilder,
+  UnsafeBoolBuilder, UnsafeControlBuilder, UnsafeFiniteSetBuilder, UnsafeFunBuilder, UnsafeLiteralAndNameBuilder,
+  UnsafeSeqBuilder, UnsafeSetBuilder, UnsafeTemporalBuilder, UnsafeVariantBuilder,
+}
+
+/**
+ * Scope-unsafe Builder for TLA+ (Quint) IR expressions.
+ *
+ * The following guarantees hold for any IR tree successfully generated exclusively via ScopeUnsafeBuilder methods:
+ *   - Typed-ness: All subexpressions will have a `Typed(_)` tag
+ *   - Type correctness:
+ *     - All literal expressions will have the correct type, as determined by their value ( `1: Int`, `"a" : Str`, etc.)
+ *     - For each operator application expression `OperEx(oper, args:_*)(Typed(resultType))`, the following holds:
+ *       - `oper(args:_*)` corresponds to some TNT operator with a signature `(T1,...,Tn) => T`
+ *       - There exists some substitution `s`, such that: `s(T1) = typeof(args[1]), ..., s(Tn) = typeof(args[n])` and
+ *         `s(T) = resultType`. Example: For `e @ OperEx(TlaSetOper.union, 1..4, {5})` the subexpressions `1..4, {5}`
+ *         and `e` will all have types `Set(Int)`, since
+ *         [[at.forsyte.apalache.tla.lir.oper.TlaSetOper.union TlaSetOper.union]] corresponds to `\union`, which has the
+ *         signature `(Set(t), Set(t)) => Set(t)`, and the substitution required is `t -> Int`.
+ *
+ * If `strict` mode is enabled, the builder rejects inputs for ApalacheOper methods, which do not adhere to the method
+ * requirements ("... must be ..."), even if their types are correct. If `strict` mode is disabled, the builder should
+ * allow for the construction of any expression, which may be present in a freshly parsed specification (i.e. before
+ * preprocessing).
+ *
+ * @author
+ *   Jure Kukovec
+ * @param strict
+ *   If true, performs method requirement checks
+ */
+class ScopeUnsafeBuilder(val strict: Boolean = true)
+    extends UnsafeBaseBuilder with UnsafeBoolBuilder with UnsafeArithmeticBuilder with UnsafeSetBuilder
+    with UnsafeFiniteSetBuilder with UnsafeSeqBuilder with UnsafeActionBuilder with UnsafeFunBuilder
+    with UnsafeControlBuilder with UnsafeTemporalBuilder with UnsafeApalacheInternalBuilder with UnsafeApalacheBuilder
+    with UnsafeVariantBuilder with UnsafeLiteralAndNameBuilder {
+
+  // The following two methods are included in the unsafe builder for interface compatibility with the
+  // scope-safe builder. They are both no-ops
+  def unchecked(ex: TlaEx): TlaEx = ex
+  def uncheckedDecl(decl: TlaOperDecl): TlaOperDecl = decl
+
+  ////////////////////
+  // HYBRID METHODS //
+  ////////////////////
+
+  /** x' = y */
+  def primeEq(x: TlaEx, y: TlaEx): TlaEx = eql(prime(x), y)
+
+  import ParamUtil._
+
+  def param(name: String, tt: TlaType1): TypedParam = ParamUtil.param(name, tt)
+
+  /** opName(params[1],...,params[n]) == body */
+  def decl(opName: String, body: TlaEx, params: TypedParam*): TlaOperDecl = {
+    params.foreach(validateParamType)
+    TlaOperDecl(opName, params.map(_._1).toList, body)(
+        Typed(
+            OperT1(params.map { _._2 }, body.typeTag.asTlaType1())
+        )
+    )
+  }
+
+  /**
+   * Creates an expression of the form
+   *
+   * {{{
+   * LET uniqueName(p1,...,pn) == body IN uniqueName
+   * }}}
+   *
+   * Matching the representation of LAMBDAs produced by SANY.
+   *
+   * NOTE: It is left up to the caller to ensure `uniqueName` is unique.
+   *
+   * Failure to ensure uniqueness of names can lead to name collisions in case lambdas are nested.
+   */
+  def lambda(uniqueName: String, body: TlaEx, params: TypedParam*): TlaEx = {
+    params.foreach(validateParamType)
+    val paramTypes = params.map(_._2)
+    val operType = OperT1(paramTypes, body.typeTag.asTlaType1())
+    letIn(name(uniqueName, operType), decl(uniqueName, body, params: _*))
+  }
+
+  /** {{{LET decl(...) = ... IN body}}} */
+  def letIn(body: TlaEx, decl: TlaOperDecl): TlaEx =
+    LetInEx(body, decl)(body.typeTag)
+
+  /**
+   * {{{LET F_1(a_1^1,...,a_{n_1}^1) == X_1 F_2(a_1^2,...,b_{n_2}^2) == X_2 ... F_N(a_1^N,...,z_{n_N}^N) == X_N IN e}}}
+   * is equivalently translated to
+   * {{{
+   *   LET F_1(a_1^1,...,a_{n_1}^1) == X_1 IN
+   *   LET F_2(a_1^2,...,b_{n_2}^2) == X_2 IN
+   *   ...
+   *   LET F_N(a_1^N,...,z_{n_N}^N) == X_N IN
+   *   e
+   * }}}
+   */
+  def letIn(body: TlaEx, decls: TlaOperDecl*): TlaEx = {
+    require(decls.nonEmpty, "decls must be nonempty.")
+    decls.foldRight(body) { case (decl, partial) =>
+      letIn(partial, decl)
+    }
+  }
+
+  /**
+   * [f EXCEPT ![a1] = e1, ![a2] = e2 ... ![an] = en]
+   *
+   * Is equivalent to {{{[[f EXCEPT ![a1] = e1] EXCEPT ![a2] = e2] EXCEPT ... ![an] = en]}}}
+   */
+  def exceptMany(
+      f: TlaEx,
+      args: (TlaEx, TlaEx)*): TlaEx = {
+    require(args.nonEmpty, s"args must be nonempty.")
+    args.foldLeft(f) { case (fn, (ai, ei)) =>
+      except(fn, ai, ei)
+    }
+  }
+
+  /**
+   * A name expression referring to the TlaVarDecl
+   */
+  def varDeclAsNameEx(decl: TlaVarDecl): TlaEx = name(decl.name, decl.typeTag.asTlaType1())
+}
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopedBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopedBuilder.scala
index 0a407d5319..6bfa4845cf 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopedBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopedBuilder.scala
@@ -168,70 +168,9 @@ class ScopedBuilder(val strict: Boolean = true)
   /** x' = y */
   def primeEq(x: TBuilderInstruction, y: TBuilderInstruction): TBuilderInstruction = eql(prime(x), y)
 
-  type TypedParam = (OperParam, TlaType1)
+  import ParamUtil._
 
-  /**
-   * Evaluates whether a parameter type satisfies the type restrictions on operator parameters in TLA+.
-   *
-   * Parameters of TLA+ operators must:
-   *   - have a non-operator type, unless they are (syntactically) marked higher-order (HO)
-   *   - have a top-level operator type (OperT1) if they are marked HO
-   *   - not contain `OperT1` in the type's syntax-tree in either case, except possibly at the root (if HO). In
-   *     particular, a parameter to a HO operator with an `OperT1` type may not be HO itself.
-   */
-  private def isAcceptableParamType(canContainOper: Boolean): TlaType1 => Boolean = {
-    case FunT1(arg, res)         => isAcceptableParamType(false)(arg) && isAcceptableParamType(false)(res)
-    case SetT1(elem)             => isAcceptableParamType(false)(elem)
-    case SeqT1(elem)             => isAcceptableParamType(false)(elem)
-    case TupT1(elems @ _*)       => elems.forall(isAcceptableParamType(false))
-    case SparseTupT1(fieldTypes) => fieldTypes.values.forall(isAcceptableParamType(false))
-    case RecT1(fieldTypes)       => fieldTypes.values.forall(isAcceptableParamType(false))
-    case OperT1(args, res) =>
-      if (canContainOper)
-        args.nonEmpty &&
-        args.forall(isAcceptableParamType(false)) &&
-        isAcceptableParamType(false)(res)
-      else false
-    case RowT1(fieldTypes, _) => fieldTypes.values.forall(isAcceptableParamType(false))
-    case RecRowT1(row)        => isAcceptableParamType(false)(row)
-    case VariantT1(row)       => isAcceptableParamType(false)(row)
-    case IntT1 | StrT1 | BoolT1 | RealT1 | VarT1(_) | ConstT1(_) => true
-  }
-
-  /**
-   * Throws if parameters don't satisfy [[isAcceptableParamType]]. Permits operator types iff the parameter arity is
-   * positive.
-   */
-  private def validateParamType(tp: TypedParam): Unit = {
-    val (OperParam(name, arity), tt) = tp
-    if (!isAcceptableParamType(canContainOper = arity > 0)(tt))
-      throw new TBuilderTypeException(
-          s"Parameter $name type $tt and arity $arity are inconsistent. Parameters have operator types iff their arity is positive."
-      )
-  }
-
-  /**
-   * Determines the parameter arity, if the type is an operator type. We distinguish nullary operators from
-   * non-operators in this method.
-   */
-  private def typeAsOperArity(tt: TlaType1): Option[Int] = tt match {
-    case OperT1(args, _) => Some(args.size)
-    case _               => None
-  }
-
-  /**
-   * Operator parameter with type information. Checks that parameters have permissible types.
-   */
-  def param(name: String, tt: TlaType1): TypedParam = {
-    val arityOpt = typeAsOperArity(tt)
-    // operator parameters may not be nullary operators
-    if (arityOpt.contains(0))
-      throw new TBuilderTypeException(s"Parameter $name may not have a nullary operator type $tt.")
-    val arity = arityOpt.getOrElse(0) // 0 here means not-an-operator
-    val ret = (OperParam(name, arity), tt)
-    validateParamType(ret)
-    ret
-  }
+  def param(name: String, tt: TlaType1): TypedParam = ParamUtil.param(name, tt)
 
   /** opName(params[1],...,params[n]) == body */
   def decl(opName: String, body: TBuilderInstruction, params: TypedParam*): TBuilderOperDeclInstruction = {
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/package.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/package.scala
index 151101aa3a..ebe867a369 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/package.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/package.scala
@@ -263,6 +263,11 @@ package object typecomp {
     def build: T = builderState
   }
 
+  // Included to facilitate seamless swapping between the scope-safe and unsafe builders
+  implicit class NoOpBuild(ex: TlaEx) {
+    def build: TlaEx = ex
+  }
+
   /**
    * Apply the `build` method to a sequence.
    *
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ActionBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ActionBuilder.scala
index 7201859d98..d9738e4e6f 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ActionBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ActionBuilder.scala
@@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.BuilderUtil.binaryFromUnsafe
  *   Jure Kukovec
  */
 trait ActionBuilder {
-  private val unsafeBuilder = new UnsafeActionBuilder
+  private val unsafeBuilder = new UnsafeActionBuilder {}
 
   /** {{{e'}}} */
   def prime(e: TBuilderInstruction): TBuilderInstruction = e.map(unsafeBuilder.prime)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala
index 086eec7375..3397a0a982 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala
@@ -15,7 +15,9 @@ import scalaz._
  */
 trait ApalacheBuilder {
   val strict: Boolean
-  private val unsafeBuilder = new UnsafeApalacheBuilder(strict)
+  // UnsafeApalacheBuilder is a trait with a parameter `strict`, so we create a class here to instantiate it
+  private case class ApalacheBuilderU(strict: Boolean) extends UnsafeApalacheBuilder
+  private val unsafeBuilder = ApalacheBuilderU(strict)
 
   /**
    * {{{lhs := rhs}}}
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheInternalBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheInternalBuilder.scala
index c8f96a10b9..78e6997869 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheInternalBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheInternalBuilder.scala
@@ -15,7 +15,7 @@ import scalaz.Scalaz._
  *   Jure Kukovec
  */
 trait ApalacheInternalBuilder {
-  private val unsafeBuilder = new UnsafeApalacheInternalBuilder
+  private val unsafeBuilder = new UnsafeApalacheInternalBuilder {}
 
   /**
    * {{{__NotSupportedByModelChecker(msg): t}}}
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ArithmeticBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ArithmeticBuilder.scala
index 8b4d52a135..a10fcf9621 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ArithmeticBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ArithmeticBuilder.scala
@@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.BuilderUtil.binaryFromUnsafe
  *   Jure Kukovec
  */
 trait ArithmeticBuilder {
-  private val unsafeBuilder = new UnsafeArithmeticBuilder
+  private val unsafeBuilder = new UnsafeArithmeticBuilder {}
 
   /** {{{x + y}}} */
   def plus(x: TBuilderInstruction, y: TBuilderInstruction): TBuilderInstruction =
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BaseBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BaseBuilder.scala
index 3297271cb7..2f9b55d0cf 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BaseBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BaseBuilder.scala
@@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeBaseBuilder
  *   Jure Kukovec
  */
 trait BaseBuilder {
-  private val unsafeBuilder = new UnsafeBaseBuilder
+  private val unsafeBuilder = new UnsafeBaseBuilder {}
 
   /** {{{lhs = rhs}}} */
   def eql(lhs: TBuilderInstruction, rhs: TBuilderInstruction): TBuilderInstruction =
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BoolBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BoolBuilder.scala
index e00c3c3b3a..7c55539a0d 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BoolBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BoolBuilder.scala
@@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.BuilderUtil._
  *   Jure Kukovec
  */
 trait BoolBuilder {
-  private val unsafeBuilder = new UnsafeBoolBuilder
+  private val unsafeBuilder = new UnsafeBoolBuilder {}
 
   /** {{{args[0] /\ ... /\ args[n]}}} */
   def and(args: TBuilderInstruction*): TBuilderInstruction = buildSeq(args).map(unsafeBuilder.and(_: _*))
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ControlBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ControlBuilder.scala
index 0e156acac8..0fdbd539d8 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ControlBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ControlBuilder.scala
@@ -12,7 +12,7 @@ import scalaz._
  *   Jure Kukovec
  */
 trait ControlBuilder {
-  private val unsafeBuilder = new UnsafeControlBuilder
+  private val unsafeBuilder = new UnsafeControlBuilder {}
 
   /** {{{IF p THEN A ELSE B}}} */
   def ite(p: TBuilderInstruction, A: TBuilderInstruction, B: TBuilderInstruction): TBuilderInstruction =
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FiniteSetBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FiniteSetBuilder.scala
index eb3e9ecd3d..a975845573 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FiniteSetBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FiniteSetBuilder.scala
@@ -10,7 +10,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeFiniteSetBuilder
  *   Jure Kukovec
  */
 trait FiniteSetBuilder {
-  private val unsafeBuilder = new UnsafeFiniteSetBuilder
+  private val unsafeBuilder = new UnsafeFiniteSetBuilder {}
 
   /** {{{IsFiniteSet(set)}}} */
   def isFiniteSet(set: TBuilderInstruction): TBuilderInstruction = set.map(unsafeBuilder.isFiniteSet)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala
index a4570d6c2f..846563253d 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala
@@ -15,7 +15,7 @@ import at.forsyte.apalache.tla.lir.VarT1
  *   Jure Kukovec
  */
 trait FunBuilder {
-  private val unsafeBuilder = new UnsafeFunBuilder
+  private val unsafeBuilder = new UnsafeFunBuilder {}
 
   /**
    * {{{[ args[0]._1 |-> args[0]._2, ..., args[n]._1 |-> args[n]._2 ]}}}
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala
index a4204a890a..5fd4178efe 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala
@@ -14,7 +14,7 @@ import scalaz._
  *   Jure Kukovec
  */
 trait LiteralAndNameBuilder {
-  private val unsafeBuilder = new UnsafeLiteralAndNameBuilder
+  private val unsafeBuilder = new UnsafeLiteralAndNameBuilder {}
 
   /** {{{i : Int}}} */
   def int(i: BigInt): TBuilderInstruction = unsafeBuilder.int(i).point[TBuilderInternalState]
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SeqBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SeqBuilder.scala
index c3ec3d5eb4..4375f677ec 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SeqBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SeqBuilder.scala
@@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeSeqBuilder
  *   Jure Kukovec
  */
 trait SeqBuilder {
-  private val unsafeBuilder = new UnsafeSeqBuilder
+  private val unsafeBuilder = new UnsafeSeqBuilder {}
 
   /** {{{Append(seq,elem)}}} */
   def append(seq: TBuilderInstruction, elem: TBuilderInstruction): TBuilderInstruction =
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SetBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SetBuilder.scala
index 293748f3ff..c1e9b6c3e1 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SetBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SetBuilder.scala
@@ -14,7 +14,7 @@ import scalaz.Scalaz._
  *   Jure Kukovec
  */
 trait SetBuilder {
-  private val unsafeBuilder = new UnsafeSetBuilder
+  private val unsafeBuilder = new UnsafeSetBuilder {}
 
   /**
    * {{{
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/TemporalBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/TemporalBuilder.scala
index 1d6de793ad..9be47382c7 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/TemporalBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/TemporalBuilder.scala
@@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeTemporalBuilder
  *   Jure Kukovec
  */
 trait TemporalBuilder {
-  private val unsafeBuilder = new UnsafeTemporalBuilder
+  private val unsafeBuilder = new UnsafeTemporalBuilder {}
 
   /** {{{[]P}}} */
   def box(P: TBuilderInstruction): TBuilderInstruction = P.map(unsafeBuilder.box)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/VariantBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/VariantBuilder.scala
index 80914ec431..7295ace16c 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/VariantBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/VariantBuilder.scala
@@ -12,7 +12,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeVariantBuilder
  *   Jure Kukovec
  */
 trait VariantBuilder {
-  private val unsafeBuilder = new UnsafeVariantBuilder
+  private val unsafeBuilder = new UnsafeVariantBuilder {}
 
   /**
    * {{{Variant(tagName, value): targetVariantType}}}
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeActionBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeActionBuilder.scala
index 00fc856656..b968f16b1c 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeActionBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeActionBuilder.scala
@@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaActionOper
  * @author
  *   Jure Kukovec
  */
-class UnsafeActionBuilder extends ProtoBuilder {
+trait UnsafeActionBuilder extends ProtoBuilder {
 
   /** {{{e'}}} */
   def prime(e: TlaEx): TlaEx = buildBySignatureLookup(TlaActionOper.prime, e)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala
index 42c63bce5a..0808c85ea3 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala
@@ -10,11 +10,9 @@ import at.forsyte.apalache.tla.lir.values.TlaInt
  * @author
  *   Jure Kukovec
  */
-class UnsafeApalacheBuilder(private val strict: Boolean = true) extends ProtoBuilder {
-
-  // We borrow the LiteralBuilder to make TLA integers from Scala ints
-  private val intBuilder = new UnsafeLiteralAndNameBuilder
-  private def mkTlaInt: BigInt => TlaEx = intBuilder.int
+trait UnsafeApalacheBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder {
+  val strict: Boolean
+  // We extend LiteralBuilder to make TLA integers from Scala ints
 
   /**
    * {{{lhs := rhs}}}
@@ -40,7 +38,7 @@ class UnsafeApalacheBuilder(private val strict: Boolean = true) extends ProtoBui
    */
   def gen(n: BigInt, t: TlaType1): TlaEx = {
     if (strict) require(n > 0, s"Expected n to be positive, found $n.")
-    OperEx(ApalacheOper.gen, mkTlaInt(n))(Typed(t))
+    OperEx(ApalacheOper.gen, int(n))(Typed(t))
   }
 
   /**
@@ -53,7 +51,7 @@ class UnsafeApalacheBuilder(private val strict: Boolean = true) extends ProtoBui
   def repeat(F: TlaEx, n: BigInt, x: TlaEx): TlaEx = {
     if (strict) require(n > 0, s"Expected n to be positive, found $n.")
     if (strict) require(isNaryPassByName(n = 2)(F), s"Expected F to be a binary operator passed by name, found $F.")
-    buildBySignatureLookup(ApalacheOper.repeat, F, mkTlaInt(n), x)
+    buildBySignatureLookup(ApalacheOper.repeat, F, int(n), x)
   }
 
   /**
@@ -116,7 +114,7 @@ class UnsafeApalacheBuilder(private val strict: Boolean = true) extends ProtoBui
       require(n >= 0, s"Expected n to be nonnegative, found $n.")
       require(isNaryPassByName(n = 1)(F), s"Expected F to be a unary operator passed by name, found $F.")
     }
-    buildBySignatureLookup(ApalacheOper.mkSeq, mkTlaInt(n), F)
+    buildBySignatureLookup(ApalacheOper.mkSeq, int(n), F)
   }
 
   /**
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheInternalBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheInternalBuilder.scala
index 68fdcf22d7..6b12d9000c 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheInternalBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheInternalBuilder.scala
@@ -9,11 +9,8 @@ import at.forsyte.apalache.tla.lir.oper.{ApalacheInternalOper, TlaOper}
  * @author
  *   Jure Kukovec
  */
-class UnsafeApalacheInternalBuilder extends ProtoBuilder {
-
-  // We borrow the LiteralBuilder to make TLA strings from Scala strings
-  private val strBuilder = new UnsafeLiteralAndNameBuilder
-  private def mkTlaStr: String => TlaEx = strBuilder.str
+trait UnsafeApalacheInternalBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder {
+  // We extend LiteralBuilder to make TLA strings from Scala strings
 
   /**
    * {{{__NotSupportedByModelChecker(msg): t}}}
@@ -22,7 +19,7 @@ class UnsafeApalacheInternalBuilder extends ProtoBuilder {
    * argument.
    */
   def notSupportedByModelChecker(msg: String, tt: TlaType1): TlaEx =
-    OperEx(ApalacheInternalOper.notSupportedByModelChecker, mkTlaStr(msg))(Typed(tt))
+    OperEx(ApalacheInternalOper.notSupportedByModelChecker, str(msg))(Typed(tt))
 
   /**
    * distinct
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeArithmeticBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeArithmeticBuilder.scala
index 7a6e1dcdba..cd4fc08636 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeArithmeticBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeArithmeticBuilder.scala
@@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaArithOper
  * @author
  *   Jure Kukovec
  */
-class UnsafeArithmeticBuilder extends ProtoBuilder {
+trait UnsafeArithmeticBuilder extends ProtoBuilder {
 
   /** {{{x + y}}} */
   def plus(x: TlaEx, y: TlaEx): TlaEx = buildBySignatureLookup(TlaArithOper.plus, x, y)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala
index 24ed493673..8da8399d03 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala
@@ -11,11 +11,8 @@ import at.forsyte.apalache.tla.types.{Substitution, TypeUnifier, TypeVarPool}
  * @author
  *   Jure Kukovec
  */
-class UnsafeBaseBuilder extends ProtoBuilder {
-
-  // We borrow the LiteralBuilder to make TLA strings from Scala strings
-  private val strBuilder = new UnsafeLiteralAndNameBuilder
-  private def mkTlaStr: String => TlaEx = strBuilder.str
+trait UnsafeBaseBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder {
+  // We extend the LiteralBuilder to make TLA strings from Scala strings
 
   /** {{{lhs = rhs}}} */
   def eql(lhs: TlaEx, rhs: TlaEx): TlaEx = buildBySignatureLookup(TlaOper.eq, lhs, rhs)
@@ -84,7 +81,7 @@ class UnsafeBaseBuilder extends ProtoBuilder {
    */
   def label(ex: TlaEx, args: String*): TlaEx = {
     require(args.nonEmpty, s"args must be nonempty.")
-    val argsAsStringExs = args.map { mkTlaStr }
+    val argsAsStringExs = args.map { str }
     buildBySignatureLookup(TlaOper.label, ex +: argsAsStringExs: _*)
   }
 }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBoolBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBoolBuilder.scala
index 48dfcb446d..5ff07224d4 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBoolBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBoolBuilder.scala
@@ -10,7 +10,7 @@ import at.forsyte.apalache.tla.typecomp.BuilderUtil
  * @author
  *   Jure Kukovec
  */
-class UnsafeBoolBuilder extends ProtoBuilder {
+trait UnsafeBoolBuilder extends ProtoBuilder {
 
   /** {{{args[0] /\ ... /\ args[n]}}} */
   def and(args: TlaEx*): TlaEx = buildBySignatureLookup(TlaBoolOper.and, args: _*)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeControlBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeControlBuilder.scala
index 6b016cced2..5d55941202 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeControlBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeControlBuilder.scala
@@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaControlOper
  * @author
  *   Jure Kukovec
  */
-class UnsafeControlBuilder extends ProtoBuilder {
+trait UnsafeControlBuilder extends ProtoBuilder {
 
   /** {{{IF p THEN A ELSE B}}} */
   def ite(p: TlaEx, A: TlaEx, B: TlaEx): TlaEx = buildBySignatureLookup(TlaControlOper.ifThenElse, p, A, B)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFiniteSetBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFiniteSetBuilder.scala
index 2e26ca8a59..6d7e258d18 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFiniteSetBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFiniteSetBuilder.scala
@@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaFiniteSetOper
  * @author
  *   Jure Kukovec
  */
-class UnsafeFiniteSetBuilder extends ProtoBuilder {
+trait UnsafeFiniteSetBuilder extends ProtoBuilder {
 
   /** {{{IsFiniteSet(set)}}} */
   def isFiniteSet(set: TlaEx): TlaEx = buildBySignatureLookup(TlaFiniteSetOper.isFiniteSet, set)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFunBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFunBuilder.scala
index f2b4bfa763..e596000136 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFunBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFunBuilder.scala
@@ -16,11 +16,8 @@ import scala.collection.immutable.SortedMap
  * @author
  *   Jure Kukovec
  */
-class UnsafeFunBuilder extends ProtoBuilder {
-
-  // We borrow the LiteralBuilder to make TLA strings from Scala strings
-  private val strBuilder = new UnsafeLiteralAndNameBuilder
-  private def mkTlaStr: String => TlaEx = strBuilder.str
+trait UnsafeFunBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder {
+  // We extend the LiteralBuilder to make TLA strings from Scala strings
 
   private def formRecordFieldTypes(args: Seq[TlaEx]): SortedMap[String, TlaType1] = {
     require(TlaFunOper.rec.arity.cond(args.size), s"Expected record args to have even arity, found $args.")
@@ -57,7 +54,7 @@ class UnsafeFunBuilder extends ProtoBuilder {
   def rowRec(rowVar: Option[VarT1], args: (String, TlaEx)*): TlaEx = {
     // _recMixed does all the require checks
     val flatArgs = args.flatMap { case (k, v) =>
-      Seq(mkTlaStr(k), v)
+      Seq(str(k), v)
     }
     rowRecMixed(rowVar, flatArgs: _*)
   }
@@ -82,7 +79,7 @@ class UnsafeFunBuilder extends ProtoBuilder {
   def rec(args: (String, TlaEx)*): TlaEx = {
     // _recMixed does all the require checks
     val flatArgs = args.flatMap { case (k, v) =>
-      Seq(mkTlaStr(k), v)
+      Seq(str(k), v)
     }
     recMixed(flatArgs: _*)
   }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeLiteralAndNameBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeLiteralAndNameBuilder.scala
index 058d0dff38..cef4cedcad 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeLiteralAndNameBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeLiteralAndNameBuilder.scala
@@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.types.ModelValueHandler
  * @author
  *   Jure Kukovec
  */
-class UnsafeLiteralAndNameBuilder {
+trait UnsafeLiteralAndNameBuilder {
 
   /** {{{i : Int}}} */
   def int(i: BigInt): TlaEx = ValEx(TlaInt(i))(Typed(IntT1))
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSeqBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSeqBuilder.scala
index 8dee27c310..55ccf2c1b0 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSeqBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSeqBuilder.scala
@@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaSeqOper
  * @author
  *   Jure Kukovec
  */
-class UnsafeSeqBuilder extends ProtoBuilder {
+trait UnsafeSeqBuilder extends ProtoBuilder {
 
   /** {{{Append(seq,elem)}}} */
   def append(seq: TlaEx, elem: TlaEx): TlaEx = buildBySignatureLookup(TlaSeqOper.append, seq, elem)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSetBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSetBuilder.scala
index 8c852397f1..f422985fdc 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSetBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSetBuilder.scala
@@ -14,11 +14,8 @@ import scala.collection.immutable.SortedMap
  * @author
  *   Jure Kukovec
  */
-class UnsafeSetBuilder extends ProtoBuilder {
-
-  // We borrow the LiteralBuilder to make TLA strings from Scala strings
-  private val strBuilder = new UnsafeLiteralAndNameBuilder
-  private def mkTlaStr: String => TlaEx = strBuilder.str
+trait UnsafeSetBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder {
+  // We extend the LiteralBuilder to make TLA strings from Scala strings
 
   /**
    * {{{
@@ -109,7 +106,7 @@ class UnsafeSetBuilder extends ProtoBuilder {
   def recSet(kvs: (String, TlaEx)*): TlaEx = {
     // _recSetMixed does all the require checks
     val args = kvs.flatMap { case (k, v) =>
-      Seq(mkTlaStr(k), v)
+      Seq(str(k), v)
     }
     recSetMixed(args: _*)
   }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeTemporalBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeTemporalBuilder.scala
index 38e1139f26..fb5aa72f73 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeTemporalBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeTemporalBuilder.scala
@@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.{NameEx, TlaEx}
  * @author
  *   Jure Kukovec
  */
-class UnsafeTemporalBuilder extends ProtoBuilder {
+trait UnsafeTemporalBuilder extends ProtoBuilder {
 
   /** {{{[]P}}} */
   def box(P: TlaEx): TlaEx = buildBySignatureLookup(TlaTempOper.box, P)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeVariantBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeVariantBuilder.scala
index 2d8d2a3a5e..a344cd8cc6 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeVariantBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeVariantBuilder.scala
@@ -12,11 +12,8 @@ import at.forsyte.apalache.tla.typecomp.{BuilderUtil, PartialSignature}
  * @author
  *   Jure Kukovec
  */
-class UnsafeVariantBuilder extends ProtoBuilder {
-
-  // We borrow the LiteralBuilder to make TLA strings from name tags (Scala strings)
-  private val strBuilder = new UnsafeLiteralAndNameBuilder
-  private def mkTlaStr: String => TlaEx = strBuilder.str
+trait UnsafeVariantBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder {
+  // We extend the LiteralBuilder to make TLA strings from name tags (Scala strings)
 
   /**
    * {{{Variant(tagName, value): targetVariantType}}}
@@ -35,7 +32,7 @@ class UnsafeVariantBuilder extends ProtoBuilder {
     }
     val sig = completePartial(VariantOper.variant.name, partialSig)
 
-    BuilderUtil.composeAndValidateTypes(VariantOper.variant, sig, mkTlaStr(tagName), value)
+    BuilderUtil.composeAndValidateTypes(VariantOper.variant, sig, str(tagName), value)
   }
 
   /** {{{VariantFilter(tagName, set)}}} */
@@ -46,7 +43,7 @@ class UnsafeVariantBuilder extends ProtoBuilder {
     }
     val sig = completePartial(VariantOper.variantFilter.name, partialSig)
 
-    BuilderUtil.composeAndValidateTypes(VariantOper.variantFilter, sig, mkTlaStr(tagName), set)
+    BuilderUtil.composeAndValidateTypes(VariantOper.variantFilter, sig, str(tagName), set)
   }
 
   /** {{{VariantTag(variant)}}} */
@@ -59,7 +56,7 @@ class UnsafeVariantBuilder extends ProtoBuilder {
       case Seq(StrT1, VariantT1(RowT1(fields, _)), a) if fields.get(tagName).contains(a) => a
     }
     val sig = completePartial(VariantOper.variantGetOrElse.name, partialSig)
-    BuilderUtil.composeAndValidateTypes(VariantOper.variantGetOrElse, sig, mkTlaStr(tagName), variant, defaultValue)
+    BuilderUtil.composeAndValidateTypes(VariantOper.variantGetOrElse, sig, str(tagName), variant, defaultValue)
   }
 
   /** {{{VariantGetUnsafe(tagName, variant)}}} */
@@ -69,6 +66,6 @@ class UnsafeVariantBuilder extends ProtoBuilder {
       case Seq(StrT1, VariantT1(RowT1(fields, _))) if fields.contains(tagName) => fields(tagName)
     }
     val sig = completePartial(VariantOper.variantGetUnsafe.name, partialSig)
-    BuilderUtil.composeAndValidateTypes(VariantOper.variantGetUnsafe, sig, mkTlaStr(tagName), variant)
+    BuilderUtil.composeAndValidateTypes(VariantOper.variantGetUnsafe, sig, str(tagName), variant)
   }
 }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala
index bbd898b721..d39d3a411e 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala
@@ -1,5 +1,7 @@
 package at.forsyte.apalache.tla
 
+import at.forsyte.apalache.tla.lir.TlaEx
+
 /**
  * Defines a premade instance of [[at.forsyte.apalache.tla.typecomp.ScopedBuilder ScopedBuilder]], named [[tla]].
  *
@@ -132,6 +134,9 @@ package object types {
 
   import at.forsyte.apalache.tla.typecomp._
 
+  type BuilderT = TBuilderInstruction
+  type BuilderUT = TlaEx
+
   /**
    * A short-hand to the instance of the typed builder, so one can easily construct expressions.
    *
@@ -150,4 +155,5 @@ package object types {
    *   [[at.forsyte.apalache.tla.typecomp.ScopedBuilder ScopedBuilder]] for implementation details.
    */
   val tla: ScopedBuilder = new ScopedBuilder(strict = true)
+  val tlaU: ScopeUnsafeBuilder = new ScopeUnsafeBuilder(strict = true)
 }
diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestApalacheBuilder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestApalacheBuilder.scala
index f8e4cf684a..c61d3035ea 100644
--- a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestApalacheBuilder.scala
+++ b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestApalacheBuilder.scala
@@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.typecomp
 
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.ApalacheOper
-import at.forsyte.apalache.tla.types.tla.TypedParam
+import at.forsyte.apalache.tla.typecomp.ParamUtil.TypedParam
 import org.junit.runner.RunWith
 import org.scalatestplus.junit.JUnitRunner
 import scalaz.unused
diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala
index 0b6400fd95..809da08b76 100644
--- a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala
+++ b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala
@@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.typecomp
 
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.{TlaActionOper, TlaBoolOper, TlaOper}
-import at.forsyte.apalache.tla.types.tla.TypedParam
+import at.forsyte.apalache.tla.typecomp.ParamUtil.TypedParam
 import org.junit.runner.RunWith
 import org.scalacheck.Prop.forAll
 import org.scalatestplus.junit.JUnitRunner