no goals
α : Type u
β : Type u_1
γ : Type ?u.85724
δ : Type ?u.85727
ε : Type ?u.85730
a : α
b : β
l : List (α × β)
⊢ zip (unzip ((a, b) :: l)).fst (unzip ((a, b) :: l)).snd = (a, b) :: l
simp only [unzip_cons, zip_cons_cons, zip_unzip l]