Goal:
  
  elt : Type
  lt_tree_dec : forall (x : T.t) (t : M.Raw.tree elt),
                {M.Raw.lt_tree x t} + {~ M.Raw.lt_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
  l0 : T.lt x k
  pf : M.Raw.lt_tree x l -> False
  s := lt_tree_dec x r : {M.Raw.lt_tree x r} + {~ M.Raw.lt_tree x r}
  f : forall y : M.Raw.key, M.Raw.In y (M.Raw.Node l k n r z) -> T.lt y x
  y : M.Raw.key
  H : M.Raw.In y l
  ============================
   (M.Raw.In y l)


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

In environment
elt : Type
lt_tree_dec : forall (x : T.t) (t : M.Raw.tree elt),
              {M.Raw.lt_tree x t} + {~ M.Raw.lt_tree x t}
x : T.t
t, l : M.Raw.tree elt
k : T.t
n : elt
r : M.Raw.tree elt
z : BinNums.Z
l0 : T.lt x k
pf : M.Raw.lt_tree x l -> False
s := lt_tree_dec x r : {M.Raw.lt_tree x r} + {~ M.Raw.lt_tree x r}
f : forall y : M.Raw.key, M.Raw.In y (M.Raw.Node l k n r z) -> T.lt y x
y : M.Raw.key
H : M.Raw.In y l
Unable to unify "k" with "y".
Level 0: Backtrace:

In environment
elt : Type
lt_tree_dec : forall (x : T.t) (t : M.Raw.tree elt),
              {M.Raw.lt_tree x t} + {~ M.Raw.lt_tree x t}
x : T.t
t, l : M.Raw.tree elt
k : T.t
n : elt
r : M.Raw.tree elt
z : BinNums.Z
l0 : T.lt x k
pf : M.Raw.lt_tree x l -> False
s := lt_tree_dec x r : {M.Raw.lt_tree x r} + {~ M.Raw.lt_tree x r}
f : forall y : M.Raw.key, M.Raw.In y (M.Raw.Node l k n r z) -> T.lt y x
y : M.Raw.key
H : M.Raw.In y l
Unable to unify "k" with "y".
Level 0: Backtrace:

In environment
elt : Type
lt_tree_dec : forall (x : T.t) (t : M.Raw.tree elt),
              {M.Raw.lt_tree x t} + {~ M.Raw.lt_tree x t}
x : T.t
t, l : M.Raw.tree elt
k : T.t
n : elt
r : M.Raw.tree elt
z : BinNums.Z
l0 : T.lt x k
pf : M.Raw.lt_tree x l -> False
s := lt_tree_dec x r : {M.Raw.lt_tree x r} + {~ M.Raw.lt_tree x r}
f : forall y : M.Raw.key, M.Raw.In y (M.Raw.Node l k n r z) -> T.lt y x
y : M.Raw.key
H : M.Raw.In y l
Unable to unify "k" with "y".