Goal:
  
  A : Type
  P : A → A → Type
  a : A
  l' : list A
  r : A
  r' : A
  X : All2 P [r] (a :: l' ++ [r'])
  X0 : P r a
  X1 : All2 P [] (l' ++ [r'])
  H : [] = l' ++ [r']
  ============================
   (All2 P [] (a :: l') × P r r')


DEBUG:Going to execute:
destruct l'

Goals:
  
  A : Type
  P : A → A → Type
  a : A
  r : A
  r' : A
  X : All2 P [r] (a :: [] ++ [r'])
  X0 : P r a
  X1 : All2 P [] ([] ++ [r'])
  H : [] = [] ++ [r']
  ============================
   (All2 P [] [a] × P r r')

  
  A : Type
  P : A → A → Type
  a : A
  a0 : A
  l' : list A
  r : A
  r' : A
  X : All2 P [r] (a :: (a0 :: l') ++ [r'])
  X0 : P r a
  X1 : All2 P [] ((a0 :: l') ++ [r'])
  H : [] = (a0 :: l') ++ [r']
  ============================
   (All2 P [] (a :: a0 :: l') × P r r')


DEBUG:Going to execute:
inversion H
DEBUG LTAC Evaluated term: l'