trait A {
  var u: BigInt
  var v: BigInt
  def f(x: BigInt): BigInt
}

case class B(a: A)

object Example {
  def invariant(b: B) = {
    b.a.f(b.a.u) == b.a.v
  }
}