Goal:
  
  ============================
   (∀ (A B : Type) (R : A → B → Type) (l1 l2 : list A) (l1' l2' : list B),
      All2 R l1 l1' → All2 R l2 l2' → All2 R (l1 ++ l2) (l1' ++ l2'))


DEBUG:Going to execute:
induction 1; cbn