We currently don't handle the head/tail pattern fully. Add an appropriate error message and add to the limitations section of the docs, then we can remove the "MLP - Must Have" and change it from a bug to a feature.

With #1066, this no longer crashes, and instead we codegen assert/assume false that will cause verification to fail if the array subslice pattern is reachable. Removing the "MLP - Must Have" label.

fn array() -> [(String, String); 3] {
    Default::default()
}

#[kani::proof]
fn move_out_by_const_subslice_and_index_field() {
    let a = array();
    let [_, _y @ ..] = a;
    let [(ref _x, _), _, _] = a;
}

#[kani::proof]
fn move_out_by_const_subslice_and_end_index_field() {
    let a = array();
    let [_y @ .., _] = a;
    let [.., (ref _x, _)] = a;
}

// Slice + Slice
#[kani::proof]
fn move_out_by_subslice_and_subslice() {
    let a = array();
    let [x @ .., _, _] = a;
    let [_, ref _y @ ..] = a;
}

with mir-opt-level=3: Failed Checks: Sub-array binding is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/707