proposition: Lemma Forall3_lookup_l l k k' i x : Forall3 P l k k' → l !! i = Some x → ∃ y z, k !! i = Some y ∧ k' !! i = Some z ∧ P x y z.
proof: Proof. intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto. Qed.
imports: stdpp(options)