proposition: Lemma zip_with_sublist_alter {A B} (f : A → B → A) g l k i n l' k' : length l = length k → sublist_lookup i n l = Some l' → sublist_lookup i n k = Some k' → length (g l') = length k' → zip_with f (g l') k' = g (zip_with f l' k') → zip_with f (sublist_alter g i n l) k = sublist_alter g i n (zip_with f l k).
proof: Proof. unfold sublist_lookup, sublist_alter. intros Hlen; rewrite Hlen. intros ?? Hl' Hk'. simplify_option_eq. by rewrite !zip_with_app_l, !zip_with_drop, Hl', drop_drop, !zip_with_take, !take_length_le, Hk' by (rewrite ?drop_length; auto with lia). Qed.
imports: stdpp(options)