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