cases i with | mk v vlt => 
cases v 
. simp [List.get]
. case succ v1 => cases v1 <;> simp [List.get]
α : Type u_1
x y : α
xs : List α
i : Fin (List.length xs + 2)
⊢ List.get (x :: y :: xs) i = List.get (y :: x :: xs) (shuffleIndex i)
no goals