fact: Definition trinode (sh: share) (p: addr) (dlr: bool * addr * addr): mpred := data_at sh node_type (vgamma2cdata dlr) (pointer_val_val p).
imports: CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin VST.veric.SeparationLogic CertiGraph.dispose.env_dispose_bin CertiGraph.floyd_ext.share