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


DEBUG:Going to execute:
induction l in l', r |- *; simpl; intros; destruct l'; simpl in *