use(queue_lemma_defs).

goal
~ forall(Q,del_min_complete(Q)).