Goal:
  
  A : Type
  B : Type
  R : A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  h : All2 R l l'
  IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
  ============================
   (All2 R (skipn (S n) (x :: l)) (skipn (S n) (y :: l')))


DEBUG:Going to execute:
<coq-core.plugins.ltac::econstructor@0>

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  h : All2 R l l'
  IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
  ============================
   (R x y)

  
  A : Type
  B : Type
  R : A → B → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  h : All2 R l l'
  IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
  ============================
   (All2 R l l')

  
  A : Type
  B : Type
  R : A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  h : All2 R l l'
  IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
  ============================
   (All2 R (skipn (S n) (x :: l)) (skipn (S n) (y :: l')))


DEBUG:Going to execute:
eauto
Level 0: Backtrace:

In environment
A : Type
B : Type
R : A → B → Type
n : nat
x : A
y : B
l : list A
l' : list B
r : R x y
h : All2 R l l'
IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
Unable to unify "All2 ?M2761 (?M2762 :: ?M2764) (?M2763 :: ?M2765)" with
 "All2 R (skipn (S n) (x :: l)) (skipn (S n) (y :: l'))".
Level 0: Backtrace:

In environment
A : Type
B : Type
R : A → B → Type
n : nat
x : A
y : B
l : list A
l' : list B
r : R x y
h : All2 R l l'
IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
Unable to unify "All2 ?M2761 (?M2762 :: ?M2764) (?M2763 :: ?M2765)" with
 "All2 R (skipn (S n) (x :: l)) (skipn (S n) (y :: l'))".

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  h : All2 R l l'
  IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
  ============================
   (R x y)

  
  A : Type
  B : Type
  R : A → B → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  h : All2 R l l'
  IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
  ============================
   (All2 R l l')

  
  A : Type
  B : Type
  R : A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  h : All2 R l l'
  IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
  ============================
   (All2 R (skipn (S n) (x :: l)) (skipn (S n) (y :: l')))


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