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