Goal:
  
  ============================
   (CompareSpec (false = true) (lt false true) (lt true false)
      (compare false true))


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