intros 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) })
α : 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) })