Goal:
    A : Type  RA : ReflectEq A  a : A  y : list A
  ============================
   ([] <> a :: y)


DEBUG:Going to execute:
<coq-core.plugins.ltac::discriminate@0>