Goal:
    x : t  x' : t  H1 : x = x'  y : t  y' : t  H2 : y = y'
  ============================
   (lt x y <-> lt x' y')


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