no goals
α : Type u
β : Type u_1
γ : Type ?u.84326
δ : Type ?u.84329
ε : Type ?u.84332
a : α
b : β
l : List (α × β)
⊢ unzip ((a, b) :: l) = (map Prod.fst ((a, b) :: l), map Prod.snd ((a, b) :: l))
simp only [unzip_cons, map_cons, unzip_eq_map l]