cases v1 <;> simp [List.get]
α : Type u_1
x y : α
xs : List α
v1 : Nat
vlt : Nat.succ v1 < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.succ v1, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.succ v1, isLt := vlt })
no goals