fact: Definition Gprog {CS: compspecs}: funspecs := ltac:(with_library prog [mallocN_spec; freePQ_spec; init_spec; push_spec; pq_emp_spec; adjustWeight_spec; popMin_spec]).
imports: VST.floyd.proofauto CertiGraph.lib.find_lemmas CertiGraph.priq.is_empty_lemmas CertiGraph.priq.priq_arr