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 (M.Raw.Leaf elt))


DEBUG:Going to execute:
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) ]