proposition: Lemma Forall_sublist_lookup l i n k : sublist_lookup i n l = Some k → Forall P l → Forall P k.
proof: Proof. unfold sublist_lookup. intros; simplify_option_eq. auto using Forall_take, Forall_drop. Qed.
imports: stdpp(options)