case cons x xs' IND => {
  intros ix bound H;
  simp [zipFlatIndexGo];
  apply IND;
}
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
⊢ ∀ (ix bound : ℕ) (H : ix + List.length (x :: xs') = bound),
    List.length (x :: xs') = List.length (zipFlatIndexGo (x :: xs') ix bound H)
no goals