proposition: Lemma map_agree_weaken {A} (m1 m1' m2 m2' : M A) : map_agree m1' m2' → m1 ⊆ m1' → m2 ⊆ m2' → map_agree m1 m2.
proof: Proof. rewrite !map_subseteq_spec, !map_agree_spec. eauto. Qed.
imports: Coq(Permutation) stdpp(options)