ADT plugin contains cannot prove lack of value

[Aurel300]

import <adt/derives.vpr>

adt List[T] {
    Nil()
    Cons(value: T, tail: List[T])
} derives {
    contains
}

method client() {
    var x: List[Int] := Cons(42, Cons(33, Nil()))
    assert contains(42, x) // passes, as expected
    assert !contains(0, x) // fails
}

I think the axioms generated for contains are strong enough to prove which values are in the given ADT, but they do not say which values are not.