α : Type u
β : Type ?u.93715
γ : Type ?u.93718
δ : Type ?u.93721
ε : Type ?u.93724
l : List α
⊢ zip (unzip (reverse (revzip l))).fst (unzip (reverse (revzip l))).snd = revzip (reverse l)
α : Type u
β : Type ?u.93715
γ : Type ?u.93718
δ : Type ?u.93721
ε : Type ?u.93724
l : List α
⊢ reverse (revzip l) = revzip (reverse l)
rw [← zip_unzip (revzip l).reverse]
no goals
α : Type u
β : Type ?u.93715
γ : Type ?u.93718
δ : Type ?u.93721
ε : Type ?u.93724
l : List α
⊢ zip (unzip (reverse (revzip l))).fst (unzip (reverse (revzip l))).snd = revzip (reverse l)
simp [unzip_eq_map, revzip, map_reverse, map_fst_zip, map_snd_zip]