proposition: Lemma partial_alter_subseteq {A} f (m : M A) i : m !! i = None → m ⊆ partial_alter f i m.
proof: Proof. rewrite map_subseteq_spec. intros Hi j x Hj. rewrite lookup_partial_alter_ne; congruence. Qed.
imports: Coq(Permutation) stdpp(options)