proposition: Lemma data_at__value_0_size: forall sh p, data_at_ sh (tarray int_or_ptr_type 0) p |-- emp.
proof: Proof. intros. rewrite data_at__eq. apply data_at_zero_array_inv; reflexivity. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec) CertiGraph.msl_ext.ramification_lemmas VST.concurrency.conclib