Imprecise logical context in the match branch (cannot prove that the scrutinee is not a data constructor that is matched before this branch)

[aseemr]

noeq
type t =
  | A : t
  | B : t

fn test (x:t)
  requires emp
  ensures emp
{
  match x {
    A -> {
      ()
    }
    _ -> {
      assert (pure (~ (A? x)))
    }
  }
}

[nikswamy]

We should improve this and when we do also correspondingly update this piece of documentation.

https://github.com/FStarLang/PoP-in-FStar/blob/pulse/book/pulse/pulse_conditionals.rst?plain=1#L170-L183