Goal:
    A : Type  R : A → A → Type  l : list A
  ============================
   (All (λ x : A, R x x) l → All2 R l l)


DEBUG:Going to execute:
induction 1

Goals:
    A : Type  R : A → A → Type
  ============================
   (All2 R [] [])

  
  A : Type
  R : A → A → Type
  x : A
  l : list A
  p : R x x
  X : All (λ x : A, R x x) l
  IHX : All2 R l l
  ============================
   (All2 R (x :: l) (x :: l))


DEBUG:Going to execute:
constructor

Goals:
    A : Type  R : A → A → Type
  ============================
   (All2 R [] [])

  
  A : Type
  R : A → A → Type
  x : A
  l : list A
  p : R x x
  X : All (λ x : A, R x x) l
  IHX : All2 R l l
  ============================
   (All2 R (x :: l) (x :: l))


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

Goals:
  
  A : Type
  R : A → A → Type
  x : A
  l : list A
  p : R x x
  X : All (λ x : A, R x x) l
  IHX : All2 R l l
  ============================
   (R x x)

  
  A : Type
  R : A → A → Type
  x : A
  l : list A
  p : R x x
  X : All (λ x : A, R x x) l
  IHX : All2 R l l
  ============================
   (All2 R l l)


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  R : A → A → Type
  x : A
  l : list A
  p : R x x
  X : All (λ x : A, R x x) l
  IHX : All2 R l l
  ============================
   (R x x)

  
  A : Type
  R : A → A → Type
  x : A
  l : list A
  p : R x x
  X : All (λ x : A, R x x) l
  IHX : All2 R l l
  ============================
   (All2 R l l)


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