Function _verus_external_fn_specification_1__60__32__91_T_59__32_N_93__32__62__32__58__58__32_as__slice 

pub unsafe exec fn _verus_external_fn_specification_1__60__32__91_T_59__32_N_93__32__62__32__58__58__32_as__slice<T, const N: usize>(
    ar: &[T; N],
) -> out : &[T]

ensures

ar@ == out@,

Specification for [<[T; N]>::as_slice]