proposition: Lemma map_disjoint_union_list_r {A} (ms : list (M A)) (m : M A) : m ##ₘ ⋃ ms ↔ Forall (.##ₘ m) ms.
proof: Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_union_list_l. Qed.
imports: Coq(Permutation) stdpp(options)