proposition: Lemma alter_compose {A} (f g : A → A) (m : M A) i: alter (f ∘ g) i m = alter f i (alter g i m).
proof: Proof. unfold alter, map_alter. rewrite <-partial_alter_compose. apply partial_alter_ext. by intros [?|]. Qed.
imports: Coq(Permutation) stdpp(options)