case cons x xs' IND => {
 intros ix bound H deltaIx GETIX; cases deltaIx;
 case zero => {
    simp;
    simp [zipFlatIndexGo, List.getF]
 }
 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 : deltaIx < length (x :: xs')),
    getF (zipFlatIndexGo (x :: xs') ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo (x :: xs') ix bound H)) =
      (getF (x :: xs') deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
no goals