proposition: Lemma alter_mono {A} f (m1 m2 : M A) i : m1 ⊆ m2 → alter f i m1 ⊆ alter f i m2.
proof: Proof. rewrite !map_subseteq_spec. intros ? j x. rewrite !lookup_alter_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)