proposition: Lemma sublist_alter_compose f g l i n k : sublist_lookup i n l = Some k → length (f k) = n → length (g k) = n → sublist_alter (f ∘ g) i n l = sublist_alter f i n (sublist_alter g i n l).
proof: Proof. unfold sublist_alter, sublist_lookup. intros Hk ??; simplify_option_eq. by rewrite !take_app_length', drop_app_length', !(assoc_L (++)), drop_app_length', take_app_length' by (rewrite ?app_length, ?take_length, ?Hk; lia). Qed.
imports: stdpp(options)