-- ********
--! FUNS
-- ********

-- ********
--! RULES
-- ********

heap_removemin_case e e1 e2 l1 l2 r1 r2 =
  []
  |=
  heapinv (Node (Node l1 e1 r1) e (Node l2 e2 r2))
  <=>
  heapinv (Node (Node l1 e1 r1) e (Node l2 e2 r2)) &&
    if e1 <= e2 then heapinv (Node (removemin (Node l1 e1 r1)) e1 (Node l2 e2 r2))
                else heapinv (Node (Node l1 e1 r1) e2 (removemin (Node l2 e2 r2)))

-- ********
--! CLAUSES
-- ********