fact: Definition pq_free_spec := DECLARE _pq_free WITH pq : val, h : heap PRE [tptr t_pq] PROP () PARAMS (pq) GLOBALS () SEP (valid_pq pq h) POST [tvoid] PROP () LOCAL () SEP (emp).
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_Zmodel CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.env_binary_heap_pro