proposition: Lemma sublist_alter_length f l i n k : sublist_lookup i n l = Some k → length (f k) = n → length (sublist_alter f i n l) = length l.
proof: Proof. unfold sublist_alter, sublist_lookup. intros Hk ?; simplify_option_eq. rewrite !app_length, Hk, !take_length, !drop_length; lia. Qed.
imports: stdpp(options)