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