proposition: Lemma Forall3_lookup_lmr l k k' i x y z : Forall3 P l k k' → l !! i = Some x → 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)