case succ deltaIx' => {
  simp [zipFlatIndexGo];
  simp [List.getF];
  rewrite [IND];
  simp [Nat.add_assoc, Nat.add_one, Nat.succ_add, Nat.add_succ];
  simp at GETIX;
  apply Nat.lt_of_succ_lt_succ;
  exact 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')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) (Nat.succ deltaIx')
      (_ : Nat.succ deltaIx' < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') (Nat.succ deltaIx') GETIX,
      { ix := ix + Nat.succ deltaIx', h_ix_inbound := (_ : ix + Nat.succ deltaIx' < bound) })
no goals