Goal:
  
  A : Type
  P : A → A → Prop
  a : A
  l' : list A
  r : A
  r' : A
  H : Forall2 P [r] (a :: l' ++ [r'])
  H3 : P r a
  H5 : Forall2 P [] (l' ++ [r'])
  ============================
   (Forall2 P [] (a :: l') ∧ P r r')


DEBUG:Going to execute:
destruct l'

Goals:
  
  A : Type
  P : A → A → Prop
  a : A
  r : A
  r' : A
  H : Forall2 P [r] (a :: [] ++ [r'])
  H3 : P r a
  H5 : Forall2 P [] ([] ++ [r'])
  ============================
   (Forall2 P [] [a] ∧ P r r')

  
  A : Type
  P : A → A → Prop
  a : A
  a0 : A
  l' : list A
  r : A
  r' : A
  H : Forall2 P [r] (a :: (a0 :: l') ++ [r'])
  H3 : P r a
  H5 : Forall2 P [] ((a0 :: l') ++ [r'])
  ============================
   (Forall2 P [] (a :: a0 :: l') ∧ P r r')


DEBUG:Going to execute:
cbn in *
DEBUG LTAC Evaluated term: l'