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' |- *; cbn in *