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