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