Datatype value inequality requires redundant assertions

[dirtybytes]

Dafny version

4.11.0.0

Code to produce this issue

datatype List<T> = Nil | Cons(head: T, tail: List<T>)

method Test(xs: List)
{
  if xs != Nil {
    // assert Cons(xs.head, xs.tail) > xs.tail;
    assert Cons(xs.head, xs.tail) != xs.tail; // "assertion might not hold"
                                              // if the line above is commented
  }
}

Command to run and resulting output

VSCode

What happened?

I expected the assertion Cons(xs.head, xs.tail) != xs.tail to pass automatically. Instead I had to state explicitly that one side contains the other. It seems to me that Dafny should be able to figure that out on its own.

What type of operating system are you experiencing the problem on?

Windows