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
  l0 : T.lt k x
  g : M.Raw.gt_tree x l
  g0 : M.Raw.gt_tree x r
  f : M.Raw.gt_tree x (M.Raw.Node l k n r z)
  ============================
   (M.Raw.In x l)


DEBUG:Going to execute:
idtac + symmetry
Level 1: Backtrace:

In environment
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, l : M.Raw.tree elt
k : M.Raw.key
n : elt
r : M.Raw.tree elt
z : Int.Z_as_Int.t
l0 : T.lt k x
g : M.Raw.gt_tree x l
g0 : M.Raw.gt_tree x r
f : M.Raw.gt_tree x (M.Raw.Node l k n r z)
Unable to unify "x" with "k".
Level 0: Backtrace:

In environment
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, l : M.Raw.tree elt
k : M.Raw.key
n : elt
r : M.Raw.tree elt
z : Int.Z_as_Int.t
l0 : T.lt k x
g : M.Raw.gt_tree x l
g0 : M.Raw.gt_tree x r
f : M.Raw.gt_tree x (M.Raw.Node l k n r z)
Unable to unify "x" with "k".
Level 0: Backtrace:

In environment
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, l : M.Raw.tree elt
k : M.Raw.key
n : elt
r : M.Raw.tree elt
z : Int.Z_as_Int.t
l0 : T.lt k x
g : M.Raw.gt_tree x l
g0 : M.Raw.gt_tree x r
f : M.Raw.gt_tree x (M.Raw.Node l k n r z)
Unable to unify "x" with "k".
Level 1: Backtrace:

In environment
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, l : M.Raw.tree elt
k : M.Raw.key
n : elt
r : M.Raw.tree elt
z : Int.Z_as_Int.t
l0 : T.lt k x
g : M.Raw.gt_tree x l
g0 : M.Raw.gt_tree x r
f : M.Raw.gt_tree x (M.Raw.Node l k n r z)
Unable to unify "x" with "k".
Level 0: Backtrace:

In environment
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, l : M.Raw.tree elt
k : M.Raw.key
n : elt
r : M.Raw.tree elt
z : Int.Z_as_Int.t
l0 : T.lt k x
g : M.Raw.gt_tree x l
g0 : M.Raw.gt_tree x r
f : M.Raw.gt_tree x (M.Raw.Node l k n r z)
Unable to unify "x" with "k".
Level 0: Backtrace:

In environment
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, l : M.Raw.tree elt
k : M.Raw.key
n : elt
r : M.Raw.tree elt
z : Int.Z_as_Int.t
l0 : T.lt k x
g : M.Raw.gt_tree x l
g0 : M.Raw.gt_tree x r
f : M.Raw.gt_tree x (M.Raw.Node l k n r z)
Unable to unify "x" with "k".