proposition: Lemma Forall2_sublist_alter f g 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') (g k') → Forall2 P (sublist_alter f i n l) (sublist_alter g i n k).
proof: Proof. intro. unfold sublist_alter, sublist_lookup. erewrite Forall2_length by eauto; intros; simplify_option_eq. auto using Forall2_app, Forall2_drop, Forall2_take. Qed.
imports: stdpp(options)