proposition: Lemma lacv_icgr_not_eq: forall l g v to, ~ In to l -> graph_has_gen g to -> no_dangling_dst g -> copy_compatible g -> iter_sepcon l (generation_rep (lgraph_add_copied_v g v to)) = iter_sepcon l (generation_rep g).
proof: Proof. intros. induction l; simpl. 1: reflexivity. rewrite IHl. - f_equal. apply lacv_generation_rep_not_eq; [|assumption..]. intro. apply H. left. assumption. - intro. apply H. right. assumption. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List