Goal:
    l1 : t  l2 : t
  ============================
   ({l1 = l2} + {l1 <> l2})


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