proposition: Lemma map_zip_fst_snd {A B} (m : M (A * B)) : map_zip (fst <$> m) (snd <$> m) = m.
proof: Proof. apply map_eq; intros k. rewrite map_lookup_zip_with, !lookup_fmap. by destruct (m !! k) as [[]|]. Qed.
imports: Coq(Permutation) stdpp(options)