Goal:
    A : Type  P : A → A → Type  l : list A  l' : list A  r : A  r' : A
  ============================
   (All2 P (l ++ [r]) (l' ++ [r']) → All2 P l l' × P r r')


DEBUG:Going to execute:
induction l in l' |- *

Goals:
    A : Type  P : A → A → Type  l' : list A  r : A  r' : A
  ============================
   (All2 P ([] ++ [r]) (l' ++ [r']) → All2 P [] l' × P r r')

  
  A : Type
  P : A → A → Type
  a : A
  l : list A
  l' : list A
  r : A
  r' : A
  IHl : ∀ l' : list A, All2 P (l ++ [r]) (l' ++ [r']) → All2 P l l' × P r r'
  ============================
   (All2 P ((a :: l) ++ [r]) (l' ++ [r']) → All2 P (a :: l) l' × P r r')


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

Goals:
    A : Type  P : A → A → Type  l' : list A  r : A  r' : A
  ============================
   (All2 P [r] (l' ++ [r']) → All2 P [] l' × P r r')

  
  A : Type
  P : A → A → Type
  a : A
  l : list A
  l' : list A
  r : A
  r' : A
  IHl : ∀ l' : list A, All2 P (l ++ [r]) (l' ++ [r']) → All2 P l l' × P r r'
  ============================
   (All2 P (a :: l ++ [r]) (l' ++ [r']) → All2 P (a :: l) l' × P r r')


DEBUG:Going to execute:
intro X