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
  l0 : T.lt x k
  l1 : M.Raw.lt_tree x l
  l2 : M.Raw.lt_tree x r
  f : M.Raw.lt_tree x (M.Raw.Node l k n r z)
  ============================
   (T.lt ?x ?x)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::etransitivity@0>

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
  l0 : T.lt x k
  l1 : M.Raw.lt_tree x l
  l2 : M.Raw.lt_tree x r
  f : M.Raw.lt_tree x (M.Raw.Node l k n r z)
  ============================
   (T.lt ?x ?y)

  
  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
  l0 : T.lt x k
  l1 : M.Raw.lt_tree x l
  l2 : M.Raw.lt_tree x r
  f : M.Raw.lt_tree x (M.Raw.Node l k n r z)
  ============================
   (T.lt ?y ?x)


DEBUG:Going to execute:
eassumption +
             (eapply f; constructor; idtac + symmetry;
               eassumption + reflexivity)