proposition: Lemma Forall_alter f l i : Forall P l → (∀ x, l !! i = Some x → P x → P (f x)) → Forall P (alter f i l).
proof: Proof. intros Hl. revert i. induction Hl; simpl; intros [|i]; constructor; auto. Qed.
imports: stdpp(options)