Goal:
    A : Type  B : Type  R : A → B → Type  l1 : list A
  ============================
   (∀ (l2 : list A) (r : list B),
      All2 R (l1 ++ l2) r
      → ∑ r1 r2 : list B, r = r1 ++ r2 × All2 R l1 r1 × All2 R l2 r2)


DEBUG:Going to execute:
induction l1; intros