Goal:
  
  A : Type
  P : nat → A → A → Type
  i : nat
  l : list A
  l' : list A
  tl : list A
  ============================
   (OnOne2i P i l l' → OnOne2i P i (l ++ tl) (l' ++ tl))


DEBUG:Going to execute:
induction 1

Goals:
  
  A : Type
  P : nat → A → A → Type
  tl : list A
  i : nat
  hd : A
  hd' : A
  tl0 : list A
  p : P i hd hd'
  ============================
   (OnOne2i P i ((hd :: tl0) ++ tl) ((hd' :: tl0) ++ tl))

  
  A : Type
  P : nat → A → A → Type
  tl : list A
  i : nat
  hd : A
  tl0 : list A
  tl' : list A
  X : OnOne2i P (S i) tl0 tl'
  IHX : OnOne2i P (S i) (tl0 ++ tl) (tl' ++ tl)
  ============================
   (OnOne2i P i ((hd :: tl0) ++ tl) ((hd :: tl') ++ tl))


DEBUG:Going to execute:
constructor

Goals:
  
  A : Type
  P : nat → A → A → Type
  tl : list A
  i : nat
  hd : A
  hd' : A
  tl0 : list A
  p : P i hd hd'
  ============================
   (OnOne2i P i ((hd :: tl0) ++ tl) ((hd' :: tl0) ++ tl))

  
  A : Type
  P : nat → A → A → Type
  tl : list A
  i : nat
  hd : A
  tl0 : list A
  tl' : list A
  X : OnOne2i P (S i) tl0 tl'
  IHX : OnOne2i P (S i) (tl0 ++ tl) (tl' ++ tl)
  ============================
   (OnOne2i P i ((hd :: tl0) ++ tl) ((hd :: tl') ++ tl))


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

Goals:
  
  A : Type
  P : nat → A → A → Type
  tl : list A
  i : nat
  hd : A
  hd' : A
  tl0 : list A
  p : P i hd hd'
  ============================
   (P i hd hd')

  
  A : Type
  P : nat → A → A → Type
  tl : list A
  i : nat
  hd : A
  tl0 : list A
  tl' : list A
  X : OnOne2i P (S i) tl0 tl'
  IHX : OnOne2i P (S i) (tl0 ++ tl) (tl' ++ tl)
  ============================
   (OnOne2i P (S i)
      ((fix app (l m : list A) {struct l} : list A :=
          match l with
          | [] => m
          | a :: l1 => a :: app l1 m
          end) tl0 tl)
      ((fix app (l m : list A) {struct l} : list A :=
          match l with
          | [] => m
          | a :: l1 => a :: app l1 m
          end) tl' tl))


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  P : nat → A → A → Type
  tl : list A
  i : nat
  hd : A
  hd' : A
  tl0 : list A
  p : P i hd hd'
  ============================
   (P i hd hd')

  
  A : Type
  P : nat → A → A → Type
  tl : list A
  i : nat
  hd : A
  tl0 : list A
  tl' : list A
  X : OnOne2i P (S i) tl0 tl'
  IHX : OnOne2i P (S i) (tl0 ++ tl) (tl' ++ tl)
  ============================
   (OnOne2i P (S i)
      ((fix app (l m : list A) {struct l} : list A :=
          match l with
          | [] => m
          | a :: l1 => a :: app l1 m
          end) tl0 tl)
      ((fix app (l m : list A) {struct l} : list A :=
          match l with
          | [] => m
          | a :: l1 => a :: app l1 m
          end) tl' tl))


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