case nil => {
    intros ix bound H deltaIx GETIX;
    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