proposition: Lemma fold_left_ext: forall {A B} (f g: A -> B -> A) l init, (forall x y, In y l -> f x y = g x y) -> fold_left f l init = fold_left g l init.
proof: Proof. intros. revert init. rev_induction l; intros; simpl. 1: reflexivity. rewrite !fold_left_app. simpl. rewrite H; intros; apply H0; rewrite in_app_iff; intuition. 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