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