rewrite [IND]
α : 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
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ getF (zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + length xs' = bound)) deltaIx'
      (_ : deltaIx' < length (zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + length xs' = bound))) =
    (getF xs' deltaIx' (_ : deltaIx' < length xs'),
      { ix := ix + Nat.succ deltaIx', h_ix_inbound := (_ : ix + Nat.succ deltaIx' < 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
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ (getF xs' deltaIx' ?GETIX, { ix := ix + 1 + deltaIx', h_ix_inbound := (_ : ix + 1 + deltaIx' < bound) }) =
    (getF xs' deltaIx' (_ : deltaIx' < length xs'),
      { ix := ix + Nat.succ deltaIx', h_ix_inbound := (_ : ix + Nat.succ deltaIx' < bound) })

case GETIX
α : 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
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ deltaIx' < length xs'