proposition: Lemma ti_rel_token_the_same: forall (h1 h2: heap) p, heap_relation h1 h2 -> ti_token_rep h1 p = ti_token_rep h2 p.
proof: Proof. intros. destruct H. unfold ti_token_rep. f_equal. apply (iter_sepcon_pointwise_eq _ _ _ _ null_space null_space). - rewrite <- !ZtoNat_Zlength, !spaces_size. reflexivity. - intros. fold (nth_space h1 i). fold (nth_space h2 i). unfold gen_size in H. unfold space_token_rep. rewrite H, H0. reflexivity. 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