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


DEBUG:Going to execute:
unfold eq in *