Goal:
  
  X : Type
  Y : Type
  R : nat → X → Y → Type
  n : nat
  xs : list X
  ys : list Y
  a : All2i R n xs ys
  ============================
   (#|xs| = #|ys|)


DEBUG:Going to execute:
induction a

Goals:
    X : Type  Y : Type  R : nat → X → Y → Type  n : nat
  ============================
   (#|[]| = #|[]|)

  
  X : Type
  Y : Type
  R : nat → X → Y → Type
  n : nat
  x : X
  y : Y
  l : list X
  r : list Y
  r0 : R n x y
  a : All2i R (S n) l r
  IHa : #|l| = #|r|
  ============================
   (#|x :: l| = #|y :: r|)


DEBUG:Going to execute:
auto
DEBUG LTAC Evaluated term: a

Goals:
    X : Type  Y : Type  R : nat → X → Y → Type  n : nat
  ============================
   (#|[]| = #|[]|)

  
  X : Type
  Y : Type
  R : nat → X → Y → Type
  n : nat
  x : X
  y : Y
  l : list X
  r : list Y
  r0 : R n x y
  a : All2i R (S n) l r
  IHa : #|l| = #|r|
  ============================
   (#|x :: l| = #|y :: r|)


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