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


DEBUG:Going to execute:
inversion 1

Goals:
  
  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 : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : T.lt k x
  p2 : M.Raw.lt_tree x l
  p3 : M.Raw.lt_tree x r
  y : M.Raw.key
  H : M.Raw.In y (M.Raw.Node l k n r z)
  l0 : M.Raw.tree elt
  r0 : M.Raw.tree elt
  h : Int.Z_as_Int.t
  y0 : T.t
  e : elt
  H1 : T.eq y k
  H0 : l0 = l
  H2 : y0 = k
  H3 : e = n
  H4 : r0 = r
  H5 : h = z
  ============================
   (T.lt y x)

  
  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 : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : T.lt k x
  p2 : M.Raw.lt_tree x l
  p3 : M.Raw.lt_tree x r
  y : M.Raw.key
  H : M.Raw.In y (M.Raw.Node l k n r z)
  l0 : M.Raw.tree elt
  r0 : M.Raw.tree elt
  h : Int.Z_as_Int.t
  y0 : M.Raw.key
  e' : elt
  H1 : M.Raw.In y l
  H0 : l0 = l
  H2 : y0 = k
  H3 : e' = n
  H4 : r0 = r
  H5 : h = z
  ============================
   (T.lt y x)

  
  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 : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : T.lt k x
  p2 : M.Raw.lt_tree x l
  p3 : M.Raw.lt_tree x r
  y : M.Raw.key
  H : M.Raw.In y (M.Raw.Node l k n r z)
  l0 : M.Raw.tree elt
  r0 : M.Raw.tree elt
  h : Int.Z_as_Int.t
  y0 : M.Raw.key
  e' : elt
  H1 : M.Raw.In y r
  H0 : l0 = l
  H2 : y0 = k
  H3 : e' = n
  H4 : r0 = r
  H5 : h = z
  ============================
   (T.lt y x)


DEBUG:Going to execute:
subst

Goals:
  
  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 : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : T.lt k x
  p2 : M.Raw.lt_tree x l
  p3 : M.Raw.lt_tree x r
  y : M.Raw.key
  H : M.Raw.In y (M.Raw.Node l k n r z)
  l0 : M.Raw.tree elt
  r0 : M.Raw.tree elt
  h : Int.Z_as_Int.t
  y0 : T.t
  e : elt
  H1 : T.eq y k
  H0 : l0 = l
  H2 : y0 = k
  H3 : e = n
  H4 : r0 = r
  H5 : h = z
  ============================
   (T.lt y x)

  
  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 : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : T.lt k x
  p2 : M.Raw.lt_tree x l
  p3 : M.Raw.lt_tree x r
  y : M.Raw.key
  H : M.Raw.In y (M.Raw.Node l k n r z)
  l0 : M.Raw.tree elt
  r0 : M.Raw.tree elt
  h : Int.Z_as_Int.t
  y0 : M.Raw.key
  e' : elt
  H1 : M.Raw.In y l
  H0 : l0 = l
  H2 : y0 = k
  H3 : e' = n
  H4 : r0 = r
  H5 : h = z
  ============================
   (T.lt y x)

  
  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 : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : T.lt k x
  p2 : M.Raw.lt_tree x l
  p3 : M.Raw.lt_tree x r
  y : M.Raw.key
  H : M.Raw.In y (M.Raw.Node l k n r z)
  l0 : M.Raw.tree elt
  r0 : M.Raw.tree elt
  h : Int.Z_as_Int.t
  y0 : M.Raw.key
  e' : elt
  H1 : M.Raw.In y r
  H0 : l0 = l
  H2 : y0 = k
  H3 : e' = n
  H4 : r0 = r
  H5 : h = z
  ============================
   (T.lt y x)


DEBUG:Going to execute:
<coq-core.plugins.ltac::subst@1>

Goals:
  
  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 : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : T.lt k x
  p2 : M.Raw.lt_tree x l
  p3 : M.Raw.lt_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 y x)

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

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


DEBUG:Going to execute:
auto

Goals:
  
  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 : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : T.lt k x
  p2 : M.Raw.lt_tree x l
  p3 : M.Raw.lt_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 y x)

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

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


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3