proposition: Lemma in_cprefix': forall {A: Type} (xs: list A) xs_done x0, In (xs_done, x0) (cprefix xs) -> exists xs_later, xs = xs_done ++ x0 :: xs_later.
proof: Proof. intros. rev_induction xs. + inversion H. + rewrite combine_prefixes_app_1 in H0. rewrite in_app_iff in H0. destruct H0. - destruct (H H0) as [xs_later ?]. exists (xs_later +:: x). change (x0 :: xs_later +:: x) with ((x0 :: xs_later) +:: x). rewrite app_assoc. f_equal; auto. - destruct H0 as [| []]. inversion H0; subst. exists nil; auto. 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