proposition: Lemma Forall_upd_Znth: forall (l: list Z) (i: Z) new F, (0 <= i < Zlength l)%Z -> Forall F l -> F new -> Forall F (upd_Znth i l new).
proof: Proof. intros. rewrite Forall_forall in *. intros. destruct (Z.eq_dec x new); [rewrite e; trivial|]. rewrite upd_Znth_unfold in H2; auto. apply in_app_or in H2; destruct H2. - apply sublist_In in H2. apply (H0 x H2). - simpl in H2. destruct H2; [lia|]. apply sublist_In in H2. apply (H0 x H2). Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver