induction xs
α : Type u_1
xs : List α
⊢ ∀ (ix bound : ℕ) (H : ix + length xs = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs),
    getF (zipFlatIndexGo xs ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs ix bound H)) =
      (getF xs deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
case nil
α : 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) })

case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (ix bound : ℕ) (H : ix + length tail✝ = bound) (deltaIx : ℕ) (GETIX : deltaIx < length tail✝),
    getF (zipFlatIndexGo tail✝ ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo tail✝ ix bound H)) =
      (getF tail✝ deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
⊢ ∀ (ix bound : ℕ) (H : ix + length (head✝ :: tail✝) = bound) (deltaIx : ℕ) (GETIX : deltaIx < length (head✝ :: tail✝)),
    getF (zipFlatIndexGo (head✝ :: tail✝) ix bound H) deltaIx
        (_ : deltaIx < length (zipFlatIndexGo (head✝ :: tail✝) ix bound H)) =
      (getF (head✝ :: tail✝) deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })