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
  l : M.Raw.tree elt
  k : T.t
  n : elt
  r : M.Raw.tree elt
  z : BinNums.Z
  e : T.eq k x
  g : forall y : M.Raw.key, M.Raw.In y l -> T.lt x y
  pf : M.Raw.gt_tree x r -> False
  f : forall y : M.Raw.key, M.Raw.In y (M.Raw.Node l k n r z) -> T.lt x y
  y : M.Raw.key
  H : M.Raw.In y r
  ============================
   (T.eq y k)


DEBUG:Going to execute:
reflexivity
Level 1: Backtrace:

No such assumption.
Level 0: Backtrace:

No such assumption.