proposition: Lemma Forall_sublist_alter_inv f l i n k : sublist_lookup i n l = Some k → Forall P (sublist_alter f i n l) → Forall P (f k).
proof: Proof. unfold sublist_alter, sublist_lookup. intros ?; simplify_option_eq. rewrite !Forall_app; tauto. Qed.
imports: stdpp(options)