proposition: Lemma Forall2_sublist_alter_l f l k i n l' k' : Forall2 P l k → sublist_lookup i n l = Some l' → sublist_lookup i n k = Some k' → Forall2 P (f l') k' → Forall2 P (sublist_alter f i n l) k.
proof: Proof. intro. unfold sublist_lookup, sublist_alter. erewrite <-Forall2_length by eauto; intros; simplify_option_eq. apply Forall2_app_l; rewrite ?take_length_le by lia; auto using Forall2_take. apply Forall2_app_l; erewrite Forall2_length, take_length, drop_length, <-Forall2_length, Nat.min_l by eauto with lia; [done|]. rewrite drop_drop; auto using Forall2_drop. Qed.
imports: stdpp(options)