Goal:
  
  X : Type
  Y : Type
  R : nat → X → Y → Type
  n : nat
  xs : list X
  xs' : list X
  ys : list Y
  ys' : list Y
  x : list Y
  x0 : list Y
  leq : ys ++ ys' = x ++ x0
  a : All2i R n xs x
  a0 : All2i R (n + #|xs|) xs' x0
  eq : #|xs| = #|ys|
  ============================
   (All2i R n xs ys × All2i R (n + #|xs|) xs' ys')


DEBUG:Going to execute:
apply app_inj_length_l in leq as (?, ?); subst
DEBUG LTAC Evaluated term: All2i_app_inv_l