Goal:
    x : t  y : t  e : x = y  z : t  t : t  e' : z = t
  ============================
   (lt x z <-> lt y t)


DEBUG:Going to execute:
subst
DEBUG LTAC Evaluated term: lt_irreflexive
DEBUG LTAC Evaluated term: lt_transitive