proposition: Lemma Forall2_same_length_lookup_2 l k : length l = length k → (∀ i x y, l !! i = Some x → k !! i = Some y → P x y) → Forall2 P l k.
proof: Proof. rewrite <-Forall2_same_length. intros Hl Hlookup. induction Hl as [|?????? IH]; constructor; [by apply (Hlookup 0)|]. apply IH. apply (λ i, Hlookup (S i)). Qed.
imports: stdpp(options)