simp
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (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) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
GETIX : Nat.zero < length (x :: xs')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) Nat.zero (_ : Nat.zero < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') Nat.zero GETIX, { ix := ix + Nat.zero, h_ix_inbound := (_ : ix + Nat.zero < bound) })
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (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) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
GETIX : Nat.zero < length (x :: xs')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) 0 (_ : Nat.zero < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') 0 GETIX, { ix := ix, h_ix_inbound := (_ : ix < bound) })