proposition: Lemma map_zip_with_empty_r {A B C} (f : A → B → C) m1 : map_zip_with f m1 ∅ =@{M C} ∅.
proof: Proof. unfold map_zip_with. apply map_eq; intros i. rewrite lookup_merge, !lookup_empty. destruct (m1 !! i); done. Qed.
imports: Coq(Permutation) stdpp(options)