Goal:
    s : t  s' : t  e : false = true  H : lt s s'
  ============================
   (s = s')


DEBUG:Going to execute:
Ltac.symmetry; trivial
Level 1: Backtrace:

In environment
s, s' : t
e : false = true
H : lt s s'
Unable to unify "s'" with "s".
Level 0: Backtrace:

In environment
s, s' : t
e : false = true
H : lt s s'
Unable to unify "s'" with "s".