use(queues).

/* 
   queue induction
  
   qi(P) == P(empty) and forall(Q,P(Q) => forall(E,P(insert(Q,E)))

   we have to instantiate this manually for each P

   In a higher-order logic we would prove that queue induction
   is correct, that is,

            qi(P) => forall(Q,P(Q)),

   using del_min_complete.
*/



(p(empty) and forall(Q,(p(Q) => forall(E,p(insert(Q,E)))))) -> forall(Q,q(Q)).