proposition: Lemma space_array_1_eq: forall (sh: share) (v: (val * (val * (val*val)))) (p: val), data_at sh (tarray space_type 1) [v] p = data_at sh space_type v p.
proof: Proof. intros. pose proof (data_at_singleton_array_eq sh space_type). apply H. reflexivity. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec)