proposition: Lemma roots_map_the_same: forall l (roots: roots_t), (forall r, In (inr r) roots -> ~ InEither r l) -> roots_map l roots = roots.
proof: Proof. do 2 intro. induction roots; intros; simpl; auto. rewrite IHroots. - f_equal. destruct a; simpl; auto. assert (~ InEither v l). { apply H. now left. } now rewrite list_bi_map_not_In. - intros. apply H. now right. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.graph_isomorphism CertiGraph.graph.reachable_ind CertiGraph.CertiGC.GCGraph