proposition: Lemma delete_partial_alter {A} (m : M A) i f : m !! i = None → delete i (partial_alter f i m) = m.
proof: Proof. intros. unfold delete, map_delete. rewrite <-partial_alter_compose. unfold compose. by apply partial_alter_self_alt. Qed.
imports: Coq(Permutation) stdpp(options)