Non-polymorphic decreases_to! panics verifier

[gancherj]

Below:

use vstd::*;
use vstd::prelude::*;

verus! {

    proof fn tst(s : Seq<nat>)
        requires s.len() > 0
        ensures #[trigger] (decreases_to!(s => s[0]))
        {
         admit();   
        }
}

produces output

thread '<unnamed>' panicked at rust_verify/src/verifier.rs:517:17:
internal error: ill-typed AIR code: error 'error 'in call to <, argument #2 has type "vstd!seq.Seq<nat.>." when it should have type "Int"' in expression '(< (%I (vstd!seq.Seq.index.? $ NAT (Poly%vstd!seq.Seq<nat.>. s!) (I 0))) s!)'' in expression '(and
 (<= 0 (%I (vstd!seq.Seq.index.? $ NAT (Poly%vstd!seq.Seq<nat.>. s!) (I 0))))
 (< (%I (vstd!seq.Seq.index.? $ NAT (Poly%vstd!seq.Seq<nat.>. s!) (I 0))) s!)
)'
note: [run with `RUST_BACKTRACE=1` environment variable to display a backtrace](https://play.verus-lang.org/?version=stable&mode=basic&edition=2021#)
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:339:17:
dropped, expected call to `into_inner` instead
stack backtrace:
   0:     0x7f72a06696f6 - std::backtrace_rs::backtrace::libunwind::trace::hbee8a7973eeb6c93
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/../../backtrace/src/backtrace/libunwind.rs:104:5
   1:     0x7f72a06696f6 - std::backtrace_rs::backtrace::trace_unsynchronized::hc8ac75eea3aa6899
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f72a06696f6 - std::sys_common::backtrace::_print_fmt::hc7f3e3b5298b1083
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/sys_common/backtrace.rs:68:5
   3:     0x7f72a06696f6 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::hbb235daedd7c6190
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7f72a06bbf40 - core::fmt::rt::Argument::fmt::h76c38a80d925a410
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/core/src/fmt/rt.rs:142:9
   5:     0x7f72a06bbf40 - core::fmt::write::h3ed6aeaa977c8e45
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/core/src/fmt/mod.rs:1120:17
   6:     0x7f72a065d53f - std::io::Write::write_fmt::h78b18af5775fedb5
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/io/mod.rs:1810:15
   7:     0x7f72a06694d4 - std::sys_common::backtrace::_print::h5d645a07e0fcfdbb
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7f72a06694d4 - std::sys_common::backtrace::print::h85035a511aafe7a8
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7f72a066c267 - std::panicking::default_hook::{{closure}}::hcce8cea212785a25
  10:     0x7f72a066bfc9 - std::panicking::default_hook::hf5fcb0f213fe709a
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/panicking.rs:292:9
  11:     0x7f72a066c828 - std::panicking::rust_panic_with_hook::h095fccf1dc9379ee
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/panicking.rs:779:13
  12:     0x560b395de26d - std::panicking::begin_panic::{{closure}}::h7d943025b9aab28a
  13:     0x560b395ddf76 - std::sys_common::backtrace::__rust_end_short_backtrace::hbe36db03c1754811
  14:     0x560b3947b2da - std::panicking::begin_panic::h7ede8bd9c91d2094
  15:     0x560b395abce6 - core::ptr::drop_in_place<core::cell::RefCell<core::option::Option<rust_verify::verifier::util::PanicOnDropVec<(alloc::sync::Arc<vir::messages::MessageX>,air::messages::MessageLevel)>>>>::h6c324136b91f7bf5
  16:     0x560b395c5246 - rust_verify::verifier::Verifier::verify_bucket::h8b22f4fbaa0c11cf
  17:     0x560b395a6280 - std::panicking::try::h67eec24a0b7b29f4
  18:     0x560b395ddfeb - std::sys_common::backtrace::__rust_begin_short_backtrace::hb4d3ba94bf1653ff
  19:     0x560b395a8c41 - core::ops::function::FnOnce::call_once{{vtable.shim}}::h4418cb5ec9e63232
  20:     0x7f72a06768e5 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h12de4fc57affb195
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/alloc/src/boxed.rs:2015:9
  21:     0x7f72a06768e5 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h3c619f45059d5cf1
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/alloc/src/boxed.rs:2015:9
  22:     0x7f72a06768e5 - std::sys::unix::thread::Thread::new::thread_start::hbac657605e4b7389
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/sys/unix/thread.rs:108:17
  23:     0x7f729a784ac3 - <unknown>
  24:     0x7f729a815a04 - __clone
  25:                0x0 - <unknown>
thread '<unnamed>' panicked at library/core/src/panicking.rs:163:5:
panic in a destructor during cleanup
thread caused non-unwinding panic. aborting.
timeout: the monitored command dumped core
/playground/tools/entrypoint.sh: line 11:     7 Aborted                 timeout --signal=KILL ${timeout} "$@"

Link to playground

I should mention that the below modification is fine:

    proof fn tst<A>(s : Seq<A>)
        requires s.len() > 0
        ensures #[trigger] (decreases_to!(s => s[0]))
        {
         admit();   
        }