proposition: Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) : ⋃ ms ##ₘ m ↔ Forall (.##ₘ m) ms.
proof: Proof. split. - induction ms; simpl; rewrite ?map_disjoint_union_l; intuition. - induction 1; simpl; [apply map_disjoint_empty_l |]. by rewrite map_disjoint_union_l. Qed.
imports: Coq(Permutation) stdpp(options)