Problem with coercion int to integer in pattern matching

[n-osborne]

Here, gospel check succeed because 0 is coerced to an integer.

type 'a t
(*@ mutable model contents : 'a sequence *)

val create : unit -> 'a t
(*@ q = create ()
    ensures q.contents = Sequence.empty *)

val pop_opt : 'a t -> 'a option
(*@ o = pop_opt q
    modifies q.contents
    ensures q.contents = match Sequence.length (old q.contents) with
                          | 0 -> Sequence.empty
                          | _ -> Sequence.tl (old q.contents) *)

But, in the generated code, 0 is an int:

    let next_state cmd__002_ state__003_ =
      match cmd__002_ with
      | Pop_opt ->
          {
            contents =
              ((try
                  match Ortac_runtime.Gospelstdlib.Sequence.length
                          state__003_.contents
                  with
                  | 0 -> Ortac_runtime.Gospelstdlib.Sequence.empty
                  | _ ->
                      Ortac_runtime.Gospelstdlib.Sequence.tl
                        state__003_.contents
                with
                | e -> ...
          }