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