induction xs generalizing ys with
| nil           => simp [min, length]
| cons x xs' ih =>
  cases ys with
  | nil        => rfl
  | cons y ys' => simp [zip, length, ih ys', min_add_add]
α β : Type
xs : List α
ys : List β
⊢ length (zip xs ys) = min (length xs) (length ys)
no goals