Goal:
  
  elt : Type
  gt_tree_dec : forall (x : T.t) (t : M.Raw.tree elt),
                {M.Raw.gt_tree x t} + {~ M.Raw.gt_tree x t}
  x : T.t
  t : M.Raw.tree elt
  ============================
   ({M.Raw.gt_tree x t} + {~ M.Raw.gt_tree x t})


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