simp [List.length, Nat.not_lt_zero] at GETIX
α : Type u_1
ix bound : ℕ
H : ix + length [] = bound
deltaIx : ℕ
GETIX : deltaIx < length []
⊢ getF (zipFlatIndexGo [] ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo [] ix bound H)) =
    (getF [] deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
no goals