Goal:
    x : string
  ============================
   (eq x x)


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

Goals:
    x : string  y : string  H : x = y
  ============================
   (Eq = Lt <-> compare y x = Gt)

    x : string  y : string  H : lt x y
  ============================
   (Lt = Lt <-> compare y x = Gt)

    x : string  y : string  H : lt y x
  ============================
   (Gt = Lt <-> compare y x = Gt)


DEBUG:Going to execute:
split; try congruence
DEBUG LTAC Evaluated term: (compare_spec x y)

Goals:
    x : string  y : string  H : x = y
  ============================
   (Eq = Lt <-> compare y x = Gt)

    x : string  y : string  H : lt x y
  ============================
   (Lt = Lt <-> compare y x = Gt)

    x : string  y : string  H : lt y x
  ============================
   (Gt = Lt <-> compare y x = Gt)


DEBUG:Going to execute:
split

Goals:
    x : string  y : string  H : x = y
  ============================
   (Eq = Lt <-> compare y x = Gt)

    x : string  y : string  H : lt x y
  ============================
   (Lt = Lt <-> compare y x = Gt)

    x : string  y : string  H : lt y x
  ============================
   (Gt = Lt <-> compare y x = Gt)


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

Goals:
    x : string  y : string  H : x = y
  ============================
   (Eq = Lt -> compare y x = Gt)

    x : string  y : string  H : x = y
  ============================
   (compare y x = Gt -> Eq = Lt)

    x : string  y : string  H : lt x y
  ============================
   (Lt = Lt -> compare y x = Gt)

    x : string  y : string  H : lt x y
  ============================
   (compare y x = Gt -> Lt = Lt)

    x : string  y : string  H : lt y x
  ============================
   (Gt = Lt -> compare y x = Gt)

    x : string  y : string  H : lt y x
  ============================
   (compare y x = Gt -> Gt = Lt)


DEBUG:Going to execute:
try congruence