proposition: Lemma map_Forall_union {A} (m1 m2 : M A) P : m1 ##ₘ m2 → map_Forall P (m1 ∪ m2) ↔ map_Forall P m1 ∧ map_Forall P m2.
proof: Proof. naive_solver eauto using map_Forall_union_1_1, map_Forall_union_1_2, map_Forall_union_2. Qed.
imports: Coq(Permutation) stdpp(options)