proposition: Lemma partial_alter_subset {A} f (m : M A) i : m !! i = None → is_Some (f (m !! i)) → m ⊂ partial_alter f i m.
proof: Proof. intros Hi Hfi. apply map_subset_alt; split; [by apply partial_alter_subseteq|]. exists i. by rewrite lookup_partial_alter. Qed.
imports: Coq(Permutation) stdpp(options)