Goal:
  
  A : Type
  R : list A → nat → A → A → Type
  P : ∀ (L : list A) (i : nat) (l l' : list A), OnOne2i (R L) i l l' → Type
  hhd : ∀ (L : list A) (i : nat) (x y : A) (l : list A) (r : R L i x y),
          P L i (x :: l) (y :: l) (OnOne2i_hd (R L) i x y l r)
  htl : ∀ (L : list A) (i : nat) (x : A) (l l' : list A) 
          (h : OnOne2i (R L) (S i) l l'),
          P L (S i) l l' h
          → P L i (x :: l) (x :: l') (OnOne2i_tl (R L) i x l l' h)
  i : nat
  l : list A
  l' : list A
  h : OnOne2i (R l) i l l'
  ============================
   (P l i l l' h)


DEBUG:Going to execute:
induction h

Goals:
  
  A : Type
  R : list A → nat → A → A → Type
  P : ∀ (L : list A) (i : nat) (l l' : list A), OnOne2i (R L) i l l' → Type
  hhd : ∀ (L : list A) (i : nat) (x y : A) (l : list A) (r : R L i x y),
          P L i (x :: l) (y :: l) (OnOne2i_hd (R L) i x y l r)
  htl : ∀ (L : list A) (i : nat) (x : A) (l l' : list A) 
          (h : OnOne2i (R L) (S i) l l'),
          P L (S i) l l' h
          → P L i (x :: l) (x :: l') (OnOne2i_tl (R L) i x l l' h)
  l : list A
  i : nat
  hd : A
  hd' : A
  tl : list A
  p : R l i hd hd'
  ============================
   (P l i (hd :: tl) (hd' :: tl) (OnOne2i_hd (R l) i hd hd' tl p))

  
  A : Type
  R : list A → nat → A → A → Type
  P : ∀ (L : list A) (i : nat) (l l' : list A), OnOne2i (R L) i l l' → Type
  hhd : ∀ (L : list A) (i : nat) (x y : A) (l : list A) (r : R L i x y),
          P L i (x :: l) (y :: l) (OnOne2i_hd (R L) i x y l r)
  htl : ∀ (L : list A) (i : nat) (x : A) (l l' : list A) 
          (h : OnOne2i (R L) (S i) l l'),
          P L (S i) l l' h
          → P L i (x :: l) (x :: l') (OnOne2i_tl (R L) i x l l' h)
  l : list A
  i : nat
  hd : A
  tl : list A
  tl' : list A
  h : OnOne2i (R l) (S i) tl tl'
  IHh : P l (S i) tl tl' h
  ============================
   (P l i (hd :: tl) (hd :: tl') (OnOne2i_tl (R l) i hd tl tl' h))


DEBUG:Going to execute:
eauto
DEBUG LTAC Evaluated term: h

Goals:
  
  A : Type
  R : list A → nat → A → A → Type
  P : ∀ (L : list A) (i : nat) (l l' : list A), OnOne2i (R L) i l l' → Type
  hhd : ∀ (L : list A) (i : nat) (x y : A) (l : list A) (r : R L i x y),
          P L i (x :: l) (y :: l) (OnOne2i_hd (R L) i x y l r)
  htl : ∀ (L : list A) (i : nat) (x : A) (l l' : list A) 
          (h : OnOne2i (R L) (S i) l l'),
          P L (S i) l l' h
          → P L i (x :: l) (x :: l') (OnOne2i_tl (R L) i x l l' h)
  l : list A
  i : nat
  hd : A
  hd' : A
  tl : list A
  p : R l i hd hd'
  ============================
   (P l i (hd :: tl) (hd' :: tl) (OnOne2i_hd (R l) i hd hd' tl p))

  
  A : Type
  R : list A → nat → A → A → Type
  P : ∀ (L : list A) (i : nat) (l l' : list A), OnOne2i (R L) i l l' → Type
  hhd : ∀ (L : list A) (i : nat) (x y : A) (l : list A) (r : R L i x y),
          P L i (x :: l) (y :: l) (OnOne2i_hd (R L) i x y l r)
  htl : ∀ (L : list A) (i : nat) (x : A) (l l' : list A) 
          (h : OnOne2i (R L) (S i) l l'),
          P L (S i) l l' h
          → P L i (x :: l) (x :: l') (OnOne2i_tl (R L) i x l l' h)
  l : list A
  i : nat
  hd : A
  tl : list A
  tl' : list A
  h : OnOne2i (R l) (S i) tl tl'
  IHh : P l (S i) tl tl' h
  ============================
   (P l i (hd :: tl) (hd :: tl') (OnOne2i_tl (R l) i hd tl tl' h))


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