Goal:
    A : Type  l : list A  l' : list A
  ============================
   (l ++ [] = l)


DEBUG:Going to execute:
case not_locked_false_eq_true; Ltac.assumption
Level 1: Backtrace:

In environment
A : Type
l, l' : list A
Unable to unify "l" with "l ++ []".
Level 0: Backtrace:

In environment
A : Type
l, l' : list A
Unable to unify "l" with "l ++ []".
Level 0: Backtrace:

No applicable tactic.
Level 0: Backtrace:

No applicable tactic.