no goals
α : Type u
β : Type u_1
γ : Type ?u.87473
δ : Type ?u.87476
ε : Type ?u.87479
l : List α
l' : List β
lp : List (α × β)
hl : map Prod.fst lp = l
hr : map Prod.snd lp = l'
⊢ lp = zip l l'
rw [← hl, ← hr, ← zip_unzip lp, ← unzip_left, ← unzip_right, zip_unzip, zip_unzip]