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