     }
   }
 
+  /// The goals to satisfy in this term.
   var goals: [[Term]] {
     switch dnf {
     case .conjunction(let lhs, let rhs):

    }
  }

  func renaming(_ variables: Set<String>) -> Term {
    switch self {
    case .var(let x) where variables.contains(x):

    }
  }

  /// The free variables occurring in this term.
  var variables: Set<String> {
    switch self {
    case .var(let x):
