module M {
  trait Object {
   ghost function typeId() : (id: string)
  }

  type A extends Object {
   ghost function typeId() : (id: string)  { "A" }
  }

  type B extends Object {
   ghost function typeId() : (id: string)  { "B" }
  }
  type C extends Object {
   ghost function typeId() : (id: string)  { "C" }
  }

  lemma test(x: Object)
    ensures multiset{x is A, x is B, x is C}[true] == 1
  {
    var _ := x.typeId();
    if (x is A) {
      assert x !is B.  // <----- Put the cursor here
    }
  }
}