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 (M.Raw.Leaf elt))


DEBUG:Going to execute:
inversion 1