proposition: Lemma Forall2_lookup l k : Forall2 P l k ↔ ∀ i, option_Forall2 P (l !! i) (k !! i).
proof: Proof. split; [induction 1; intros [|?]; simpl; try constructor; eauto|]. revert k. induction l as [|x l IH]; intros [| y k] H. - done. - oinv (H 0). - oinv (H 0). - constructor; [by oinv (H 0)|]. apply (IH _ $ λ i, H (S i)). Qed.
imports: stdpp(options)