proposition: Lemma delete_subset {A} (m : M A) i : is_Some (m !! i) → delete i m ⊂ m.
proof: Proof. intros [x ?]; apply map_subset_alt; split; [apply delete_subseteq|]. exists i. rewrite lookup_delete; eauto. Qed.
imports: Coq(Permutation) stdpp(options)