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 : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : T.lt x k
  p2 : M.Raw.gt_tree x l
  p3 : M.Raw.gt_tree x r
  y : M.Raw.key
  H : M.Raw.In y (M.Raw.Node l k n r z)
  H1 : T.eq y k
  ============================
   (T.lt x y)


DEBUG:Going to execute:
rewrite <- H' in H
DEBUG LTAC Evaluated term: H1
Level 1: Backtrace:

Found no subterm matching "y" in the current goal.