proposition: Lemma list_alter_fmap (g : A → A) (h : B → B) l i : Forall (λ x, f (g x) = h (f x)) l → f <$> alter g i l = alter h i (f <$> l).
proof: Proof. intros Hl. revert i. by induction Hl; intros [|i]; f_equal/=. Qed.
imports: stdpp(options)