Goal:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  H : ∀ (n : nat) (x : A) (y : B), R n x y
  n : nat
  l : list A
  l' : list B
  ============================
   (#|l| = #|l'| → All2i R n l l')


DEBUG:Going to execute:
induction l in n, l' |- *

Goals:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  H : ∀ (n : nat) (x : A) (y : B), R n x y
  n : nat
  l' : list B
  ============================
   (#|[]| = #|l'| → All2i R n [] l')

  
  A : Type
  B : Type
  R : nat → A → B → Type
  H : ∀ (n : nat) (x : A) (y : B), R n x y
  n : nat
  a : A
  l : list A
  l' : list B
  IHl : ∀ (n : nat) (l' : list B), #|l| = #|l'| → All2i R n l l'
  ============================
   (#|a :: l| = #|l'| → All2i R n (a :: l) l')


DEBUG:Going to execute:
destruct l'
DEBUG LTAC Evaluated term: l

Goals:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  H : ∀ (n : nat) (x : A) (y : B), R n x y
  n : nat
  ============================
   (#|[]| = #|[]| → All2i R n [] [])

  
  A : Type
  B : Type
  R : nat → A → B → Type
  H : ∀ (n : nat) (x : A) (y : B), R n x y
  n : nat
  b : B
  l' : list B
  ============================
   (#|[]| = #|b :: l'| → All2i R n [] (b :: l'))

  
  A : Type
  B : Type
  R : nat → A → B → Type
  H : ∀ (n : nat) (x : A) (y : B), R n x y
  n : nat
  a : A
  l : list A
  IHl : ∀ (n : nat) (l' : list B), #|l| = #|l'| → All2i R n l l'
  ============================
   (#|a :: l| = #|[]| → All2i R n (a :: l) [])

  
  A : Type
  B : Type
  R : nat → A → B → Type
  H : ∀ (n : nat) (x : A) (y : B), R n x y
  n : nat
  a : A
  l : list A
  b : B
  l' : list B
  IHl : ∀ (n : nat) (l' : list B), #|l| = #|l'| → All2i R n l l'
  ============================
   (#|a :: l| = #|b :: l'| → All2i R n (a :: l) (b :: l'))


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: l'
DEBUG LTAC Evaluated term: l'

Goals:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  H : ∀ (n : nat) (x : A) (y : B), R n x y
  n : nat
  ============================
   (0 = 0 → All2i R n [] [])

  
  A : Type
  B : Type
  R : nat → A → B → Type
  H : ∀ (n : nat) (x : A) (y : B), R n x y
  n : nat
  b : B
  l' : list B
  ============================
   (0 = S #|l'| → All2i R n [] (b :: l'))

  
  A : Type
  B : Type
  R : nat → A → B → Type
  H : ∀ (n : nat) (x : A) (y : B), R n x y
  n : nat
  a : A
  l : list A
  IHl : ∀ (n : nat) (l' : list B), #|l| = #|l'| → All2i R n l l'
  ============================
   (S #|l| = 0 → All2i R n (a :: l) [])

  
  A : Type
  B : Type
  R : nat → A → B → Type
  H : ∀ (n : nat) (x : A) (y : B), R n x y
  n : nat
  a : A
  l : list A
  b : B
  l' : list B
  IHl : ∀ (n : nat) (l' : list B), #|l| = #|l'| → All2i R n l l'
  ============================
   (S #|l| = S #|l'| → All2i R n (a :: l) (b :: l'))


DEBUG:Going to execute:
try discriminate