Goal:
  
  elt : Type
  bst_dec : forall t : M.Raw.tree elt, {M.Raw.bst t} + {~ M.Raw.bst t}
  t : M.Raw.tree elt
  ============================
   ({M.Raw.bst t} + {~ M.Raw.bst t})


DEBUG:Going to execute:
refine
match t with
| M.Raw.Leaf _ => left _
| M.Raw.Node l k n r z =>
    match bst_dec l, bst_dec r, lt_tree_dec k l, gt_tree_dec k r with
    | right pf, _, _, _ | _, right pf, _, _ | _, _, right pf, _ |
      _, _, _, right pf => right _
    | left p1, left p2, left p3, left p4 => left _
    end
end