Type inference for int constants worse in pulse functions

The following snippet highlights the issue:
```fstar
open Pulse.Lib.Pervasives

#lang-pulse

val rnat (p: FStar.Seq.seq nat): slprop

let works = rnat seq![0]

fn foo_works ()
requires emp
ensures rnat seq![0 <: nat]

fn foo ()
requires emp
ensures rnat seq![0]
```

I get a `Assertion failed` error (also not a very intuitive error, e.g. `seq int is not a subtype of seq nat` would be better). The error is due to `seq![0]` typing as `FStar.Seq.seq int` in the Pulse postcondition (this also happens in the body of a pulse function).

This happens even when using `seq![x; x; 0]` with `x: nat` or when writing out the `seq!` as `cons`s. The surprising thing to me is that it works in the F* code but not pulse.

Reproduce the provided Pulse snippet and compare the inferred type of seq![0] in the working F* expression with its type in the Pulse postcondition and function body. Trace the Pulse type-inference path from that example; done means compatible nat inference works in both contexts and the mismatch, if still reported, uses a clear diagnostic.

Written by the indexing model from the issue text.