simp [zipFlatIndexGo]
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
ix bound : ℕ
H : ix + List.length (x :: xs') = bound
⊢ List.length (x :: xs') = List.length (zipFlatIndexGo (x :: xs') ix bound H)
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
ix bound : ℕ
H : ix + List.length (x :: xs') = bound
⊢ List.length xs' = List.length (zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + List.length xs' = bound))