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