proposition: Lemma snd_map_zip {A B} (m1 : M A) (m2 : M B) : (∀ k : K, is_Some (m2 !! k) → is_Some (m1 !! k)) → snd <$> map_zip m1 m2 = m2.
proof: Proof. intros ?. by apply map_fmap_zip_with_r. Qed.
imports: Coq(Permutation) stdpp(options)