proposition: Lemma Forall2_sublist_lookup_l l k n i l' : Forall2 P l k → sublist_lookup n i l = Some l' → ∃ k', sublist_lookup n i k = Some k' ∧ Forall2 P l' k'.
proof: Proof. unfold sublist_lookup. intros Hlk Hl. exists (take i (drop n k)); simplify_option_eq. - auto using Forall2_take, Forall2_drop. - apply Forall2_length in Hlk; lia. Qed.
imports: stdpp(options)