proposition: Lemma lookup_total_partial_alter {A} `{Inhabited A} (f : option A → option A) (m : M A) i: partial_alter f i m !!! i = default inhabitant (f (m !! i)).
proof: Proof. by rewrite lookup_total_alt, lookup_partial_alter. Qed.
imports: Coq(Permutation) stdpp(options)