Goal:
  
  A : Type
  B : Type
  R : list A → B → A → A → Type
  P : ∀ (L : list A) (i : list B) (l l' : list A),
        OnOne2All (R L) i l l' → Type
  hhd : ∀ (L : list A) (b : B) (bs : list B) (x y : A) 
          (l : list A) (r : R L b x y) (len : #|bs| = #|l|),
          P L (b :: bs) (x :: l) (y :: l)
            (OnOne2All_hd (R L) b bs x y l r len)
  htl : ∀ (L : list A) (b : B) (bs : list B) (x : A) 
          (l l' : list A) (h : OnOne2All (R L) bs l l'),
          P L bs l l' h
          → P L (b :: bs) (x :: l) (x :: l')
              (OnOne2All_tl (R L) b bs x l l' h)
  i : list B
  l : list A
  l' : list A
  h : OnOne2All (R l) i l l'
  ============================
   (P l i l l' h)


DEBUG:Going to execute:
induction h

Goals:
  
  A : Type
  B : Type
  R : list A → B → A → A → Type
  P : ∀ (L : list A) (i : list B) (l l' : list A),
        OnOne2All (R L) i l l' → Type
  hhd : ∀ (L : list A) (b : B) (bs : list B) (x y : A) 
          (l : list A) (r : R L b x y) (len : #|bs| = #|l|),
          P L (b :: bs) (x :: l) (y :: l)
            (OnOne2All_hd (R L) b bs x y l r len)
  htl : ∀ (L : list A) (b : B) (bs : list B) (x : A) 
          (l l' : list A) (h : OnOne2All (R L) bs l l'),
          P L bs l l' h
          → P L (b :: bs) (x :: l) (x :: l')
              (OnOne2All_tl (R L) b bs x l l' h)
  l : list A
  b : B
  bs : list B
  hd : A
  hd' : A
  tl : list A
  p : R l b hd hd'
  e : #|bs| = #|tl|
  ============================
   (P l (b :: bs) (hd :: tl) (hd' :: tl)
      (OnOne2All_hd (R l) b bs hd hd' tl p e))

  
  A : Type
  B : Type
  R : list A → B → A → A → Type
  P : ∀ (L : list A) (i : list B) (l l' : list A),
        OnOne2All (R L) i l l' → Type
  hhd : ∀ (L : list A) (b : B) (bs : list B) (x y : A) 
          (l : list A) (r : R L b x y) (len : #|bs| = #|l|),
          P L (b :: bs) (x :: l) (y :: l)
            (OnOne2All_hd (R L) b bs x y l r len)
  htl : ∀ (L : list A) (b : B) (bs : list B) (x : A) 
          (l l' : list A) (h : OnOne2All (R L) bs l l'),
          P L bs l l' h
          → P L (b :: bs) (x :: l) (x :: l')
              (OnOne2All_tl (R L) b bs x l l' h)
  l : list A
  b : B
  bs : list B
  hd : A
  tl : list A
  tl' : list A
  h : OnOne2All (R l) bs tl tl'
  IHh : P l bs tl tl' h
  ============================
   (P l (b :: bs) (hd :: tl) (hd :: tl')
      (OnOne2All_tl (R l) b bs hd tl tl' h))


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

Goals:
  
  A : Type
  B : Type
  R : list A → B → A → A → Type
  P : ∀ (L : list A) (i : list B) (l l' : list A),
        OnOne2All (R L) i l l' → Type
  hhd : ∀ (L : list A) (b : B) (bs : list B) (x y : A) 
          (l : list A) (r : R L b x y) (len : #|bs| = #|l|),
          P L (b :: bs) (x :: l) (y :: l)
            (OnOne2All_hd (R L) b bs x y l r len)
  htl : ∀ (L : list A) (b : B) (bs : list B) (x : A) 
          (l l' : list A) (h : OnOne2All (R L) bs l l'),
          P L bs l l' h
          → P L (b :: bs) (x :: l) (x :: l')
              (OnOne2All_tl (R L) b bs x l l' h)
  l : list A
  b : B
  bs : list B
  hd : A
  hd' : A
  tl : list A
  p : R l b hd hd'
  e : #|bs| = #|tl|
  ============================
   (P l (b :: bs) (hd :: tl) (hd' :: tl)
      (OnOne2All_hd (R l) b bs hd hd' tl p e))

  
  A : Type
  B : Type
  R : list A → B → A → A → Type
  P : ∀ (L : list A) (i : list B) (l l' : list A),
        OnOne2All (R L) i l l' → Type
  hhd : ∀ (L : list A) (b : B) (bs : list B) (x y : A) 
          (l : list A) (r : R L b x y) (len : #|bs| = #|l|),
          P L (b :: bs) (x :: l) (y :: l)
            (OnOne2All_hd (R L) b bs x y l r len)
  htl : ∀ (L : list A) (b : B) (bs : list B) (x : A) 
          (l l' : list A) (h : OnOne2All (R L) bs l l'),
          P L bs l l' h
          → P L (b :: bs) (x :: l) (x :: l')
              (OnOne2All_tl (R L) b bs x l l' h)
  l : list A
  b : B
  bs : list B
  hd : A
  tl : list A
  tl' : list A
  h : OnOne2All (R l) bs tl tl'
  IHh : P l bs tl tl' h
  ============================
   (P l (b :: bs) (hd :: tl) (hd :: tl')
      (OnOne2All_tl (R l) b bs hd tl tl' h))


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