proposition: Lemma map_snd_cprefix': forall {A B: Type} (l: list A) (f: A -> B), map f l = map (fun p => f (snd p)) (cprefix l).
proof: Proof. intros. unfold cprefix. rewrite <- (map_map snd f). rewrite map_snd_combine; auto. apply length_prefixes. 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