proposition: Lemma partial_alter_compose {A} f g (m : M A) i: partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m).
proof: Proof. intros. apply map_eq. intros ii. by destruct (decide (i = ii)) as [->|?]; rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne. Qed.
imports: Coq(Permutation) stdpp(options)