proposition: Lemma Forall2_same_length_lookup l k : Forall2 P l k ↔ length l = length k ∧ (∀ i x y, l !! i = Some x → k !! i = Some y → P x y).
proof: Proof. naive_solver eauto using Forall2_length, Forall2_lookup_lr, Forall2_same_length_lookup_2. Qed.
imports: stdpp(options)