proposition: Lemma Forall2_sublist_lookup_r l k n i k' : Forall2 P l k → sublist_lookup n i k = Some k' → ∃ l', sublist_lookup n i l = Some l' ∧ Forall2 P l' k'.
proof: Proof. intro. unfold sublist_lookup. erewrite Forall2_length by eauto; intros; simplify_option_eq. eauto using Forall2_take, Forall2_drop. Qed.
imports: stdpp(options)