proposition: Lemma sepcon_unique_vertex_at sh: writable_share sh -> iter_sepcon.sepcon_unique2 (@vertex_at _ _ _ _ _ (SGP_VST sh)).
proof: Proof. intros. hnf; intros. simpl. destruct y1 as [[? ?] ?], y2 as [[? ?] ?]. unfold trinode. rewrite data_at_isptr. normalize. apply data_at_conflict. + apply readable_nonidentity, writable_readable. auto. + simpl. lia. Qed.
imports: CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin VST.veric.SeparationLogic CertiGraph.dispose.env_dispose_bin CertiGraph.floyd_ext.share