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
  ============================
   ({M.Raw.lt_tree x t} + {~ M.Raw.lt_tree x t})


DEBUG:Going to execute:
<coq-core.plugins.ltac::refine@0> $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
  ============================
   (M.Raw.lt_tree x (M.Raw.Leaf elt))

  
  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))

  
  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 k x
  l1 : M.Raw.lt_tree x l
  pf : ~ M.Raw.lt_tree x r
  ============================
   (~ M.Raw.lt_tree x (M.Raw.Node l k n r z))

  
  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 k x
  pf : ~ M.Raw.lt_tree x l
  s := lt_tree_dec x r : {M.Raw.lt_tree x r} + {~ M.Raw.lt_tree x r}
  ============================
   (~ M.Raw.lt_tree x (M.Raw.Node l k n r z))

  
  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
  e : T.eq k x
  l0 : M.Raw.lt_tree x l
  l1 : M.Raw.lt_tree x r
  ============================
   (~ M.Raw.lt_tree x (M.Raw.Node l k n r z))

  
  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
  e : T.eq k x
  l0 : M.Raw.lt_tree x l
  pf : ~ M.Raw.lt_tree x r
  ============================
   (~ M.Raw.lt_tree x (M.Raw.Node l k n r z))

  
  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
  e : T.eq k x
  pf : ~ M.Raw.lt_tree x l
  s := lt_tree_dec x r : {M.Raw.lt_tree x r} + {~ M.Raw.lt_tree x r}
  ============================
   (~ M.Raw.lt_tree x (M.Raw.Node l k n r z))

  
  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
  ============================
   (~ M.Raw.lt_tree x (M.Raw.Node l k n r z))

  
  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
  pf : ~ M.Raw.lt_tree x r
  ============================
   (~ M.Raw.lt_tree x (M.Raw.Node l k n r z))

  
  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
  pf : ~ M.Raw.lt_tree x l
  s := lt_tree_dec x r : {M.Raw.lt_tree x r} + {~ M.Raw.lt_tree x r}
  ============================
   (~ M.Raw.lt_tree x (M.Raw.Node l k n r z))


DEBUG:Going to execute:
try (solve
            [ inversion 1
            | inversion 1; subst; auto;
               match goal with
               | H:T.lt _ _, H':T.eq _ _
                 |- _ => now first [ rewrite H' in H | rewrite <- H' in H ]
               end
            | intro f; apply pf; hnf in *; intros; apply f; constructor;
               assumption + reflexivity
            | intro f; eapply M.Raw.Proofs.MX.lt_antirefl;
               idtac + etransitivity;
               eassumption +
                 (eapply f; constructor; idtac + symmetry;
                   eassumption + reflexivity) ])