Goal:
    A : Type  R : ReflectEq A  x : A  y : A  Heq_anonymous : true = (x == y)
  ============================
   (is_true (x == y))


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

In environment
A : Type
R : ReflectEq A
x, y : A
Heq_anonymous : true = (x == y)
Unable to unify "true" with "x == y".
Level 0: Backtrace:

In environment
A : Type
R : ReflectEq A
x, y : A
Heq_anonymous : true = (x == y)
Unable to unify "true" with "x == y".