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 : #|xs| = #|x|
  a0 : #|xs'| = #|x0|
  eq : #|xs| = #|ys|
  ============================
   (#|ys| = #|x|)


DEBUG:Going to execute:
<coq-core.plugins.cc::cc@0> $1
DEBUG LTAC Evaluated term: All2i_length
DEBUG LTAC Evaluated term: All2i_length