proposition: Lemma body_int_or_ptr_to_int: semax_body Vprog Gprog f_int_or_ptr_to_int int_or_ptr_to_int_spec.
proof: Proof. start_function. red in H. destruct x; try easy. forward. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec)