Goal:
    A : Type  P : A → A → Type  l : list A  l' : list A  tl : list A
  ============================
   (OnOne2 P l l' → OnOne2 P (l ++ tl) (l' ++ tl))


DEBUG:Going to execute:
induction 1

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

  
  A : Type
  P : A → A → Type
  tl : list A
  hd : A
  tl0 : list A
  tl' : list A
  X : OnOne2 P tl0 tl'
  IHX : OnOne2 P (tl0 ++ tl) (tl' ++ tl)
  ============================
   (OnOne2 P ((hd :: tl0) ++ tl) ((hd :: tl') ++ tl))


DEBUG:Going to execute:
constructor

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

  
  A : Type
  P : A → A → Type
  tl : list A
  hd : A
  tl0 : list A
  tl' : list A
  X : OnOne2 P tl0 tl'
  IHX : OnOne2 P (tl0 ++ tl) (tl' ++ tl)
  ============================
   (OnOne2 P ((hd :: tl0) ++ tl) ((hd :: tl') ++ tl))


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

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

  
  A : Type
  P : A → A → Type
  tl : list A
  hd : A
  tl0 : list A
  tl' : list A
  X : OnOne2 P tl0 tl'
  IHX : OnOne2 P (tl0 ++ tl) (tl' ++ tl)
  ============================
   (OnOne2 P
      ((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 : A → A → Type
  tl : list A
  hd : A
  hd' : A
  tl0 : list A
  p : P hd hd'
  ============================
   (P hd hd')

  
  A : Type
  P : A → A → Type
  tl : list A
  hd : A
  tl0 : list A
  tl' : list A
  X : OnOne2 P tl0 tl'
  IHX : OnOne2 P (tl0 ++ tl) (tl' ++ tl)
  ============================
   (OnOne2 P
      ((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