cases v with
| zero => simp [shuffleIndex] 
| succ v1 => cases v1 <;> simp [shuffleIndex]
case mk
n v : Nat
lt : v < n + 2
⊢ shuffleIndex (shuffleIndex { val := v, isLt := lt }) = { val := v, isLt := lt }
no goals