proposition: Lemma map_fmap_zip_with_r {A B C} (f : A → B → C) (g : C → B) (m1 : M A) (m2 : M B) : (∀ x y, g (f x y) = y) → (∀ k, is_Some (m2 !! k) → is_Some (m1 !! k)) → g <$> map_zip_with f m1 m2 = m2.
proof: Proof. intros ? Hm. apply map_eq; intros k. rewrite lookup_fmap, map_lookup_zip_with. destruct (m2 !! _) as [x|] eqn:?; simpl; [|by destruct (m1 !! _)]. destruct (Hm k) as [y ->]; [by eauto|]. by f_equal/=. Qed.
imports: Coq(Permutation) stdpp(options)