unfold zipFlatIndexGo
α : Type u_1
ix✝ bound✝ : ℕ
H✝ : ix✝ + List.length [] = bound✝
⊢ List.length [] = List.length (zipFlatIndexGo [] ix✝ bound✝ H✝)
α : Type u_1
ix✝ bound✝ : ℕ
H✝ : ix✝ + List.length [] = bound✝
⊢ List.length [] = List.length []