proposition: Lemma body_push: semax_body Vprog (@Gprog size inf _) f_push (@push_spec size inf _).
proof: Proof. start_function. forward. entailer!. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.find_lemmas CertiGraph.priq.priq_arr_specs CertiGraph.priq.is_empty_lemmas CertiGraph.priq.priq_arr