diff --git a/langs/tla/defns.scala b/langs/tla/defns.scala
index 0372867..fb8dbd1 100644
--- a/langs/tla/defns.scala
+++ b/langs/tla/defns.scala
@@ -74,7 +74,9 @@ object defns:
   case object PROPOSITION extends ReservedWord
   case object ONLY extends ReservedWord
 
-  sealed trait Operator extends Token, HasSpelling
+  sealed trait Operator extends Token, HasSpelling:
+    def highPrecedence: Int
+    def lowPrecedence: Int
 
   object Operator:
     lazy val instances: IArray[Operator] =
@@ -100,7 +102,7 @@ object defns:
 
   sealed trait InfixOperator(
       val lowPrecedence: Int,
-      val highPredecence: Int,
+      val highPrecedence: Int,
       val isAssociative: Boolean = false,
   ) extends Operator
   object InfixOperator extends util.HasInstanceArray[InfixOperator]
@@ -209,7 +211,9 @@ object defns:
   case object `\\supset` extends InfixOperator(5, 5)
   case object `%%` extends InfixOperator(10, 11, true)
 
-  sealed trait PostfixOperator(val predecence: Int) extends Operator
+  sealed trait PostfixOperator(val precedence: Int) extends Operator:
+    def highPrecedence: Int = precedence
+    def lowPrecedence: Int = precedence
   object PostfixOperator extends util.HasInstanceArray[PostfixOperator]
 
   case object `^+` extends PostfixOperator(15)
diff --git a/langs/tla/package.scala b/langs/tla/package.scala
index be312f0..2bfee44 100644
--- a/langs/tla/package.scala
+++ b/langs/tla/package.scala
@@ -101,6 +101,7 @@ object lang extends WellformedDef:
           Expr.TupleLiteral,
           Expr.RecordLiteral,
           Expr.Project,
+          Expr.RecordSetLiteral,
           Expr.OpCall,
           Expr.FnCall,
           Expr.If,
@@ -180,7 +181,8 @@ object lang extends WellformedDef:
           ),
         )
 
-    object Case extends t(repeated(Case.Branch, minCount = 1)):
+    object Case extends t(fields(Case.Branches, Case.Other)):
+      object Branches extends t(repeated(Branch, minCount = 1))
       object Branch
           extends t(
             fields(
@@ -188,6 +190,8 @@ object lang extends WellformedDef:
               Expr,
             ),
           )
+      object Other extends t(choice(Expr, None))
+      object None extends t(Atom)
     end Case
 
     object Let
diff --git a/src/Node.scala b/src/Node.scala
index 953b660..015fb44 100644
--- a/src/Node.scala
+++ b/src/Node.scala
@@ -391,7 +391,7 @@ object Node:
 
       require(
         results.size == 1,
-        s"token(s) not found ${(tok +: toks).map(_.name).mkString(", ")}",
+        s"token(s) not found ${(tok +: toks).map(_.name).mkString(", ")}, in ${this.toShortString()}",
       )
       results.head
 
diff --git a/src/wf/Wellformed.scala b/src/wf/Wellformed.scala
index 7141ab5..dcf0201 100644
--- a/src/wf/Wellformed.scala
+++ b/src/wf/Wellformed.scala
@@ -555,6 +555,15 @@ object Wellformed:
               s"$token's shape is not appropriate for adding cases ($shape)",
             )
 
+      def deleteShape(): Unit =
+        token match
+          case Node.Top =>
+            require(topShapeOpt.nonEmpty)
+            topShapeOpt = None
+          case token: Token =>
+            require(assigns.contains(token))
+            assigns.remove(token)
+
       def importFrom(wf2: Wellformed): Unit =
         def fillFromShape(shape: Shape): Unit =
           shape match