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 (?, ?)

Goals:
  
  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
  H : ys = x
  H0 : ys' = 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')

  
  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|
  ============================
   (#|ys| = #|x|)


DEBUG:Going to execute:
subst
DEBUG LTAC Evaluated term: app_inj_length_l

Goals:
  
  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
  H : ys = x
  H0 : ys' = 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')

  
  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|
  ============================
   (#|ys| = #|x|)


DEBUG:Going to execute:
<coq-core.plugins.ltac::subst@1>

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

  
  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|
  ============================
   (#|ys| = #|x|)


DEBUG:Going to execute:
auto

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

  
  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|
  ============================
   (#|ys| = #|x|)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3