no goals
ι : Type ?u.479474
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
as : List α
b : β
bs : List β
⊢ zipRight as bs = (zipRight' as bs).fst
induction as generalizing bs <;> cases bs <;> simp [*]